divergence definitions

TestingLowerBounds.lean

@@ -4,3 +4,4 @@ import TestingLowerBounds.FDiv
 import TestingLowerBounds.Hellinger
 import TestingLowerBounds.KullbackLeibler
 import TestingLowerBounds.Renyi
+import TestingLowerBounds.TotalVariation

TestingLowerBounds/Hellinger.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2024 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import TestingLowerBounds.FDiv
+
+/-!
+# Squared Helliger distance
+
+## Main definitions
+
+* `FooBar`
+
+## Main statements
+
+* `fooBar_unique`
+
+## Notation
+
+
+
+## Implementation details
+
+
+
+## References
+
+* [F. Bar, *Quuxes*][bibkey]
+
+## Tags
+
+Foobars, barfoos
+-/
+
+open Real MeasureTheory
+
+open scoped ENNReal NNReal Topology
+
+namespace ProbabilityTheory
+
+variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α}
+
+/-- Squared Hellinger distance between two measures. -/
+noncomputable def sqHellinger (μ ν : Measure α) : ℝ := fDivReal (fun x ↦ 2⁻¹ * (1 - sqrt x)^2) μ ν
+
+end ProbabilityTheory

TestingLowerBounds/KullbackLeibler.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Rémy Degenne. All rights reserved.
+Copyright (c) 2024 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/

TestingLowerBounds/TotalVariation.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2024 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import TestingLowerBounds.FDiv
+
+/-!
+# Total variation distance
+
+## Main definitions
+
+* `FooBar`
+
+## Main statements
+
+* `fooBar_unique`
+
+## Notation
+
+
+
+## Implementation details
+
+
+
+## References
+
+* [F. Bar, *Quuxes*][bibkey]
+
+## Tags
+
+Foobars, barfoos
+-/
+
+open Real MeasureTheory
+
+open scoped ENNReal NNReal Topology
+
+namespace ProbabilityTheory
+
+variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α}
+
+/-- Total variation distance between two measures. -/
+noncomputable def tv (μ ν : Measure α) : ℝ := fDivReal (fun x ↦ 2⁻¹ * |1 - x|) μ ν
+
+end ProbabilityTheory

blueprint/src/sections/hellinger.tex

@@ -2,8 +2,8 @@ \chapter{Hellinger distance}
 
 \begin{definition}[Squared Hellinger distance]
   \label{def:Hellinger}
-  %\lean{}
-  %\leanok
+  \lean{ProbabilityTheory.sqHellinger}
+  \leanok
   \uses{def:fDiv}
   Let $\mu, \nu$ be two measures. The squared Hellinger distance between $\mu$ and $\nu$ is
   \begin{align*}

blueprint/src/sections/total_variation.tex

@@ -2,8 +2,8 @@ \chapter{Total variation distance}
 
 \begin{definition}[TV distance]
   \label{def:TV}
-  %\lean{}
-  %\leanok
+  \lean{ProbabilityTheory.tv}
+  \leanok
   \uses{def:fDiv}
     Let $\mu, \nu$ be two measures on $\mathcal X$. The total variation distance between $\mu$ and $\nu$ is
   \begin{align*}