remove hellingerDiv_symm and rename hellingerDiv_symm' to `hellin…

…gerDiv_symm`
RemyDegenne · Nov 17, 2024 · bbf8c64 · bbf8c64
1 parent 1a37692
commit bbf8c64
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 8 deletions.
diff --git a/TestingLowerBounds/Divergences/Hellinger/Hellinger.lean b/TestingLowerBounds/Divergences/Hellinger/Hellinger.lean
@@ -438,7 +438,7 @@ lemma toReal_hellingerDiv_symm (ha_pos : 0 < a) (ha : a < 1)
   rw [← neg_sub, neg_mul, mul_inv_cancel₀, mul_neg, mul_inv_cancel₀ ha_pos.ne']
   linarith
 
-lemma hellingerDiv_symm' (ha_pos : 0 < a) (ha : a < 1) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
+lemma hellingerDiv_symm (ha_pos : 0 < a) (ha : a < 1) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     ENNReal.ofReal (1 - a) * hellingerDiv a μ ν = ENNReal.ofReal a * hellingerDiv (1 - a) ν μ := by
   rw [← ENNReal.toReal_eq_toReal_iff', ENNReal.toReal_mul, ENNReal.toReal_mul]
   rotate_left
@@ -448,11 +448,6 @@ lemma hellingerDiv_symm' (ha_pos : 0 < a) (ha : a < 1) [IsFiniteMeasure μ] [IsF
   rw [ENNReal.toReal_ofReal ha_pos.le, ENNReal.toReal_ofReal (by linarith)]
   exact toReal_hellingerDiv_symm ha_pos ha
 
-lemma hellingerDiv_symm (ha_pos : 0 < a) (ha : a < 1)
-    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
-    ENNReal.ofReal (1 - a) * hellingerDiv a μ ν = ENNReal.ofReal a * hellingerDiv (1 - a) ν μ :=
-  hellingerDiv_symm' ha_pos ha
-
 -- lemma hellingerDiv_zero_nonneg (μ ν : Measure α) :
 --     0 ≤ hellingerDiv 0 μ ν := hellingerDiv_zero _ _ ▸ EReal.coe_ennreal_nonneg _
 

diff --git a/blueprint/src/sections/hellinger_alpha.tex b/blueprint/src/sections/hellinger_alpha.tex
@@ -78,10 +78,10 @@ \section{Hellinger alpha-divergences}
 
 \begin{lemma}
   \label{lem:hellingerAlpha_symm}
-  \lean{ProbabilityTheory.hellingerDiv_symm'}
+  \lean{ProbabilityTheory.hellingerDiv_symm}
   \leanok
   \uses{def:hellingerAlpha}
-  For $\alpha \in (0, 1)$ and finite measures $\mu, \nu$ with $\mu(\mathcal X) = \nu(\mathcal X)$, $(1 - \alpha) \He_\alpha(\mu, \nu) = \alpha \He_{1 - \alpha}(\nu, \mu)$.
+  For $\alpha \in (0, 1)$ and finite measures $\mu, \nu$, $(1 - \alpha) \He_\alpha(\mu, \nu) = \alpha \He_{1 - \alpha}(\nu, \mu)$.
 \end{lemma}
 
 \begin{proof}\leanok