fix name

TestingLowerBounds/CondFDiv.lean

@@ -56,36 +56,36 @@ section Conditional
 open Classical in
 /- Conditional f-divergence. -/
 noncomputable
-def condFDIv (f : ℝ → ℝ) (κ η : kernel α β) (μ : Measure α) : EReal :=
+def condFDiv (f : ℝ → ℝ) (κ η : kernel α β) (μ : Measure α) : EReal :=
   if (∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤)
     ∧ (Integrable (fun x ↦ (fDiv f (κ x) (η x)).toReal) μ)
   then ((μ[fun x ↦ (fDiv f (κ x) (η x)).toReal] : ℝ) : EReal)
   else ⊤
 
-lemma condFDIv_of_not_ae_finite (hf : ¬ ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤) :
-    condFDIv f κ η μ = ⊤ := by
-  rw [condFDIv, if_neg]
+lemma condFDiv_of_not_ae_finite (hf : ¬ ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤) :
+    condFDiv f κ η μ = ⊤ := by
+  rw [condFDiv, if_neg]
   push_neg
   exact fun h ↦ absurd h hf
 
-lemma condFDIv_of_not_integrable
+lemma condFDiv_of_not_integrable
     (hf : ¬ Integrable (fun x ↦ (fDiv f (κ x) (η x)).toReal) μ) :
-    condFDIv f κ η μ = ⊤ := by
-  rw [condFDIv, if_neg]
+    condFDiv f κ η μ = ⊤ := by
+  rw [condFDiv, if_neg]
   push_neg
   exact fun _ ↦ hf
 
-lemma condFDIv_eq (hf_ae : ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤)
+lemma condFDiv_eq (hf_ae : ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤)
     (hf : Integrable (fun x ↦ (fDiv f (κ x) (η x)).toReal) μ) :
-    condFDIv f κ η μ = ((μ[fun x ↦ (fDiv f (κ x) (η x)).toReal] : ℝ) : EReal) :=
+    condFDiv f κ η μ = ((μ[fun x ↦ (fDiv f (κ x) (η x)).toReal] : ℝ) : EReal) :=
   if_pos ⟨hf_ae, hf⟩
 
 variable [MeasurableSpace.CountablyGenerated β]
 
 section Integrable
 
 /-! We show that the integrability of the functions used in `fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η)`
-and in `condFDIv f κ η μ` are equivalent. -/
+and in `condFDiv f κ η μ` are equivalent. -/
 
 -- todo find better name
 theorem _root_.MeasureTheory.Integrable.compProd_mk_left_ae' [NormedAddCommGroup E]
@@ -336,12 +336,12 @@ lemma integrable_fDiv_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKern
     rw [this]
     exact h.sub h_int
 
-lemma condFDIv_ne_top_iff [IsFiniteMeasure μ] [IsMarkovKernel κ] [IsFiniteKernel η] :
-  condFDIv f κ η μ ≠ ⊤ ↔
+lemma condFDiv_ne_top_iff [IsFiniteMeasure μ] [IsMarkovKernel κ] [IsFiniteKernel η] :
+  condFDiv f κ η μ ≠ ⊤ ↔
     (∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a))
       ∧ Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂(η a)) μ
       ∧ (derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) := by
-  rw [condFDIv]
+  rw [condFDiv]
   split_ifs with h
   · have h' := h
     simp_rw [fDiv_ne_top_iff] at h
@@ -370,25 +370,25 @@ lemma condFDIv_ne_top_iff [IsFiniteMeasure μ] [IsMarkovKernel κ] [IsFiniteKern
     rw [integrable_fDiv_iff h_top] at h
     exact h h_int
 
-lemma condFDIv_ne_top_iff_fDiv_compProd_ne_top [IsFiniteMeasure μ]
+lemma condFDiv_ne_top_iff_fDiv_compProd_ne_top [IsFiniteMeasure μ]
     [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
     (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
-    condFDIv f κ η μ ≠ ⊤ ↔ fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) ≠ ⊤ := by
-  rw [condFDIv_ne_top_iff, fDiv_compProd_right_ne_top_iff hf h_cvx]
+    condFDiv f κ η μ ≠ ⊤ ↔ fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) ≠ ⊤ := by
+  rw [condFDiv_ne_top_iff, fDiv_compProd_right_ne_top_iff hf h_cvx]
 
-lemma condFDIv_eq_top_iff_fDiv_compProd_eq_top [IsFiniteMeasure μ]
+lemma condFDiv_eq_top_iff_fDiv_compProd_eq_top [IsFiniteMeasure μ]
     [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
     (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
-    condFDIv f κ η μ = ⊤ ↔ fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) = ⊤ := by
+    condFDiv f κ η μ = ⊤ ↔ fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) = ⊤ := by
   rw [← not_iff_not]
-  exact condFDIv_ne_top_iff_fDiv_compProd_ne_top hf h_cvx
+  exact condFDiv_ne_top_iff_fDiv_compProd_ne_top hf h_cvx
 
-lemma condFDIv_eq_add [IsFiniteMeasure μ]
+lemma condFDiv_eq_add [IsFiniteMeasure μ]
     [IsFiniteKernel κ] [IsFiniteKernel η] (hf_ae : ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤)
     (hf : Integrable (fun x ↦ (fDiv f (κ x) (η x)).toReal) μ) :
-    condFDIv f κ η μ = (μ[fun a ↦ ∫ y, f ((∂κ a/∂η a) y).toReal ∂η a] : ℝ)
+    condFDiv f κ η μ = (μ[fun a ↦ ∫ y, f ((∂κ a/∂η a) y).toReal ∂η a] : ℝ)
       + (derivAtTop f).toReal * (μ[fun a ↦ ((κ a).singularPart (η a) Set.univ).toReal] : ℝ) := by
-  rw [condFDIv_eq hf_ae hf]
+  rw [condFDiv_eq hf_ae hf]
   have : (fun x ↦ EReal.toReal (fDiv f (κ x) (η x)))
       =ᵐ[μ] fun x ↦ ∫ y, f ((∂(κ x)/∂(η x)) y).toReal ∂(η x)
         + (derivAtTop f * (κ x).singularPart (η x) Set.univ).toReal := by
@@ -420,38 +420,38 @@ lemma condFDIv_eq_add [IsFiniteMeasure μ]
   rw [integral_mul_left]
   simp only [_root_.EReal.toReal_coe_ennreal, EReal.coe_mul]
 
-lemma condFDIv_of_derivAtTop_eq_top [IsFiniteMeasure μ]
+lemma condFDiv_of_derivAtTop_eq_top [IsFiniteMeasure μ]
     [IsFiniteKernel κ] [IsFiniteKernel η] (hf_ae : ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤)
     (hf : Integrable (fun x ↦ (fDiv f (κ x) (η x)).toReal) μ) (h_top : derivAtTop f = ⊤) :
-    condFDIv f κ η μ = (μ[fun a ↦ ∫ y, f ((∂κ a/∂η a) y).toReal ∂η a] : ℝ) := by
-  rw [condFDIv_eq_add hf_ae hf]
+    condFDiv f κ η μ = (μ[fun a ↦ ∫ y, f ((∂κ a/∂η a) y).toReal ∂η a] : ℝ) := by
+  rw [condFDiv_eq_add hf_ae hf]
   simp [h_top]
 
 end Integrable
 
 lemma fDiv_compProd_left (μ : Measure α) [IsFiniteMeasure μ]
     (κ η : kernel α β) [IsMarkovKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f)
     (h_cvx : ConvexOn ℝ (Set.Ici 0) f) :
-    fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) = condFDIv f κ η μ := by
-  by_cases hf_top : condFDIv f κ η μ = ⊤
-  · rwa [hf_top, ← condFDIv_eq_top_iff_fDiv_compProd_eq_top hf h_cvx]
+    fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) = condFDiv f κ η μ := by
+  by_cases hf_top : condFDiv f κ η μ = ⊤
+  · rwa [hf_top, ← condFDiv_eq_top_iff_fDiv_compProd_eq_top hf h_cvx]
   have hf_top' := hf_top
   have hf_top'' := hf_top
   have hf_top''' := hf_top
-  rw [← ne_eq, condFDIv_ne_top_iff] at hf_top'
-  rw [condFDIv_eq_top_iff_fDiv_compProd_eq_top hf h_cvx, ← ne_eq, fDiv_ne_top_iff]
+  rw [← ne_eq, condFDiv_ne_top_iff] at hf_top'
+  rw [condFDiv_eq_top_iff_fDiv_compProd_eq_top hf h_cvx, ← ne_eq, fDiv_ne_top_iff]
     at hf_top''
-  rw [condFDIv_eq_top_iff_fDiv_compProd_eq_top hf h_cvx] at hf_top'''
+  rw [condFDiv_eq_top_iff_fDiv_compProd_eq_top hf h_cvx] at hf_top'''
   rcases hf_top' with ⟨h1, h2, h3⟩
   rcases hf_top'' with ⟨h4, h5⟩
   classical
   by_cases h_deriv : derivAtTop f = ⊤
   · rw [fDiv_of_derivAtTop_eq_top h_deriv, if_pos ⟨h4, h5 h_deriv⟩,
-      condFDIv_of_derivAtTop_eq_top _ _ h_deriv]
+      condFDiv_of_derivAtTop_eq_top _ _ h_deriv]
     · sorry
     · sorry
     · sorry
-  · rw [fDiv_of_ne_top, condFDIv_eq_add]
+  · rw [fDiv_of_ne_top, condFDiv_eq_add]
     rotate_left
     · sorry
     · sorry

blueprint/src/sections/chernoff.tex

@@ -4,13 +4,26 @@ \chapter{Chernoff divergence}
   \label{def:Chernoff}
   %\lean{}
   %\leanok
-  \uses{def:Renyi}
-    The Chernoff divergence between two measures $\mu$ and $\nu$ is
+  \uses{def:KL}
+    The Chernoff divergence between two measures $\mu$ and $\nu$ on $\mathcal X$ is
   \begin{align*}
-    C(\mu, \nu) = \max_{\alpha\in [0,1]} (1 - \alpha)R_\alpha(\mu, \nu) \: .
+    C(\mu, \nu) = \inf_{\xi \in \mathcal P(\mathcal X)}\max\{\KL(\xi, \mu), \KL(\xi, \nu)\} \: .
   \end{align*}
 \end{definition}
 
+\begin{lemma}
+  \label{lem:chernoff_eq_max_renyi}
+  %\lean{}
+  %\leanok
+  \uses{def:Chernoff, def:Renyi}
+  \begin{align*}
+  C(\mu, \nu) = \max_{\alpha\in [0,1]} (1 - \alpha)R_\alpha(\mu, \nu) \: .
+  \end{align*}
+\end{lemma}
+
+\begin{proof}
+\end{proof}
+
 \begin{lemma}
   \label{lem:chernoff_symm}
   %\lean{}
@@ -20,6 +33,6 @@ \chapter{Chernoff divergence}
 \end{lemma}
 
 \begin{proof}
-\uses{lem:renyi_symm}
-Apply Lemma~\ref{lem:renyi_symm}.
-\end{proof}
+\uses{lem:chernoff_eq_max_renyi, lem:renyi_symm}
+Apply Lemma~\ref{lem:chernoff_eq_max_renyi}, then Lemma~\ref{lem:renyi_symm}.
+\end{proof}