Stat.Minimax

theorem one_sub_tvDist_le_test {A : Set Ω} (hA : MeasurableSet A) : 1 - tvDist μ ν ≤ μ.real A + ν.real Aᶜ := by have hcompl : ν.real Aᶜ = 1 - ν.real A := by rw [measureReal_compl hA, probReal_univ] rw [hcompl] have h := measureReal_sub_le_tvDist (μ := μ) (ν := ν) hA linarith

theorem tvDist_le_half_sqrt_chiSqDiv (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) (hint : Integrable (fun x => ((μ.rnDeriv ν x).toReal - 1) ^ 2) ν) : tvDist μ ν ≤ (1/2) * sqrt (chiSqDiv μ ν) := by -- Density deviation `f = p − 1`. set f : Ω → ℝ := fun x => (μ.rnDeriv ν x).toReal - 1 with hf_def have hmeas : AEStronglyMeasurable f ν := (Measure.measurable_rnDeriv μ ν).ennreal_toReal.aestronglyMeasurable.sub aestronglyMeasurable_const -- `f ∈ L²(ν)` since `f²` is integrable. have hfL2 : MemLp f 2 ν := (memLp_two_iff_integrable_sq hmeas).2 hint -- `|f| ∈ L²(ν)` (same norm) and `1 ∈ L²(ν)` (`ν` probability). have habsL2 : MemLp (fun x => |f x|) (ofReal 2) ν := by have h := hfL2.norm simp only [Real.norm_eq_abs] at h simpa using h have honeL2 : MemLp (fun _ : Ω => (1:ℝ)) (ofReal 2) ν := by simpa using (memLp_const (1:ℝ) : MemLp (fun _ : Ω => (1:ℝ)) 2 ν) -- Hölder with `p = q = 2`: `∫ |f|·1 ≤ (∫ |f|²)^½ · (∫ 1²)^½`. have hholder : ∫ x, |f x| * (1:ℝ) ∂ν ≤ (∫ x, |f x| ^ (2:ℝ) ∂ν) ^ (1 / (2:ℝ)) * (∫ x, (1:ℝ) ^ (2:ℝ) ∂ν) ^ (1 / (2:ℝ)) := integral_mul_le_Lp_mul_Lq_of_nonneg Real.HolderConjugate.two_two (Filter.Eventually.of_forall fun x => abs_nonneg _) (Filter.Eventually.of_forall fun _ => zero_le_one) habsL2 honeL2 -- Simplify the right-hand factors. have hone : (∫ x, (1:ℝ) ^ (2:ℝ) ∂ν) ^ (1 / (2:ℝ)) = 1 := by simp have hLHS : ∫ x, |f x| * (1:ℝ) ∂ν = ∫ x, |f x| ∂ν := by simp -- `∫ |f|² = chiSqDiv μ ν` (rewrite real power 2 to `^2`). have hsq : ∫ x, |f x| ^ (2:ℝ) ∂ν = chiSqDiv μ ν := by rw [chiSqDiv] apply integral_congr_ae refine Filter.Eventually.of_forall fun x => ?_ change |f x| ^ (2:ℝ) = (f x) ^ 2 rw [Real.rpow_two, sq_abs] -- `∫ |f| ≤ √(chiSqDiv μ ν)`. have hint_abs : ∫ x, |f x| ∂ν ≤ sqrt (chiSqDiv μ ν) := by rw [hLHS, hsq, hone, mul_one] at hholder have hrw : (chiSqDiv μ ν) ^ (1 / (2:ℝ)) = sqrt (chiSqDiv μ ν) := (Real.sqrt_eq_rpow (chiSqDiv μ ν)).symm rwa [hrw] at hholder -- Combine with Scheffé. have hscheffe := tvDist_le_half_integral_abs_rnDeriv μ ν hac calc tvDist μ ν ≤ (1/2) * ∫ x, |f x| ∂ν := hscheffe _ ≤ (1/2) * sqrt (chiSqDiv μ ν) := by apply mul_le_mul_of_nonneg_left hint_abs (by norm_num)

theorem one_add_chiSqDiv_pi_iid {Ω : Type*} [MeasurableSpace Ω] [Fintype Ω] [MeasurableSingletonClass Ω] (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) (n : ℕ) : 1 + chiSqDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν)) = (1 + chiSqDiv μ ν) ^ n := by induction n with | zero => rw [Measure.pi_of_empty (fun _ : Fin 0 => μ), Measure.pi_of_empty (fun _ : Fin 0 => ν), chiSqDiv_self] simp | succ n ih => have hμ := (measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => μ) 0).map_eq have hν := (measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => ν) 0).map_eq rw [← chiSqDiv_map_measurableEquiv (MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) => Ω) 0), hμ, hν] have hac_pi : Measure.pi (fun _ : Fin n => μ) ≪ Measure.pi (fun _ : Fin n => ν) := pi_iid_absolutelyContinuous μ ν hac n rw [chiSqDiv_prod μ ν (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν)) hac hac_pi (Integrable.of_finite) (Integrable.of_finite), ih, pow_succ] ring

theorem one_add_chiSqDiv_pi_iid_general {S : Type*} [MeasurableSpace S] (μ ν : Measure S) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) (hint : Integrable (fun x => ((μ.rnDeriv ν x).toReal - 1) ^ 2) ν) (n : ℕ) : 1 + chiSqDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν)) = (1 + chiSqDiv μ ν) ^ n := by induction n with | zero => rw [Measure.pi_of_empty (fun _ : Fin 0 => μ), Measure.pi_of_empty (fun _ : Fin 0 => ν), chiSqDiv_self] simp | succ n ih => have hμ := (measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => μ) 0).map_eq have hν := (measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => ν) 0).map_eq rw [← chiSqDiv_map_measurableEquiv (MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) => S) 0), hμ, hν] have hac_pi : Measure.pi (fun _ : Fin n => μ) ≪ Measure.pi (fun _ : Fin n => ν) := pi_iid_absolutelyContinuous μ ν hac n rw [chiSqDiv_prod μ ν (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν)) hac hac_pi hint (pi_iid_integrable_sq_dev μ ν hac hint n), ih, pow_succ] ring

lemma testing_error_lower_of_chi {Ω : Type*} [MeasurableSpace Ω] (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hac : P ≪ Q) (hint : Integrable (fun x => ((P.rnDeriv Q x).toReal - 1) ^ 2) Q) {C : ℝ} (hC : 0 ≤ C) (hchi : chiSqDiv P Q ≤ C) {A : Set Ω} (hA : MeasurableSet A) : P.real Aᶜ + Q.real A ≥ 1 / (4 * (C + 1)) := by let e : ℝ := P.real Aᶜ + Q.real A let K : ℝ := C + 1 have hKpos : 0 < K := by dsimp [K] linarith have hKge1 : 1 ≤ K := by dsimp [K] linarith have hQ_nonneg : 0 ≤ Q.real A := measureReal_nonneg have hPcomp_nonneg : 0 ≤ P.real Aᶜ := measureReal_nonneg have hcs : P.real A ≤ sqrt (K * Q.real A) := by simpa [K] using rnDeriv_setIntegral_le_sqrt_chi P Q hac hint hchi hA have hcomp : P.real Aᶜ = 1 - P.real A := by rw [measureReal_compl hA, probReal_univ] have hgap : 1 - e ≤ sqrt (K * Q.real A) := by dsimp [e] rw [hcomp] linarith [hcs, hQ_nonneg] by_contra hnot have hlt : e < 1 / (4 * K) := by exact lt_of_not_ge (by simpa [e, K] using hnot) have hQ_le_e : Q.real A ≤ e := by dsimp [e] linarith have hQ_lt : Q.real A < 1 / (4 * K) := lt_of_le_of_lt hQ_le_e hlt have hKQ_lt : K * Q.real A < 1 / 4 := by calc K * Q.real A < K * (1 / (4 * K)) := mul_lt_mul_of_pos_left hQ_lt hKpos _ = 1 / 4 := by field_simp [hKpos.ne'] have hsqrt_lt : sqrt (K * Q.real A) < 1 / 2 := by rw [Real.sqrt_lt' (by norm_num : (0 : ℝ) < 1 / 2)] norm_num exact hKQ_lt have hc_le_quarter : 1 / (4 * K) ≤ 1 / 4 := by have hden : 0 < 4 * K := mul_pos (by norm_num) hKpos rw [one_div_le_one_div hden (by norm_num : (0 : ℝ) < 4)] nlinarith have he_lt_quarter : e < 1 / 4 := lt_of_lt_of_le hlt hc_le_quarter have hleft_gt : 1 / 2 < 1 - e := by linarith have hleft_lt : 1 - e < 1 / 2 := lt_of_le_of_lt hgap hsqrt_lt linarith

lemma le_cam_two_point_chisq : (∀ Cchi : ℝ, 0 ≤ Cchi → ∃ c : ℝ, 0 < c ∧ ∀ {Ω : Type} [MeasurableSpace Ω] (Pp Pm : Measure Ω) [IsProbabilityMeasure Pp] [IsProbabilityMeasure Pm], Pp ≪ Pm → Integrable (fun x => ((Pp.rnDeriv Pm x).toReal - 1) ^ 2) Pm → chiSqDiv Pp Pm ≤ Cchi → ∀ A : Set Ω, MeasurableSet A → Pp.real Aᶜ + Pm.real A ≥ c) ∧ (∀ c0 : ℝ, 0 ≤ c0 → ∃ c' : ℝ, 0 < c' ∧ ∀ {Ω : Type} [MeasurableSpace Ω] (Pp Pm : Measure Ω) [IsProbabilityMeasure Pp] [IsProbabilityMeasure Pm], Pp ≪ Pm → Integrable (fun x => ((Pp.rnDeriv Pm x).toReal - 1) ^ 2) Pm → ∀ (m : ℕ), 0 < m → chiSqDiv Pp Pm ≤ c0 / (m : ℝ) → ∀ A : Set (Fin m → Ω), MeasurableSet A → (Measure.pi (fun _ : Fin m => Pp)).real Aᶜ + (Measure.pi (fun _ : Fin m => Pm)).real A ≥ c') := by constructor · intro Cchi hCchi refine ⟨1 / (4 * (Cchi + 1)), by positivity, ?_⟩ intro Ω _ Pp Pm _ _ hac hint hchi A hA exact testing_error_lower_of_chi Pp Pm hac hint hCchi hchi hA · intro c0 hc0 refine ⟨1 / (4 * exp c0), by positivity, ?_⟩ intro Ω _ Pp Pm _ _ hac hint m hm hchi A hA let Pprod : Measure (Fin m → Ω) := Measure.pi (fun _ : Fin m => Pp) let Qprod : Measure (Fin m → Ω) := Measure.pi (fun _ : Fin m => Pm) have hac_prod : Pprod ≪ Qprod := by dsimp [Pprod, Qprod] exact pi_iid_absolutelyContinuous Pp Pm hac m have hint_prod : Integrable (fun x => ((Pprod.rnDeriv Qprod x).toReal - 1) ^ 2) Qprod := by dsimp [Pprod, Qprod] exact pi_iid_integrable_sq_dev Pp Pm hac hint m have hchi_non : 0 ≤ chiSqDiv Pp Pm := chiSqDiv_nonneg have hmR : 0 < (m : ℝ) := by exact_mod_cast hm have hmul : (m : ℝ) * chiSqDiv Pp Pm ≤ c0 := by have := mul_le_mul_of_nonneg_left hchi (le_of_lt hmR) field_simp [hmR.ne'] at this exact this have hpow : (1 + chiSqDiv Pp Pm) ^ m ≤ exp ((m : ℝ) * chiSqDiv Pp Pm) := by calc (1 + chiSqDiv Pp Pm) ^ m ≤ (exp (chiSqDiv Pp Pm)) ^ m := by exact pow_le_pow_left₀ (by linarith) (by linarith [Real.add_one_le_exp (chiSqDiv Pp Pm)]) m _ = exp ((m : ℝ) * chiSqDiv Pp Pm) := by rw [← Real.exp_nat_mul] have hexp_le : exp ((m : ℝ) * chiSqDiv Pp Pm) ≤ exp c0 := by exact Real.exp_le_exp.mpr hmul have hprod_eq : 1 + chiSqDiv Pprod Qprod = (1 + chiSqDiv Pp Pm) ^ m := by dsimp [Pprod, Qprod] exact one_add_chiSqDiv_pi_iid_general Pp Pm hac hint m have hchi_prod : chiSqDiv Pprod Qprod ≤ exp c0 - 1 := by have hone : 1 + chiSqDiv Pprod Qprod ≤ exp c0 := by rw [hprod_eq] exact hpow.trans hexp_le linarith have hCprod_nonneg : 0 ≤ exp c0 - 1 := by have h1 : 1 ≤ exp c0 := by have := Real.add_one_le_exp c0 linarith linarith have htest := testing_error_lower_of_chi Pprod Qprod hac_prod hint_prod hCprod_nonneg hchi_prod hA have hconst : 1 / (4 * ((exp c0 - 1) + 1)) = 1 / (4 * exp c0) := by ring_nf simpa [Pprod, Qprod, hconst] using htest

theorem assouad_average (hmeas : ∀ j (b : Bool), MeasurableSet {ω | est ω j = b}) {β : ℝ} (hβ : ∀ j τ, tvDist (P τ) (P (flipBit j τ)) ≤ β) : (d / 2 : ℝ) * (1 - β) ≤ (∑ τ, hammingRisk P est τ) / (card (Fin d → Bool)) := by set C : ℝ := (card (Fin d → Bool) : ℝ) with hC have hCnat : 0 < card (Fin d → Bool) := Fintype.card_pos_iff.mpr ⟨fun _ => false⟩ have hCpos : (0 : ℝ) < C := by rw [hC]; exact_mod_cast hCnat -- Per coordinate: `C·(1−β)/2 ≤ ∑_τ (coordinate-j error mass)`. have hG : ∀ j, C * (1 - β) / 2 ≤ ∑ τ, (P τ).real {ω | est ω j ≠ τ j} := by intro j have hcoord := sum_decode_ge P est hmeas j have hβsum : C * (1 - β) ≤ ∑ τ, (1 - tvDist (P τ) (P (flipBit j τ))) := by have h1 : ∑ _τ : Fin d → Bool, (1 - β) ≤ ∑ τ, (1 - tvDist (P τ) (P (flipBit j τ))) := Finset.sum_le_sum (fun τ _ => by linarith [hβ j τ]) have h2 : ∑ _τ : Fin d → Bool, (1 - β) = C * (1 - β) := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, hC] linarith [h1, h2] linarith [hβsum, hcoord] -- Sum the coordinate bounds, then divide by the cube size. have hswap : ∑ τ, hammingRisk P est τ = ∑ j, ∑ τ, (P τ).real {ω | est ω j ≠ τ j} := by simp_rw [hammingRisk]; rw [Finset.sum_comm] have hfinal : (d : ℝ) * (C * (1 - β) / 2) ≤ ∑ τ, hammingRisk P est τ := by rw [hswap] have h2 : (d : ℝ) * (C * (1 - β) / 2) = ∑ _j : Fin d, (C * (1 - β) / 2) := by rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] rw [h2] exact Finset.sum_le_sum (fun j _ => hG j) rw [le_div_iff₀ hCpos] have hrw : (d / 2 : ℝ) * (1 - β) * C = (d : ℝ) * (C * (1 - β) / 2) := by ring rw [hrw]; exact hfinal

theorem assouad_exists (hmeas : ∀ j (b : Bool), MeasurableSet {ω | est ω j = b}) {β : ℝ} (hβ : ∀ j τ, tvDist (P τ) (P (flipBit j τ)) ≤ β) : ∃ τ, (d / 2 : ℝ) * (1 - β) ≤ hammingRisk P est τ := by set C : ℝ := (card (Fin d → Bool) : ℝ) with hC have hCnat : 0 < card (Fin d → Bool) := Fintype.card_pos_iff.mpr ⟨fun _ => false⟩ have hCpos : (0 : ℝ) < C := by rw [hC]; exact_mod_cast hCnat have havg := assouad_average P est hmeas hβ rw [← hC] at havg by_contra hcon push_neg at hcon have hstrict : ∑ τ, hammingRisk P est τ < C * ((d / 2 : ℝ) * (1 - β)) := by calc ∑ τ, hammingRisk P est τ < ∑ _τ : Fin d → Bool, ((d / 2 : ℝ) * (1 - β)) := Finset.sum_lt_sum_of_nonempty ⟨fun _ => false, Finset.mem_univ _⟩ (fun τ _ => hcon τ) _ = C * ((d / 2 : ℝ) * (1 - β)) := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, hC] rw [le_div_iff₀ hCpos] at havg nlinarith [havg, hstrict]

theorem real_two_point_lower_bound {est : Ω → ℝ} (hest : Measurable est) {θ₀ θ₁ s : ℝ} (hsep : 2 * s ≤ |θ₀ - θ₁|) : (1 - tvDist P₀ P₁) / 2 ≤ max (P₀.real {ω | s ≤ |est ω - θ₀|}) (P₁.real {ω | s ≤ |est ω - θ₁|}) := by have hsep' : 2 * s ≤ dist θ₀ θ₁ := by rwa [Real.dist_eq] have h := half_one_sub_tvDist_le_max_error (P₀ := P₀) (P₁ := P₁) (Θ := ℝ) hest hsep' simpa only [Real.dist_eq] using h

theorem two_point_lower_bound_of_tvDist_le {est : Ω → ℝ} (hest : Measurable est) {θ₀ θ₁ s c : ℝ} (hsep : 2 * s ≤ |θ₀ - θ₁|) (hc : tvDist P₀ P₁ ≤ c) : (1 - c) / 2 ≤ max (P₀.real {ω | s ≤ |est ω - θ₀|}) (P₁.real {ω | s ≤ |est ω - θ₁|}) := by have h := real_two_point_lower_bound (P₀ := P₀) (P₁ := P₁) hest hsep have : (1 - c) / 2 ≤ (1 - tvDist P₀ P₁) / 2 := by linarith exact this.trans h

theorem iid_two_point_lower_bound {S : Type*} [MeasurableSpace S] (P₀ P₁ : Measure S) [IsProbabilityMeasure P₀] [IsProbabilityMeasure P₁] (τ : Measure S → ℝ) (n : ℕ) {s : ℝ} (hsep : 2 * s ≤ |τ P₀ - τ P₁|) {est : (Fin n → S) → ℝ} (hest : Measurable est) : (1 - tvDist (Measure.pi fun _ : Fin n => P₀) (Measure.pi fun _ : Fin n => P₁)) / 2 ≤ max ((Measure.pi fun _ : Fin n => P₀).real {x | s ≤ |est x - τ P₀|}) ((Measure.pi fun _ : Fin n => P₁).real {x | s ≤ |est x - τ P₁|}) := real_two_point_lower_bound (P₀ := Measure.pi fun _ : Fin n => P₀) (P₁ := Measure.pi fun _ : Fin n => P₁) hest hsep

theorem two_point_lower_bound_of_chiSqDiv_le {est : Ω → ℝ} (hest : Measurable est) {θ₀ θ₁ s : ℝ} (hsep : 2 * s ≤ |θ₀ - θ₁|) (hac : P₀ ≪ P₁) (hint : Integrable (fun x => ((P₀.rnDeriv P₁ x).toReal - 1) ^ 2) P₁) {c : ℝ} (hc : chiSqDiv P₀ P₁ ≤ c) : (1 - (1 / 2) * sqrt c) / 2 ≤ max (P₀.real {ω | s ≤ |est ω - θ₀|}) (P₁.real {ω | s ≤ |est ω - θ₁|}) := by have htv : tvDist P₀ P₁ ≤ (1 / 2) * sqrt c := by refine (tvDist_le_half_sqrt_chiSqDiv P₀ P₁ hac hint).trans ?_ gcongr exact two_point_lower_bound_of_tvDist_le hest hsep htv

theorem pinskerBound_of_ac_of_ne_top (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) (hfin : klDiv μ ν ≠ ⊤) : PinskerBound μ ν := by set p : Ω → ℝ := fun x => (μ.rnDeriv ν x).toReal with hp_def set K : ℝ := (klDiv μ ν).toReal with hK_def set g : Ω → ℝ := fun x => (p x - 1) ^ 2 / (p x + 2) with hg_def set f₁ : Ω → ℝ := fun x => |p x - 1| / sqrt (p x + 2) with hf₁_def set f₂ : Ω → ℝ := fun x => sqrt (p x + 2) with hf₂_def have hp_nonneg : ∀ x, 0 ≤ p x := by intro x rw [hp_def] exact ENNReal.toReal_nonneg have hK_nonneg : 0 ≤ K := by rw [hK_def] exact ENNReal.toReal_nonneg have hp_int : Integrable p ν := by rw [hp_def] exact Measure.integrable_toReal_rnDeriv have hp_meas : AEStronglyMeasurable p ν := by rw [hp_def] exact (Measure.measurable_rnDeriv μ ν).ennreal_toReal.aestronglyMeasurable have hp_integral_one : ∫ x, p x ∂ν = 1 := by rw [hp_def, Measure.integral_toReal_rnDeriv hac] rw [measureReal_def, measure_univ] simp have hllr_int : Integrable (llr μ ν) μ := (InformationTheory.klDiv_ne_top_iff.mp hfin).2 have hkl_int : Integrable (fun x => klFun (p x)) ν := by rw [hp_def] exact (InformationTheory.integrable_klFun_rnDeriv_iff hac).2 hllr_int have hK_eq_integral : K = ∫ x, klFun (p x) ∂ν := by rw [hK_def, hp_def] exact InformationTheory.toReal_klDiv_eq_integral_klFun hac have hg_nonneg : ∀ x, 0 ≤ g x := by intro x rw [hg_def] exact pinsker_weight_nonneg (hp_nonneg x) have hg_le : ∀ x, g x ≤ (2 / 3) * klFun (p x) := by intro x rw [hg_def] exact pinsker_weight_le_klFun (hp_nonneg x) have hg_meas : AEStronglyMeasurable g ν := by rw [hg_def] exact (by fun_prop : AEMeasurable (fun x => (p x - 1) ^ 2 / (p x + 2)) ν) |>.aestronglyMeasurable have hf₂_meas : AEStronglyMeasurable f₂ ν := by rw [hf₂_def] fun_prop have hf₁_meas : AEStronglyMeasurable f₁ ν := by rw [hf₁_def] exact (by fun_prop : AEMeasurable (fun x => |p x - 1| / sqrt (p x + 2)) ν) |>.aestronglyMeasurable have hg_int : Integrable g ν := by refine Integrable.mono' (hkl_int.const_mul (2 / 3)) hg_meas ?_ exact Filter.Eventually.of_forall fun x => by rw [Real.norm_eq_abs, abs_of_nonneg (hg_nonneg x)] exact hg_le x have hg_integral_le : ∫ x, g x ∂ν ≤ (2 / 3) * K := by have hdom_int : Integrable (fun x => (2 / 3) * klFun (p x)) ν := hkl_int.const_mul (2 / 3) have hle_int : ∫ x, g x ∂ν ≤ ∫ x, (2 / 3) * klFun (p x) ∂ν := integral_mono_ae hg_int hdom_int (Filter.Eventually.of_forall hg_le) calc ∫ x, g x ∂ν ≤ ∫ x, (2 / 3) * klFun (p x) ∂ν := hle_int _ = (2 / 3) * K := by rw [integral_const_mul, ← hK_eq_integral] have hf₁_sq_int : Integrable (fun x => f₁ x ^ 2) ν := by refine hg_int.congr (Filter.Eventually.of_forall fun x => ?_) rw [hf₁_def, hg_def] exact (pinsker_abs_div_sqrt_sq (hp_nonneg x)).symm have hf₂_sq_int : Integrable (fun x => f₂ x ^ 2) ν := by refine (hp_int.add (integrable_const 2)).congr (Filter.Eventually.of_forall fun x => ?_) rw [hf₂_def] exact (Real.sq_sqrt (by linarith [hp_nonneg x] : 0 ≤ p x + 2)).symm have hf₁L2 : MemLp f₁ (ofReal 2) ν := by simpa using (memLp_two_iff_integrable_sq hf₁_meas).2 hf₁_sq_int have hf₂L2 : MemLp f₂ (ofReal 2) ν := by simpa using (memLp_two_iff_integrable_sq hf₂_meas).2 hf₂_sq_int have hf₁_nonneg : 0 ≤ᵐ[ν] f₁ := Filter.Eventually.of_forall fun x => by rw [hf₁_def] exact div_nonneg (abs_nonneg _) (Real.sqrt_nonneg _) have hf₂_nonneg : 0 ≤ᵐ[ν] f₂ := Filter.Eventually.of_forall fun x => by rw [hf₂_def] exact Real.sqrt_nonneg _ have hholder : ∫ x, f₁ x * f₂ x ∂ν ≤ (∫ x, f₁ x ^ (2 : ℝ) ∂ν) ^ (1 / (2 : ℝ)) * (∫ x, f₂ x ^ (2 : ℝ) ∂ν) ^ (1 / (2 : ℝ)) := integral_mul_le_Lp_mul_Lq_of_nonneg Real.HolderConjugate.two_two hf₁_nonneg hf₂_nonneg hf₁L2 hf₂L2 have hLHS : ∫ x, f₁ x * f₂ x ∂ν = ∫ x, |p x - 1| ∂ν := by apply integral_congr_ae exact Filter.Eventually.of_forall fun x => by rw [hf₁_def, hf₂_def] exact pinsker_abs_div_sqrt_mul_sqrt (hp_nonneg x) have hf₁_rpow : ∫ x, f₁ x ^ (2 : ℝ) ∂ν = ∫ x, g x ∂ν := by apply integral_congr_ae exact Filter.Eventually.of_forall fun x => by rw [hf₁_def, hg_def] change (|p x - 1| / √(p x + 2)) ^ (2 : ℝ) = (p x - 1) ^ 2 / (p x + 2) rw [Real.rpow_two] exact pinsker_abs_div_sqrt_sq (hp_nonneg x) have hf₂_rpow : ∫ x, f₂ x ^ (2 : ℝ) ∂ν = 3 := by have hsqrt_sq : ∫ x, f₂ x ^ (2 : ℝ) ∂ν = ∫ x, p x + 2 ∂ν := by apply integral_congr_ae exact Filter.Eventually.of_forall fun x => by rw [hf₂_def] change √(p x + 2) ^ (2 : ℝ) = p x + 2 rw [Real.rpow_two] exact Real.sq_sqrt (by linarith [hp_nonneg x] : 0 ≤ p x + 2) rw [hsqrt_sq] calc ∫ x, p x + 2 ∂ν = (∫ x, p x ∂ν) + ∫ _ : Ω, (2 : ℝ) ∂ν := integral_add hp_int (integrable_const 2) _ = 3 := by rw [hp_integral_one]; norm_num have h_int_abs : ∫ x, |p x - 1| ∂ν ≤ sqrt (2 * K) := by rw [hLHS, hf₁_rpow, hf₂_rpow] at hholder have hrpow_g : (∫ x, g x ∂ν) ^ (1 / (2 : ℝ)) = sqrt (∫ x, g x ∂ν) := (Real.sqrt_eq_rpow (∫ x, g x ∂ν)).symm have hrpow_three : (3 : ℝ) ^ (1 / (2 : ℝ)) = sqrt 3 := (Real.sqrt_eq_rpow 3).symm rw [hrpow_g, hrpow_three] at hholder have hg_int_nonneg : 0 ≤ ∫ x, g x ∂ν := integral_nonneg fun x => hg_nonneg x have hsqrt_g_le : sqrt (∫ x, g x ∂ν) ≤ sqrt ((2 / 3) * K) := Real.sqrt_le_sqrt hg_integral_le have hprod_le : sqrt (∫ x, g x ∂ν) * sqrt 3 ≤ sqrt ((2 / 3) * K) * sqrt 3 := by exact mul_le_mul_of_nonneg_right hsqrt_g_le (Real.sqrt_nonneg 3) calc ∫ x, |p x - 1| ∂ν ≤ sqrt (∫ x, g x ∂ν) * sqrt 3 := hholder _ ≤ sqrt ((2 / 3) * K) * sqrt 3 := hprod_le _ = sqrt (2 * K) := by rw [← Real.sqrt_mul (by positivity : 0 ≤ (2 / 3) * K) (3 : ℝ)] congr 1 ring have hscheffe := tvDist_le_half_integral_abs_rnDeriv μ ν hac unfold PinskerBound have hscheffe_p : tvDist μ ν ≤ (1 / 2) * ∫ x, |p x - 1| ∂ν := by simpa [hp_def] using hscheffe calc tvDist μ ν ≤ (1 / 2) * ∫ x, |p x - 1| ∂ν := hscheffe_p _ ≤ (1 / 2) * sqrt (2 * K) := by exact mul_le_mul_of_nonneg_left h_int_abs (by norm_num) _ = sqrt (K / 2) := pinsker_half_sqrt_two_mul K hK_nonneg _ = sqrt ((klDiv μ ν).toReal / 2) := by rw [hK_def]

theorem pinskerBound_pi_iid {α : Type*} [MeasurableSpace α] (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) (hint : Integrable (llr μ ν) μ) (n : ℕ) : PinskerBound (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν)) := by have hac_pi := pi_iid_absolutelyContinuous μ ν hac n have hint_pi := pi_iid_llr_integrable μ ν hac hint n exact pinskerBound_of_ac_of_ne_top _ _ hac_pi (InformationTheory.klDiv_ne_top hac_pi hint_pi)

theorem klForm_two_point_lower_bound_of_pinsker (h : PinskerBound P₀ P₁) {est : Ω → Θ} (hest : Measurable est) {θ₀ θ₁ : Θ} {s : ℝ} (hsep : 2 * s ≤ dist θ₀ θ₁) : (1 - sqrt ((klDiv P₀ P₁).toReal / 2)) / 2 ≤ max (P₀.real {ω | s ≤ dist (est ω) θ₀}) (P₁.real {ω | s ≤ dist (est ω) θ₁}) := by have hmax := half_one_sub_tvDist_le_max_error (P₀ := P₀) (P₁ := P₁) hest hsep have htv : (1 - sqrt ((klDiv P₀ P₁).toReal / 2)) / 2 ≤ (1 - tvDist P₀ P₁) / 2 := by have := h unfold PinskerBound at this linarith exact htv.trans hmax

theorem klForm_two_point_lower_bound (hac : P₀ ≪ P₁) (hfin : klDiv P₀ P₁ ≠ ⊤) {est : Ω → Θ} (hest : Measurable est) {θ₀ θ₁ : Θ} {s : ℝ} (hsep : 2 * s ≤ dist θ₀ θ₁) : (1 - sqrt ((klDiv P₀ P₁).toReal / 2)) / 2 ≤ max (P₀.real {ω | s ≤ dist (est ω) θ₀}) (P₁.real {ω | s ≤ dist (est ω) θ₁}) := klForm_two_point_lower_bound_of_pinsker (pinskerBound_of_ac_of_ne_top P₀ P₁ hac hfin) hest hsep

theorem bretagnolle_huber_affinity (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) (hfin : klDiv μ ν ≠ ⊤) : (1 / 2 : ℝ) * exp (-(klDiv μ ν).toReal) ≤ 1 - tvDist μ ν := by set K : ℝ := (klDiv μ ν).toReal with hK_def set ρ : ℝ := ∫ x, sqrt ((μ.rnDeriv ν x).toReal) ∂ν with hρ_def have hint : Integrable (llr μ ν) μ := (klDiv_ne_top_iff.mp hfin).2 have hρ_nonneg : 0 ≤ ρ := by rw [hρ_def]; exact integral_nonneg fun x => Real.sqrt_nonneg _ have hL3 : exp (-(1 / 2) * K) ≤ ρ := exp_neg_half_klDiv_le_bhattacharyya μ ν hac hint -- square it: exp(-K) ≤ ρ² have hexp_sq : exp (-K) = exp (-(1 / 2) * K) ^ 2 := by have hsum : -K = -(1 / 2) * K + -(1 / 2) * K := by ring rw [sq, ← Real.exp_add, ← hsum] have hsq : exp (-K) ≤ ρ ^ 2 := by rw [hexp_sq] nlinarith [hL3, Real.exp_nonneg (-(1 / 2) * K), hρ_nonneg] -- Cauchy–Schwarz + affinity have hL2 : ρ ^ 2 ≤ 2 * ∫ x, min ((μ.rnDeriv ν x).toReal) 1 ∂ν := by rw [hρ_def]; exact sq_bhattacharyya_le_two_mul_integral_min μ ν hac have hL1 : ∫ x, min ((μ.rnDeriv ν x).toReal) 1 ∂ν ≤ 1 - tvDist μ ν := integral_min_le_one_sub_tvDist μ ν hac rw [hK_def] linarith [hsq, hL2, hL1]

theorem finite_one_add_chiSqDiv {Ω : Type*} [MeasurableSpace Ω] [Fintype Ω] [MeasurableSingletonClass Ω] (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) : 1 + chiSqDiv μ ν = ∑ x, (μ.real {x}) ^ 2 / (ν.real {x}) := by have hexp : 1 + chiSqDiv μ ν = ∫ x, ((μ.rnDeriv ν x).toReal) ^ 2 ∂ν := by rw [chiSqDiv_eq hac (Integrable.of_finite)]; ring rw [hexp, integral_fintype (Integrable.of_finite)] apply Finset.sum_congr rfl intro x _ by_cases h : ν {x} = 0 · -- `ν {x} = 0` forces `μ {x} = 0` (absolute continuity); both sides vanish. have hνr : ν.real {x} = 0 := by rw [measureReal_def, h, ENNReal.toReal_zero] have hμr : μ.real {x} = 0 := by rw [measureReal_def, hac h, ENNReal.toReal_zero] rw [hνr, hμr]; simp · have hνtop : ν {x} ≠ ⊤ := measure_ne_top ν {x} have hνr0 : ν.real {x} ≠ 0 := by rw [measureReal_def]; exact ENNReal.toReal_ne_zero.2 ⟨h, hνtop⟩ -- Invert the density on the atom `{x}` via the discrete RN bridge. have hrn : (μ.rnDeriv ν x).toReal = μ.real {x} / ν.real {x} := by have hc := congrArg toReal (rnDeriv_mul_measure_singleton μ ν hac x) rw [ENNReal.toReal_mul, ← measureReal_def, ← measureReal_def] at hc rw [eq_div_iff hνr0, mul_comm, hc] rw [hrn, smul_eq_mul] field_simp

lemma coordinatewise_overlap_direct_product {M : ℕ} (hM : 1 ≤ M) {Z S : Fin M → Type*} {A : Type*} [∀ j, MeasurableSpace (Z j)] [∀ j, StandardBorelSpace (Z j)] [∀ j, MeasurableSpace (S j)] [∀ j, StandardBorelSpace (S j)] [MeasurableSpace A] [StandardBorelSpace A] (Q : ∀ j, Bool → Measure (Z j)) (R : Measure A) [∀ j b, IsProbabilityMeasure (Q j b)] [IsProbabilityMeasure R] (compress : ∀ j, Z j → S j) (hcompress : ∀ j, Measurable (compress j)) (decoder : ∀ j, S j → ((k : Fin M) → Z k) → A → Bool) (hdecoder : ∀ j, Measurable (fun p : S j × ((k : Fin M) → Z k) × A => decoder j p.1 p.2.1 p.2.2)) (hlocal : ∀ j s z z' a, (∀ k, k ≠ j → z k = z' k) → decoder j s z a = decoder j s z' a) : coordinatewiseSuccessProbability Q R compress decoder ≤ ofReal ((1 / 2 : ℝ) * (1 + ∏ j, (1 - coordinateOverlap Q compress j))) ∧ ∀ κ : ℝ, κ < 1 → (∀ j, klDiv (compressedCoordinateLaw (compress j) (Q j false)) (compressedCoordinateLaw (compress j) (Q j true)) ≤ ofReal (κ * log M)) → ofReal ((1 / 2 : ℝ) * (1 - exp (-((M : ℝ) ^ (1 - κ)) / 2))) ≤ 1 - coordinatewiseSuccessProbability Q R compress decoder := by letI mapProb (j : Fin M) (b : Bool) : IsProbabilityMeasure (compressedCoordinateLaw (compress j) (Q j b)) := Measure.isProbabilityMeasure_map (hcompress j).aemeasurable have hmain : coordinatewiseSuccessProbability Q R compress decoder ≤ ofReal ((1 / 2 : ℝ) * (1 + ∏ j, (1 - coordinateOverlap Q compress j))) := by classical let gamma : ∀ j, Measure (Z j × Z j) := fun j => compressionCoupling (Q j false) (Q j true) (compress j) (hcompress j) let Gamma : Measure ((j : Fin M) → Z j × Z j) := Measure.pi gamma let selected (omega : Fin M → Bool) : ((j : Fin M) → Z j × Z j) → ((j : Fin M) → Z j) := fun z => selectCoupledRaw omega z have hcoord (omega : Fin M → Bool) (j : Fin M) : MeasurePreserving (fun p : Z j × Z j => if omega j then p.2 else p.1) (gamma j) (Q j (omega j)) := by cases hbit : omega j · constructor · simpa [hbit] using (measurable_fst : Measurable (Prod.fst : Z j × Z j → Z j)) · simpa [gamma, hbit] using compressionCoupling_map_fst (Q j false) (Q j true) (compress j) (hcompress j) · constructor · simpa [hbit] using (measurable_snd : Measurable (Prod.snd : Z j × Z j → Z j)) · simpa [gamma, hbit] using compressionCoupling_map_snd (Q j false) (Q j true) (compress j) (hcompress j) have hselected (omega : Fin M → Bool) : MeasurePreserving (selected omega) Gamma (Measure.pi fun j => Q j (omega j)) := by exact measurePreserving_pi gamma (fun j => Q j (omega j)) (hcoord omega) have htargetMeas (omega : Fin M → Bool) : MeasurableSet {data : A × ((j : Fin M) → Z j) | ∀ j, decoder j (compress j (data.2 j)) data.2 data.1 = omega j} := by rw [show {data : A × ((j : Fin M) → Z j) | ∀ j, decoder j (compress j (data.2 j)) data.2 data.1 = omega j} = ⋂ j, {data | decoder j (compress j (data.2 j)) data.2 data.1 = omega j} by ext data; simp] apply MeasurableSet.iInter intro j apply measurableSet_eq_fun _ measurable_const have hm := (hdecoder j).comp (((hcompress j).comp ((measurable_pi_apply j).comp measurable_snd)).prodMk (measurable_snd.prodMk measurable_fst)) simpa only [Function.comp_def] using hm have hmeasure (omega : Fin M → Bool) : (R.prod (Measure.pi fun j => Q j (omega j))) {data | ∀ j, decoder j (compress j (data.2 j)) data.2 data.1 = omega j} = (R.prod Gamma) {data | coupledDecoderGood compress decoder omega data.2 data.1} := by let mp := (MeasurePreserving.id R).prod (hselected omega) have happ := Measure.map_apply (μ := R.prod Gamma) mp.measurable (htargetMeas omega) rw [mp.map_eq] at happ rw [happ] congr 1 have hsourceMeas (omega : Fin M → Bool) : MeasurableSet {data : A × ((j : Fin M) → Z j × Z j) | coupledDecoderGood compress decoder omega data.2 data.1} := by exact (htargetMeas omega).preimage (measurable_id.prodMap (hselected omega).measurable) have hindMeas (omega : Fin M → Bool) : Measurable (fun data : A × ((j : Fin M) → Z j × Z j) => coupledGoodIndicator compress decoder omega data.2 data.1) := by let E : Set (A × ((j : Fin M) → Z j × Z j)) := {data | coupledDecoderGood compress decoder omega data.2 data.1} rw [show (fun data : A × ((j : Fin M) → Z j × Z j) => coupledGoodIndicator compress decoder omega data.2 data.1) = E.indicator (fun _ => (1 : ℝ≥0∞)) by funext data by_cases hgood : coupledDecoderGood compress decoder omega data.2 data.1 <;> simp [coupledGoodIndicator, E, hgood]] exact measurable_const.indicator (hsourceMeas omega) have hindicator (omega : Fin M → Bool) : ∫⁻ data, coupledGoodIndicator compress decoder omega data.2 data.1 ∂(R.prod Gamma) = (R.prod Gamma) {data | coupledDecoderGood compress decoder omega data.2 data.1} := by let E : Set (A × ((j : Fin M) → Z j × Z j)) := {data | coupledDecoderGood compress decoder omega data.2 data.1} have hE : MeasurableSet E := hsourceMeas omega rw [← setLIntegral_one E] rw [← lintegral_indicator hE] apply lintegral_congr intro data by_cases hgood : coupledDecoderGood compress decoder omega data.2 data.1 <;> simp [coupledGoodIndicator, E, hgood] let N : Set ((j : Fin M) → Z j × Z j) := {z | ∀ j, compress j (z j).1 ≠ compress j (z j).2} have hNj (j : Fin M) : MeasurableSet {p : Z j × Z j | compress j p.1 ≠ compress j p.2} := by letI : MeasurableEq (S j) := measurableEqOfStandardBorel (S j) exact (measurableSet_eq_fun ((hcompress j).comp measurable_fst) ((hcompress j).comp measurable_snd)).compl have hN : MeasurableSet N := by rw [show N = Set.univ.pi fun j => {p : Z j × Z j | compress j p.1 ≠ compress j p.2} by ext z; simp [N]] exact MeasurableSet.univ_pi hNj have hgammaN (j : Fin M) : gamma j {p : Z j × Z j | compress j p.1 ≠ compress j p.2} ≤ ofReal (tvDist (compressedCoordinateLaw (compress j) (Q j false)) (compressedCoordinateLaw (compress j) (Q j true))) := by have heq := compressionCoupling_equal_compression_mass_ge (Q j false) (Q j true) (compress j) (hcompress j) have hEqMeas : MeasurableSet {p : Z j × Z j | compress j p.1 = compress j p.2} := by letI : MeasurableEq (S j) := measurableEqOfStandardBorel (S j) exact measurableSet_eq_fun ((hcompress j).comp measurable_fst) ((hcompress j).comp measurable_snd) have hcompl := tsub_le_tsub_left heq 1 rw [show {p : Z j × Z j | compress j p.1 ≠ compress j p.2} = {p : Z j × Z j | compress j p.1 = compress j p.2}ᶜ by ext; simp, measure_compl hEqMeas (measure_ne_top (gamma j) _), measure_univ] calc 1 - gamma j {p : Z j × Z j | compress j p.1 = compress j p.2} ≤ 1 - ofReal (1 - tvDist (compressedCoordinateLaw (compress j) (Q j false)) (compressedCoordinateLaw (compress j) (Q j true))) := by simpa [gamma, compressedCoordinateLaw] using hcompl _ = ofReal (tvDist (compressedCoordinateLaw (compress j) (Q j false)) (compressedCoordinateLaw (compress j) (Q j true))) := by rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_sub (1 : ℝ) (by exact sub_nonneg.mpr tvDist_le_one)] congr 1 ring have hGammaN : Gamma N ≤ ofReal (∏ j, tvDist (compressedCoordinateLaw (compress j) (Q j false)) (compressedCoordinateLaw (compress j) (Q j true))) := by change (Measure.pi gamma) N ≤ _ rw [show N = Set.univ.pi fun j => {p : Z j × Z j | compress j p.1 ≠ compress j p.2} by ext z; simp [N], Measure.pi_pi] calc (∏ j, gamma j {p : Z j × Z j | compress j p.1 ≠ compress j p.2}) ≤ ∏ j, ofReal (tvDist (compressedCoordinateLaw (compress j) (Q j false)) (compressedCoordinateLaw (compress j) (Q j true))) := Finset.prod_le_prod (fun _ _ => bot_le) (fun j _ => hgammaN j) _ = _ := by rw [ENNReal.ofReal_prod_of_nonneg] exact fun j _ => tvDist_nonneg have hpoint (data : A × ((j : Fin M) → Z j × Z j)) : (∑ omega : Fin M → Bool, coupledGoodIndicator compress decoder omega data.2 data.1) ≤ (2 : ℝ≥0∞) ^ M / 2 * (1 + N.indicator (fun _ => (1 : ℝ≥0∞)) data.2) := by by_cases hz : data.2 ∈ N · have htriv : (∑ omega : Fin M → Bool, coupledGoodIndicator compress decoder omega data.2 data.1) ≤ (2 : ℝ≥0∞) ^ M := by calc _ ≤ ∑ _omega : Fin M → Bool, (1 : ℝ≥0∞) := Finset.sum_le_sum fun omega _ => by by_cases hg : coupledDecoderGood compress decoder omega data.2 data.1 <;> simp [coupledGoodIndicator, hg] _ = _ := by simp have hcancel : (2 : ℝ≥0∞) ^ M / 2 * (1 + 1) = (2 : ℝ≥0∞) ^ M := by rw [one_add_one_eq_two, ENNReal.div_mul_cancel (by norm_num) (by norm_num)] simpa [Set.indicator_of_mem hz, hcancel] using htriv · have hz' : ¬ ∀ j, compress j (data.2 j).1 ≠ compress j (data.2 j).2 := by simpa [N] using hz push_neg at hz' obtain ⟨j, hj⟩ := hz' have hhalf := coupledDecoderGood_count_le_half compress decoder hlocal data.2 data.1 j hj simpa [indicator, hz] using hhalf have hsumMeasure : (∑ omega : Fin M → Bool, (R.prod (Measure.pi fun j => Q j (omega j))) {data | ∀ j, decoder j (compress j (data.2 j)) data.2 data.1 = omega j}) ≤ (2 : ℝ≥0∞) ^ M / 2 * (1 + Gamma N) := by have hIndIntegral : (∫⁻ data : A × ((j : Fin M) → Z j × Z j), N.indicator (fun _ => (1 : ℝ≥0∞)) data.2 ∂(R.prod Gamma)) = Gamma N := by rw [show (fun data : A × ((j : Fin M) → Z j × Z j) => N.indicator (fun _ => (1 : ℝ≥0∞)) data.2) = (univ ×ˢ N).indicator (fun _ => (1 : ℝ≥0∞)) by funext data by_cases hz : data.2 ∈ N <;> simp [indicator, hz]] rw [lintegral_indicator_const (MeasurableSet.univ.prod hN)] rw [Measure.prod_apply (MeasurableSet.univ.prod hN)] simp simp_rw [hmeasure, ← hindicator] rw [← lintegral_finset_sum univ (fun omega _ => hindMeas omega)] calc _ ≤ ∫⁻ data, (2 : ℝ≥0∞) ^ M / 2 * (1 + N.indicator (fun _ => (1 : ℝ≥0∞)) data.2) ∂(R.prod Gamma) := lintegral_mono hpoint _ = (2 : ℝ≥0∞) ^ M / 2 * (1 + Gamma N) := by rw [lintegral_const_mul] · rw [lintegral_add_left measurable_const] rw [lintegral_const, measure_univ, hIndIntegral] simp · exact measurable_const.fun_add ((measurable_const.indicator hN).comp measurable_snd) unfold coordinatewiseSuccessProbability have hprodReal : 0 ≤ ∏ j, tvDist (compressedCoordinateLaw (compress j) (Q j false)) (compressedCoordinateLaw (compress j) (Q j true)) := Finset.prod_nonneg fun j _ => tvDist_nonneg calc _ ≤ ((2 : ℝ≥0∞) ^ M / 2 * (1 + Gamma N)) / (2 : ℝ≥0∞) ^ M := ENNReal.div_le_div_right hsumMeasure _ -- … truncated; follow the source link for the rest …

theorem fano_average_error {est : Ω → Θ} (hest : Measurable est) {θ : ι → Θ} {s : ℝ} (hsep : ∀ i k, i ≠ k → 2 * s ≤ dist (θ i) (θ k)) (i₀ : ι) : 1 - (1 + ∑ i, tvDist (P i₀) (P i)) / (Fintype.card ι) ≤ (∑ i, (P i).real {ω | s ≤ dist (est ω) (θ i)}) / (Fintype.card ι) := by set N : ℝ := (Fintype.card ι : ℝ) with hN have hNpos : 0 < N := by rw [hN, Nat.cast_pos] exact Fintype.card_pos_iff.mpr ⟨i₀⟩ have hNne : N ≠ 0 := ne_of_gt hNpos have herr : ∀ i, (P i).real {ω | s ≤ dist (est ω) (θ i)} = 1 - (P i).real (acceptanceRegion est (θ i) s) := by intro i rw [← acceptanceRegion_compl est (θ i) s, measureReal_compl (measurableSet_acceptanceRegion hest (θ i) s)] simp [probReal_univ] have hsumerr : ∑ i, (P i).real {ω | s ≤ dist (est ω) (θ i)} = N - ∑ i, (P i).real (acceptanceRegion est (θ i) s) := by simp_rw [herr] rw [Finset.sum_sub_distrib] congr 1 rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one, hN] have hcorrect := sum_correct_le P hest hsep i₀ rw [hsumerr, le_div_iff₀ hNpos, sub_mul, div_mul_cancel₀ _ hNne, one_mul] linarith [hcorrect]

theorem fano_exists_error {est : Ω → Θ} (hest : Measurable est) {θ : ι → Θ} {s : ℝ} (hsep : ∀ i k, i ≠ k → 2 * s ≤ dist (θ i) (θ k)) (i₀ : ι) {β : ℝ} (hβ : ∀ i, tvDist (P i₀) (P i) ≤ β) : ∃ i, 1 - 1 / (Fintype.card ι) - β ≤ (P i).real {ω | s ≤ dist (est ω) (θ i)} := by set N : ℝ := (Fintype.card ι : ℝ) with hN have hNpos : 0 < N := by rw [hN, Nat.cast_pos]; exact Fintype.card_pos_iff.mpr ⟨i₀⟩ have havg := fano_average_error P hest hsep i₀ rw [← hN] at havg have hsumtv : ∑ i, tvDist (P i₀) (P i) ≤ N * β := by calc ∑ i, tvDist (P i₀) (P i) ≤ ∑ _i : ι, β := Finset.sum_le_sum (fun i _ => hβ i) _ = N * β := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, hN] have hstep : (1 + ∑ i, tvDist (P i₀) (P i)) / N ≤ 1 / N + β := by rw [add_div] have hle : (∑ i, tvDist (P i₀) (P i)) / N ≤ β := by rw [div_le_iff₀ hNpos]; linarith [hsumtv] linarith have hbound : 1 - 1 / N - β ≤ (∑ i, (P i).real {ω | s ≤ dist (est ω) (θ i)}) / N := by refine le_trans ?_ havg linarith [hstep] by_contra hcon push_neg at hcon have hstrict : ∑ i, (P i).real {ω | s ≤ dist (est ω) (θ i)} < N * (1 - 1 / N - β) := by calc ∑ i, (P i).real {ω | s ≤ dist (est ω) (θ i)} < ∑ _i : ι, (1 - 1 / N - β) := Finset.sum_lt_sum_of_nonempty (Finset.univ_nonempty_iff.mpr ⟨i₀⟩) (fun i _ => hcon i) _ = N * (1 - 1 / N - β) := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, hN] rw [le_div_iff₀ hNpos] at hbound nlinarith [hbound, hstrict]

lemma tvDist_le_sqrt_two_mul_one_sub_affinity {α : Type*} [MeasurableSpace α] (μ : Measure α) (f g : α → ℝ) (hf : Integrable f μ) (hg : Integrable g μ) (hf0 : 0 ≤ f) (hg0 : 0 ≤ g) (hf1 : ∫ x, f x ∂μ = 1) (hg1 : ∫ x, g x ∂μ = 1) : tvDist (μ.withDensity (fun x => ofReal (f x))) (μ.withDensity (fun x => ofReal (g x))) ≤ sqrt (2 * (1 - densityAffinity μ f g)) := by let P := μ.withDensity (fun x => ofReal (f x)) let Q := μ.withDensity (fun x => ofReal (g x)) have hreal_f {A : Set α} (hA : MeasurableSet A) : P.real A = ∫ x in A, f x ∂μ := by rw [measureReal_def, withDensity_apply _ hA] rw [← MeasureTheory.ofReal_integral_eq_lintegral_ofReal hf.integrableOn] · rw [ENNReal.toReal_ofReal] exact integral_nonneg_of_ae (Filter.Eventually.of_forall fun x => hf0 x) · exact Filter.Eventually.of_forall fun x => hf0 x have hreal_g {A : Set α} (hA : MeasurableSet A) : Q.real A = ∫ x in A, g x ∂μ := by rw [measureReal_def, withDensity_apply _ hA] rw [← MeasureTheory.ofReal_integral_eq_lintegral_ofReal hg.integrableOn] · rw [ENNReal.toReal_ofReal] exact integral_nonneg_of_ae (Filter.Eventually.of_forall fun x => hg0 x) · exact Filter.Eventually.of_forall fun x => hg0 x have hfg : Integrable (fun x => f x - g x) μ := hf.sub hg have hfg0 : ∫ x, (f x - g x) ∂μ = 0 := by rw [integral_sub hf hg, hf1, hg1] ring have htv : tvDist P Q ≤ (1 / 2 : ℝ) * ∫ x, |f x - g x| ∂μ := by unfold tvDist refine ciSup_le fun A => ?_ rw [hreal_f A.2, hreal_g A.2, ← integral_sub hf.integrableOn hg.integrableOn] exact abs_setIntegral_le_half_integral_abs_of_integral_eq_zero hfg hfg0 A.2 have hsf_asm : AEStronglyMeasurable (fun x => sqrt (f x)) μ := (Real.continuous_sqrt.measurable.comp_aemeasurable hf.aestronglyMeasurable.aemeasurable).aestronglyMeasurable have hsg_asm : AEStronglyMeasurable (fun x => sqrt (g x)) μ := (Real.continuous_sqrt.measurable.comp_aemeasurable hg.aestronglyMeasurable.aemeasurable).aestronglyMeasurable have hsf : MemLp (fun x => sqrt (f x)) 2 μ := by rw [memLp_two_iff_integrable_sq hsf_asm] convert hf using 1 funext x exact Real.sq_sqrt (hf0 x) have hsg : MemLp (fun x => sqrt (g x)) 2 μ := by rw [memLp_two_iff_integrable_sq hsg_asm] convert hg using 1 funext x exact Real.sq_sqrt (hg0 x) let u : α → ℝ := fun x => sqrt (f x) - sqrt (g x) let v : α → ℝ := fun x => sqrt (f x) + sqrt (g x) have hu : MemLp u 2 μ := hsf.sub hsg have hv : MemLp v 2 μ := hsf.add hsg have hfact : ∀ x, |f x - g x| = |u x| * |v x| := by intro x rw [← abs_mul] dsimp [u, v] rw [show (sqrt (f x) - sqrt (g x)) * (sqrt (f x) + sqrt (g x)) = sqrt (f x) ^ 2 - sqrt (g x) ^ 2 by ring] simp only [Real.sq_sqrt (hf0 x), Real.sq_sqrt (hg0 x)] have hholder : ∫ x, |u x| * |v x| ∂μ ≤ (∫ x, |u x| ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) * (∫ x, |v x| ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) := by apply integral_mul_le_Lp_mul_Lq_of_nonneg (p := (2 : ℝ)) (q := (2 : ℝ)) · exact Real.HolderConjugate.two_two · exact Filter.Eventually.of_forall fun x => abs_nonneg _ · exact Filter.Eventually.of_forall fun x => abs_nonneg _ · rw [show (ofReal 2 : ℝ≥0∞) = 2 from by norm_num] exact hu.abs · rw [show (ofReal 2 : ℝ≥0∞) = 2 from by norm_num] exact hv.abs have hsfg : Integrable (fun x => sqrt (f x) * sqrt (g x)) μ := hsf.integrable_mul hsg have hu_sq : ∫ x, |u x| ^ (2 : ℝ) ∂μ = 2 * (1 - densityAffinity μ f g) := by simp_rw [Real.rpow_two, sq_abs] have hpoint : (fun x => u x ^ 2) = (fun x => f x + g x - 2 * sqrt (f x * g x)) := by funext x dsimp [u] rw [show sqrt (f x * g x) = sqrt (f x) * sqrt (g x) by rw [Real.sqrt_mul (hf0 x)]] nlinarith [Real.sq_sqrt (hf0 x), Real.sq_sqrt (hg0 x)] rw [hpoint] have hsqrtfg : Integrable (fun x => sqrt (f x * g x)) μ := by convert hsfg using 1 funext x rw [Real.sqrt_mul (hf0 x)] change ∫ x, (f + g) x - (2 * (fun x => sqrt (f x * g x)) x) ∂μ = 2 * (1 - densityAffinity μ f g) rw [integral_sub (hf.add hg) (hsqrtfg.const_mul 2)] change (∫ x, f x + g x ∂μ) - ∫ x, 2 * sqrt (f x * g x) ∂μ = 2 * (1 - densityAffinity μ f g) rw [integral_add hf hg, integral_const_mul, hf1, hg1] simp [densityAffinity] ring have hv_sq_plain : ∫ x, v x ^ 2 ∂μ ≤ 4 := by calc ∫ x, v x ^ 2 ∂μ ≤ ∫ x, (2 * f x + 2 * g x) ∂μ := by apply integral_mono_ae hv.integrable_sq ((hf.const_mul 2).add (hg.const_mul 2)) exact Filter.Eventually.of_forall fun x => by dsimp [v] have hsf0 := Real.sqrt_nonneg (f x) have hsg0 := Real.sqrt_nonneg (g x) nlinarith [Real.sq_sqrt (hf0 x), Real.sq_sqrt (hg0 x), sq_nonneg (sqrt (f x) - sqrt (g x))] _ = 4 := by rw [integral_add (hf.const_mul 2) (hg.const_mul 2), integral_const_mul, integral_const_mul, hf1, hg1] ring have hv_sq : ∫ x, |v x| ^ (2 : ℝ) ∂μ ≤ 4 := by simpa [Real.rpow_two, sq_abs] using hv_sq_plain have hu_sq_nonneg : 0 ≤ 2 * (1 - densityAffinity μ f g) := by rw [← hu_sq] exact integral_nonneg_of_ae (Filter.Eventually.of_forall fun x => by positivity) exact htv.trans (by rw [show (fun x => |f x - g x|) = (fun x => |u x| * |v x|) by funext x; exact hfact x] calc (1 / 2 : ℝ) * ∫ x, |u x| * |v x| ∂μ ≤ (1 / 2 : ℝ) * ((∫ x, |u x| ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) * (∫ x, |v x| ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ))) := by gcongr _ ≤ sqrt (2 * (1 - densityAffinity μ f g)) := by rw [hu_sq, ← Real.sqrt_eq_rpow] have hv_sq_nonneg : 0 ≤ ∫ x, |v x| ^ (2 : ℝ) ∂μ := integral_nonneg_of_ae (Filter.Eventually.of_forall fun x => by positivity) rw [← Real.sqrt_eq_rpow] have hsqrtv : sqrt (∫ x, |v x| ^ (2 : ℝ) ∂μ) ≤ 2 := by rw [Real.sqrt_le_iff] norm_num simpa [Real.rpow_two, sq_abs] using hv_sq nlinarith [Real.sqrt_nonneg (2 * (1 - densityAffinity μ f g))])

theorem coverage_tv_expectedRestrictedVolume_lower {Ω : Type*} [MeasurableSpace Ω] (Q : ℝ → Measure Ω) (C : Ω → Set ℝ) (region I : Set ℝ) (reference coverage tv : ℝ) (hQ : ∀ u, IsProbabilityMeasure (Q u)) (hcover : ∀ u ∈ I, coverage ≤ (Q u {ω | u ∈ C ω}).toReal) (htv : ∀ u ∈ I, tvDist (Q u) (Q reference) ≤ tv) (hgraph : MeasurableSet {p : Ω × ℝ | p.2 ∈ C p.1}) (hregion : MeasurableSet region) (hregionFinite : volume region ≠ ⊤) (hI : MeasurableSet I) (hI_sub : I ⊆ region) : (volume I).toReal * (coverage - tv) ≤ ∫ ω, restrictedSetVolume region (C ω) ∂Q reference := by letI : IsProbabilityMeasure (Q reference) := hQ reference have hpoint : ∀ u ∈ I, coverage - tv ≤ (Q reference {ω | u ∈ C ω}).toReal := by intro u hu letI : IsProbabilityMeasure (Q u) := hQ u have hE : MeasurableSet {ω | u ∈ C ω} := hgraph.preimage (measurable_id.prodMk measurable_const) have hgap := measureReal_sub_le_tvDist (μ := Q reference) (ν := Q u) hE change (Q u {ω | u ∈ C ω}).toReal - (Q reference {ω | u ∈ C ω}).toReal ≤ tvDist (Q reference) (Q u) at hgap rw [tvDist_symm] at hgap linarith [hcover u hu, htv u hu] rw [expected_restrictedSetVolume_eq_integral_inclusion (Q := Q reference) C region hgraph hregion hregionFinite] have hmeas : Measurable fun u => (Q reference {ω | u ∈ C ω}).toReal := Measurable.ennreal_toReal (measurable_measure_prodMk_right hgraph) have hIfinite : volume I ≠ ⊤ := ne_top_of_le_ne_top hregionFinite (measure_mono hI_sub) have hrhsint : IntegrableOn (fun u => (Q reference {ω | u ∈ C ω}).toReal) I := by letI : IsFiniteMeasure (volume.restrict I) := isFiniteMeasure_restrict.mpr hIfinite exact Integrable.of_bound hmeas.aestronglyMeasurable.restrict 1 (Filter.Eventually.of_forall fun u => by rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg] simpa only [← measureReal_def] using (measureReal_le_one (μ := Q reference) (s := {ω | u ∈ C ω}))) have hrhsRegion : IntegrableOn (fun u => (Q reference {ω | u ∈ C ω}).toReal) region := by letI : IsFiniteMeasure (volume.restrict region) := isFiniteMeasure_restrict.mpr hregionFinite exact Integrable.of_bound hmeas.aestronglyMeasurable.restrict 1 (Filter.Eventually.of_forall fun u => by rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg] simpa only [← measureReal_def] using (measureReal_le_one (μ := Q reference) (s := {ω | u ∈ C ω}))) calc (volume I).toReal * (coverage - tv) = ∫ _u in I, coverage - tv := by rw [setIntegral_const] simp [measureReal_def] _ ≤ ∫ u in I, (Q reference {ω | u ∈ C ω}).toReal := setIntegral_mono_on (integrableOn_const hIfinite) hrhsint hI hpoint _ ≤ ∫ u in region, (Q reference {ω | u ∈ C ω}).toReal := setIntegral_mono_set hrhsRegion (Filter.Eventually.of_forall fun _ => ENNReal.toReal_nonneg) (Filter.Eventually.of_forall hI_sub)