Skip to content

Commit

Permalink
apply changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@LorenzoLuccioli
LorenzoLuccioli committed Aug 29, 2024
1 parent 7dbb831 commit afa0751
Show file tree
Hide file tree
Showing 6 changed files with 216 additions and 241 deletions.
119 changes: 55 additions & 64 deletions TestingLowerBounds/Divergences/Hellinger.lean
View file

Large diffs are not rendered by default.

66 changes: 32 additions & 34 deletions TestingLowerBounds/Divergences/KullbackLeibler.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -143,12 +143,12 @@ lemma kl_ne_bot (μ ν : Measure α) : kl μ ν ≠ ⊥ := by

lemma kl_ge_mul_log' [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
(hμν : μ ≪ ν) :
(μ Set.univ).toReal * log (μ Set.univ).toReal ≤ kl μ ν :=
(μ .univ).toReal * log (μ .univ).toReal ≤ kl μ ν :=
(le_fDiv_of_ac convexOn_mul_log continuous_mul_log.continuousOn hμν).trans_eq
kl_eq_fDiv.symm

lemma kl_ge_mul_log (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
(μ Set.univ).toReal * log ((μ Set.univ).toReal / (ν Set.univ).toReal) ≤ kl μ ν := by
(μ .univ).toReal * log ((μ .univ).toReal / (ν .univ).toReal) ≤ kl μ ν := by
by_cases hμν : μ ≪ ν
swap; · simp [hμν]
by_cases h_int : Integrable (llr μ ν) μ
Expand All @@ -161,7 +161,7 @@ lemma kl_ge_mul_log (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure
· refine absurd ?_ hμ
rw [hν] at hμν
exact Measure.absolutelyContinuous_zero_iff.mp hμν
let ν' := (ν Set.univ)⁻¹ • ν
let ν' := (ν .univ)⁻¹ • ν
have : IsProbabilityMeasure ν' := by
constructor
simp only [ν', Measure.coe_smul, Pi.smul_apply, smul_eq_mul]
Expand All @@ -172,11 +172,11 @@ lemma kl_ge_mul_log (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure
refine Measure.AbsolutelyContinuous.trans hμν (Measure.absolutelyContinuous_smul ?_)
simp [measure_ne_top ν]
have h := kl_ge_mul_log' hμν'
rw [kl_of_ac_of_integrable hμν', integral_congr_ae (llr_smul_right hμν (ν Set.univ)⁻¹ _ _)] at h
rw [kl_of_ac_of_integrable hμν', integral_congr_ae (llr_smul_right hμν (ν .univ)⁻¹ _ _)] at h
rotate_left
· simp [measure_ne_top ν _]
· simp [hν]
· rw [integrable_congr (llr_smul_right hμν (ν Set.univ)⁻¹ _ _)]
· rw [integrable_congr (llr_smul_right hμν (ν .univ)⁻¹ _ _)]
rotate_left
· simp [measure_ne_top ν _]
· simp [hν]
Expand All @@ -191,14 +191,14 @@ lemma kl_ge_mul_log (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure
simp [hν, measure_ne_top ν]

lemma kl_nonneg' (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
(h : μ Set.univ ≥ ν Set.univ) :
(h : μ .univ ≥ ν .univ) :
0 ≤ kl μ ν := by
by_cases hμν : μ ≪ ν
swap; · rw [kl_of_not_ac hμν]; simp
by_cases h_int : Integrable (llr μ ν) μ
swap; · rw [kl_of_not_integrable h_int]; simp
calc 0
≤ ((μ Set.univ).toReal : EReal) * log ((μ Set.univ).toReal / (ν Set.univ).toReal) := by
≤ ((μ .univ).toReal : EReal) * log ((μ .univ).toReal / (ν .univ).toReal) := by
by_cases h_zero : NeZero ν
swap; · simp [not_neZero.mp h_zero]
refine mul_nonneg (EReal.coe_nonneg.mpr ENNReal.toReal_nonneg) ?_
Expand All @@ -216,7 +216,7 @@ lemma kl_nonneg (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMea

/-- **Converse Gibbs' inequality**: the Kullback-Leibler divergence between two finite measures is
zero if and only if the two distributions are equal. -/
lemma kl_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ Set.univ = ν Set.univ) :
lemma kl_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ .univ = ν .univ) :
kl μ ν = 0 ↔ μ = ν :=
kl_eq_fDiv (μ := μ) (ν := ν) ▸ fDiv_eq_zero_iff h_mass derivAtTop_mul_log
Real.strictConvexOn_mul_log Real.continuous_mul_log.continuousOn (by norm_num)
Expand Down Expand Up @@ -407,7 +407,7 @@ lemma condKL_nonneg (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel

@[simp]
lemma condKL_const {ξ : Measure β} [IsFiniteMeasure ξ] [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
condKL (Kernel.const β μ) (Kernel.const β ν) ξ = (kl μ ν) * ξ Set.univ := by
condKL (Kernel.const β μ) (Kernel.const β ν) ξ = (kl μ ν) * ξ .univ := by
rw [condKL_eq_condFDiv, kl_eq_fDiv]
exact condFDiv_const convexOn_mul_log

Expand Down Expand Up @@ -447,22 +447,22 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
{ξ : Kernel α β} [IsSFiniteKernel ξ] {κ η : Kernel (α × β) γ}
[IsMarkovKernel κ] [IsMarkovKernel η] :
condKL κ η (μ ⊗ₘ ξ) = ⊤
↔ ¬ (∀ᵐ a ∂μ, condKL (Kernel.snd' κ a) (Kernel.snd' η a) (ξ a) ≠ ⊤)
∨ ¬ Integrable (fun x ↦ (condKL (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal) μ := by
↔ ¬ (∀ᵐ a ∂μ, condKL (κ.snd' a) (η.snd' a) (ξ a) ≠ ⊤)
∨ ¬ Integrable (fun x ↦ (condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal) μ := by
rw [condKL_eq_top_iff]
have h_ae_eq (h_ae : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, κ (a, b) ≪ η (a, b))
(h_int : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, Integrable (llr (κ (a, b)) (η (a, b))) (κ (a, b))) :
(fun x ↦ (condKL (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal)
(fun x ↦ (condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal)
=ᵐ[μ] fun a ↦ ∫ b, (kl (κ (a, b)) (η (a, b))).toReal ∂ξ a := by
filter_upwards [h_ae, h_int] with a ha_ae ha_int
rw [condKL_toReal_of_ae_ac_of_ae_integrable]
· simp only [Kernel.snd'_apply]
· filter_upwards [ha_ae] with b hb using Kernel.snd'_apply _ _ _ ▸ hb
· filter_upwards [ha_int] with b hb using Kernel.snd'_apply _ _ _ ▸ hb
· filter_upwards [ha_ae] with b hb using κ.snd'_apply _ _ ▸ hb
· filter_upwards [ha_int] with b hb using κ.snd'_apply _ _ ▸ hb
constructor
· by_cases h_ae : ∀ᵐ x ∂(μ ⊗ₘ ξ), κ x ≪ η x
swap
· rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ae
· rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ae
simp_rw [condKL_ne_top_iff, Kernel.snd'_apply, eventually_and, not_and_or]
intro; left; left
exact h_ae
Expand All @@ -485,7 +485,7 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
simp only [condKL_ne_top_iff, Kernel.snd'_apply] at ha_int2
exact ha_int2.2.2
right
rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ae
rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ae
apply Integrable.congr.mt
swap; exact fun a ↦ ∫ b, (kl (κ (a, b)) (η (a, b))).toReal ∂(ξ a)
push_neg
Expand All @@ -500,7 +500,7 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
contrapose! h
obtain ⟨h_ae, ⟨h_int1, h_int2⟩⟩ := h
rw [ae_compProd_integrable_llr_iff h_ae] at h_int1
rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ae
rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ae
have h_meas := (Integrable.integral_compProd' h_int2).aestronglyMeasurable
rw [Measure.integrable_compProd_iff h_int2.aestronglyMeasurable] at h_int2
constructor
Expand All @@ -524,7 +524,7 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
lemma condKL_compProd_meas [CountableOrCountablyGenerated (α × β) γ] [SFinite μ] {ξ : Kernel α β}
[IsSFiniteKernel ξ] {κ η : Kernel (α × β) γ} [IsMarkovKernel κ] [IsMarkovKernel η]
(h : condKL κ η (μ ⊗ₘ ξ) ≠ ⊤) :
condKL κ η (μ ⊗ₘ ξ) = ∫ x, (condKL (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal ∂μ := by
condKL κ η (μ ⊗ₘ ξ) = ∫ x, (condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal ∂μ := by
rw [condKL_ne_top_iff'.mp h, Measure.integral_compProd (condKL_ne_top_iff.mp h).2.2]
replace h := condKL_compProd_meas_eq_top.mpr.mt h
push_neg at h
Expand Down Expand Up @@ -571,29 +571,28 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
condKL_ne_bot, condKL_of_not_integrable', EReal.add_top_of_ne_bot, kl_ne_bot,
condKL_of_not_ae_integrable]
have intμν := integrable_llr_of_integrable_llr_compProd h_prod h_int
have intκη : Integrable (fun a ↦ ∫ (x : β), log (Kernel.rnDeriv κ η a x).toReal ∂κ a) μ := by
have intκη : Integrable (fun a ↦ ∫ (x : β), log (κ.rnDeriv η a x).toReal ∂κ a) μ := by
apply Integrable.congr (integrable_integral_llr_of_integrable_llr_compProd h_prod h_int)
filter_upwards [hκη] with a ha
apply integral_congr_ae
filter_upwards [ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)] with x hx
filter_upwards [ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)] with x hx
rw [hx, llr_def]
have intκη2 := ae_integrable_llr_of_integrable_llr_compProd h_prod h_int
calc kl (μ ⊗ₘ κ) (ν ⊗ₘ η) = ∫ p, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂(μ ⊗ₘ κ) :=
kl_of_ac_of_integrable h_prod h_int
_ = ∫ a, ∫ x, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) (a, x) ∂κ a ∂μ := mod_cast Measure.integral_compProd h_int
_ = ∫ a, ∫ x, log (μ.rnDeriv ν a).toReal
+ log (Kernel.rnDeriv κ η a x).toReal ∂κ a ∂μ := by
_ = ∫ a, ∫ x, log (μ.rnDeriv ν a).toReal + log (κ.rnDeriv η a x).toReal ∂κ a ∂μ := by
norm_cast
have h := hμν.ae_le (Measure.ae_ae_of_ae_compProd (Kernel.rnDeriv_measure_compProd μ ν κ η))
apply Kernel.integral_congr_ae₂
filter_upwards [h, hκη, Measure.rnDeriv_toReal_pos hμν] with a ha hκηa hμν_pos
have hμν_zero : (μ.rnDeriv ν a).toReal ≠ 0 := by linarith
filter_upwards [Kernel.rnDeriv_toReal_pos hκηa, hκηa.ae_le ha] with x hκη_pos hx
have hκη_zero : (Kernel.rnDeriv κ η a x).toReal ≠ 0 := by linarith
have hκη_zero : (κ.rnDeriv η a x).toReal ≠ 0 := by linarith
rw [llr, hx, ENNReal.toReal_mul]
exact log_mul hμν_zero hκη_zero
_ = ∫ a, ∫ _, log (μ.rnDeriv ν a).toReal ∂κ a ∂μ
+ ∫ a, ∫ x, log (Kernel.rnDeriv κ η a x).toReal ∂κ a ∂μ := by
+ ∫ a, ∫ x, log (κ.rnDeriv η a x).toReal ∂κ a ∂μ := by
norm_cast
rw [← integral_add']
simp only [Pi.add_apply]
Expand All @@ -603,7 +602,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
· exact intκη
apply integral_congr_ae
filter_upwards [hκη, intκη2] with a ha hκηa
have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
have h := ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)
rw [← integral_add']
rotate_left
· simp only [integrable_const]
Expand All @@ -619,7 +618,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
congr 2
apply Kernel.integral_congr_ae₂
filter_upwards [hκη] with a ha
have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
have h := ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)
filter_upwards [h] with x hx
congr
_ = kl μ ν + condKL κ η μ := by
Expand All @@ -630,7 +629,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
simp_rw [llr_def]
apply Integrable.congr intκη
filter_upwards [hκη] with a ha
have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
have h := ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)
apply integral_congr_ae
filter_upwards [h] with x hx
rw [hx]
Expand Down Expand Up @@ -672,13 +671,13 @@ lemma kl_compProd_kernel_of_ae_ac_of_ae_integrable [CountableOrCountablyGenerate
simp only [Kernel.absolutelyContinuous_compProd_iff, eventually_and] at h_ac
filter_upwards [h_ac.1, h_ac.2, h_ae_int.1, h_ae_int.2.1, h_ae_int.2.2] with a ha_ac₁ ha_ac₂
ha_int₁ ha_int_kl₂ ha_int₂
have h_snd_ne_top : condKL (Kernel.snd' κ₂ a) (Kernel.snd' η₂ a) (κ₁ a) ≠ ⊤ := by
have h_snd_ne_top : condKL (κ₂.snd' a) (η₂.snd' a) (κ₁ a) ≠ ⊤ := by
apply condKL_ne_top_iff.mpr
simp_rw [Kernel.snd'_apply]
exact ⟨ha_ac₂, ⟨ha_int₂, ha_int_kl₂⟩⟩
simp_rw [Kernel.compProd_apply_eq_compProd_snd', kl_compProd,
EReal.toReal_add (kl_ne_top_iff.mpr ⟨ha_ac₁, ha_int₁⟩) (kl_ne_bot (κ₁ a) (η₁ a)) h_snd_ne_top
(condKL_ne_bot (Kernel.snd' κ₂ a) (Kernel.snd' η₂ a) (κ₁ a)),
(condKL_ne_bot (κ₂.snd' a) (η₂.snd' a) (κ₁ a)),
condKL_ne_top_iff'.mp h_snd_ne_top, EReal.toReal_coe, Kernel.snd'_apply]

lemma condKL_compProd_kernel_eq_top [CountableOrCountablyGenerated (α × β) γ] {κ₁ η₁ : Kernel α β}
Expand All @@ -691,14 +690,13 @@ lemma condKL_compProd_kernel_eq_top [CountableOrCountablyGenerated (α × β) γ
simp only [condKL_isEmpty_left]
tauto
have := countableOrCountablyGenerated_right_of_prod_left_of_nonempty (α := α) (β := β) (γ := γ)
simp_rw [condKL_eq_top_iff,
Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)]
simp_rw [condKL_eq_top_iff, Measure.ae_compProd_iff (κ₂.measurableSet_absolutelyContinuous _)]
by_cases h_ac : ∀ᵐ a ∂μ, (κ₁ ⊗ₖ κ₂) a ≪ (η₁ ⊗ₖ η₂) a
<;> have h_ac' := h_ac
<;> simp only [Kernel.absolutelyContinuous_compProd_iff, eventually_and, not_and_or] at h_ac'
<;> simp only [h_ac, h_ac', not_false_eq_true, true_or, not_true, true_iff, false_or]
swap; tauto
rw [← Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ac'
rw [← Measure.ae_compProd_iff (κ₂.measurableSet_absolutelyContinuous _)] at h_ac'
by_cases h_ae_int : ∀ᵐ a ∂μ, Integrable (llr ((κ₁ ⊗ₖ κ₂) a) ((η₁ ⊗ₖ η₂) a)) ((κ₁ ⊗ₖ κ₂) a)
<;> have h_ae_int' := h_ae_int
<;> simp only [eventually_congr (h_ac.mono (fun a h ↦ (Kernel.integrable_llr_compProd_iff' a h))),
Expand Down Expand Up @@ -757,7 +755,7 @@ variable {β : Type*} {mβ : MeasurableSpace β}

lemma kl_prod_two' [CountableOrCountablyGenerated α β] {ξ ψ : Measure β} [IsProbabilityMeasure ξ]
[IsProbabilityMeasure ψ] [IsFiniteMeasure μ] [IsFiniteMeasure ν]:
kl (μ.prod ξ) (ν.prod ψ) = kl μ ν + kl ξ ψ * (μ Set.univ) := by
kl (μ.prod ξ) (ν.prod ψ) = kl μ ν + kl ξ ψ * (μ .univ) := by
simp only [← condKL_const, ← kl_compProd, Measure.compProd_const]

/--Tensorization property for KL divergence-/
Expand All @@ -783,7 +781,7 @@ lemma Measure.pi_map_piCongrLeft {ι ι' : Type*} [hι : Fintype ι] [hι' : Fin
refine Measure.pi_eq (fun s _ ↦ ?_) |>.symm
rw [e_meas.measurableEmbedding.map_apply]
let s' : (i : ι) → Set (β (e i)) := fun i ↦ s (e i)
have : e_meas ⁻¹' Set.pi Set.univ s = Set.pi Set.univ s' := by
have : e_meas ⁻¹' Set.univ.pi s = Set.univ.pi s' := by
ext x
simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, forall_true_left, s']
refine (e.forall_congr ?_).symm
Expand Down
16 changes: 8 additions & 8 deletions TestingLowerBounds/Divergences/Renyi.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ Hellinger divergence to the Rényi divergence. -/

noncomputable def renyiDiv (a : ℝ) (μ ν : Measure α) : EReal :=
if a = 1 then kl μ ν
else (a - 1)⁻¹ * ENNReal.log ((↑(ν Set.univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal)
else (a - 1)⁻¹ * ENNReal.log ((↑(ν .univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal)

@[simp]
lemma renyiDiv_zero (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure ν] :
Expand All @@ -99,7 +99,7 @@ lemma renyiDiv_one (μ ν : Measure α) : renyiDiv 1 μ ν = kl μ ν := by

lemma renyiDiv_of_ne_one (ha_ne_one : a ≠ 1) (μ ν : Measure α) :
renyiDiv a μ ν
= (a - 1)⁻¹ * ENNReal.log ((↑(ν Set.univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal) := by
= (a - 1)⁻¹ * ENNReal.log ((↑(ν .univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal) := by
rw [renyiDiv, if_neg ha_ne_one]

@[simp]
Expand Down Expand Up @@ -312,7 +312,7 @@ lemma renyiDiv_eq_log_integral' (ha_pos : 0 < a) (ha : a ≠ 1) [IsFiniteMeasure

end IntegralForm

lemma renyiDiv_symm' (ha_pos : 0 < a) (ha : a < 1) (h_eq : μ Set.univ = ν Set.univ)
lemma renyiDiv_symm' (ha_pos : 0 < a) (ha : a < 1) (h_eq : μ .univ = ν .univ)
[IsFiniteMeasure μ] [IsFiniteMeasure ν] :
(1 - a) * renyiDiv a μ ν = a * renyiDiv (1 - a) ν μ := by
rw [renyiDiv_of_ne_one ha.ne, renyiDiv_of_ne_one (by linarith)]
Expand Down Expand Up @@ -491,7 +491,7 @@ lemma condRenyiDiv_of_ne_zero [CountableOrCountablyGenerated α β] (ha_nonneg :
(ha_ne_one : a ≠ 1) (κ η : Kernel α β) (μ : Measure α) [IsFiniteKernel κ] [∀ x, NeZero (κ x)]
[IsFiniteKernel η] [IsFiniteMeasure μ] :
condRenyiDiv a κ η μ = (a - 1)⁻¹
* ENNReal.log (↑((μ ⊗ₘ η) Set.univ) + (a - 1) * (condHellingerDiv a κ η μ)).toENNReal := by
* ENNReal.log (↑((μ ⊗ₘ η) .univ) + (a - 1) * (condHellingerDiv a κ η μ)).toENNReal := by
rw [condRenyiDiv, renyiDiv_of_ne_one ha_ne_one, hellingerDiv_compProd_left ha_nonneg _]

end TopAndBounds
Expand All @@ -505,7 +505,7 @@ variable {β : Type*} {mβ : MeasurableSpace β} {κ η : Kernel α β}

lemma le_renyiDiv_of_le_hellingerDiv {a : ℝ} {μ₁ ν₁ : Measure α} {μ₂ ν₂ : Measure β}
[SigmaFinite μ₁] [SigmaFinite ν₁] [SigmaFinite μ₂] [SigmaFinite ν₂]
(h_eq : ν₁ Set.univ = ν₂ Set.univ) (h_le : hellingerDiv a μ₁ ν₁ ≤ hellingerDiv a μ₂ ν₂) :
(h_eq : ν₁ .univ = ν₂ .univ) (h_le : hellingerDiv a μ₁ ν₁ ≤ hellingerDiv a μ₂ ν₂) :
renyiDiv a μ₁ ν₁ ≤ renyiDiv a μ₂ ν₂ := by
rcases lt_trichotomy a 1 with (ha | rfl | ha)
· simp_rw [renyiDiv_of_ne_one ha.ne, h_eq]
Expand All @@ -514,7 +514,7 @@ lemma le_renyiDiv_of_le_hellingerDiv {a : ℝ} {μ₁ ν₁ : Measure α} {μ₂
gcongr
· simp only [EReal.coe_nonneg, inv_nonneg, sub_nonneg, ha.le]
refine ENNReal.log_monotone <| EReal.toENNReal_le_toENNReal ?_
gcongr (ν₂ Set.univ) + ?_
gcongr (ν₂ .univ) + ?_
apply EReal.neg_le_neg_iff.mp
norm_cast
simp_rw [← neg_mul, ← EReal.coe_neg, neg_sub]
Expand All @@ -536,7 +536,7 @@ lemma le_renyiDiv_compProd [CountableOrCountablyGenerated α β] (ha_pos : 0 < a
(κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η] :
renyiDiv a μ ν ≤ renyiDiv a (μ ⊗ₘ κ) (ν ⊗ₘ η) := by
refine le_renyiDiv_of_le_hellingerDiv ?_ (le_hellingerDiv_compProd ha_pos μ ν κ η)
rw [Measure.compProd_apply MeasurableSet.univ]
rw [Measure.compProd_apply .univ]
simp

lemma renyiDiv_fst_le [Nonempty β] [StandardBorelSpace β] (ha_pos : 0 < a)
Expand Down Expand Up @@ -570,7 +570,7 @@ lemma renyiDiv_comp_right_le [Nonempty α] [StandardBorelSpace α] (ha_pos : 0 <
(κ : Kernel α β) [IsMarkovKernel κ] :
renyiDiv a (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ renyiDiv a μ ν := by
refine le_renyiDiv_of_le_hellingerDiv ?_ (hellingerDiv_comp_right_le ha_pos μ ν κ)
rw [← Measure.snd_compProd ν κ, Measure.snd_univ, Measure.compProd_apply MeasurableSet.univ]
rw [← Measure.snd_compProd ν κ, Measure.snd_univ, Measure.compProd_apply .univ]
simp

end DataProcessingInequality
Expand Down
4 changes: 2 additions & 2 deletions TestingLowerBounds/Divergences/StatInfo.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ lemma statInfo_of_measure_false_eq_zero (μ ν : Measure 𝒳) (hπ : π {false}
lemma statInfo_comp_le (μ ν : Measure 𝒳) (π : Measure Bool) (η : Kernel 𝒳 𝒳') [IsMarkovKernel η] :
statInfo (η ∘ₘ μ) (η ∘ₘ ν) π ≤ statInfo μ ν π := by
refine tsub_le_tsub ?_ (bayesBinaryRisk_le_bayesBinaryRisk_comp _ _ _ _)
simp [Measure.bind_apply MeasurableSet.univ (Kernel.measurable _)]
simp [Measure.bind_apply .univ (Kernel.measurable _)]

lemma toReal_statInfo_eq_toReal_sub [IsFiniteMeasure ν] [IsFiniteMeasure π] :
(statInfo μ ν π).toReal = (min (π {false} * μ univ) (π {true} * ν univ)).toReal
Expand Down Expand Up @@ -940,7 +940,7 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_mutuallySingular [IsFiniteMeasure μ
← lintegral_mul_const _]
swap
· simp_rw [derivAtTop_statInfoFun_eq]
refine (Measurable.ite (MeasurableSet.const _) ?_ ?_).coe_real_ereal.ereal_toENNReal <;>
refine (Measurable.ite (.const _) ?_ ?_).coe_real_ereal.ereal_toENNReal <;>
· refine Measurable.ite (measurableSet_le (fun _ a ↦ a) ?_) ?_ ?_ <;> exact measurable_const
rw [← lintegral_add_left]
swap; · exact measurable_statInfoFun2.ennreal_ofReal.mul_const _
Expand Down
Loading

0 comments on commit afa0751

Please sign in to comment.