Mathlib.Probability.Kernel.Three­Bernoulli.Selected­Law­KL

theorem bernoulliKL_le_inv_margin_sq {η p q : ℝ} (hη0 : 0 < η) (hp : p ∈ Icc η (1 - η)) (hq : q ∈ Icc η (1 - η)) : bernoulliKL p q ≤ (p - q) ^ 2 / η ^ 2 := by have hp0 : 0 < p := lt_of_lt_of_le hη0 hp.1 have hp1 : 0 < 1 - p := by linarith [hp.2] have hq0 : 0 < q := lt_of_lt_of_le hη0 hq.1 have hq1 : 0 < 1 - q := by linarith [hq.2] have hlog₁ := Real.log_le_sub_one_of_pos (div_pos hp0 hq0) have hlog₂ := Real.log_le_sub_one_of_pos (div_pos hp1 hq1) have hden : η ^ 2 ≤ q * (1 - q) := by calc η ^ 2 = η * η := by ring _ ≤ q * (1 - q) := mul_le_mul hq.1 (by linarith [hq.2]) hη0.le hq0.le have hqden : 0 < q * (1 - q) := mul_pos hq0 hq1 have hηden : 0 < η ^ 2 := sq_pos_of_pos hη0 unfold bernoulliKL calc p * log (p / q) + (1 - p) * log ((1 - p) / (1 - q)) ≤ p * (p / q - 1) + (1 - p) * ((1 - p) / (1 - q) - 1) := add_le_add (mul_le_mul_of_nonneg_left hlog₁ hp0.le) (mul_le_mul_of_nonneg_left hlog₂ hp1.le) _ = (p - q) ^ 2 / (q * (1 - q)) := by field_simp ring _ ≤ (p - q) ^ 2 / η ^ 2 := by exact div_le_div_of_nonneg_left (sq_nonneg _) hηden hden

theorem bernoulliKL_symmetric_le_four {t : ℝ} (ht : |t| ≤ 1 / 32) : bernoulliKL (1 / 2 + t) (1 / 2 - t) ≤ 4 * ((1 / 2 + t) - (1 / 2 - t)) ^ 2 := by have htlo : -(1 / 32 : ℝ) ≤ t := (abs_le.mp ht).1 have hthi : t ≤ (1 / 32 : ℝ) := (abs_le.mp ht).2 unfold bernoulliKL exact bernoulli_kl_le_four_sq_sub_of_mem_quarter_band (by linarith) (by linarith) (by linarith) (by linarith)

theorem selectedLaw_eq_withDensity {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ q₀' q₁' : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (hq₀' : Measurable q₀') (hq₁' : Measurable q₁') {η : ℝ} (hη0 : 0 < η) (heη : ∀ x, e x ∈ Icc η (1 - η)) (hq₀'η : ∀ x, q₀' x ∈ Icc η (1 - η)) (hq₁'η : ∀ x, q₁' x ∈ Icc η (1 - η)) : selectedLaw μ e q₀ q₁ = (selectedLaw μ e q₀' q₁').withDensity (selectedCellRatio e q₀ q₁ q₀' q₁') := by let ν : Measure ((Bool × Bool) × X) := ((Measure.count : Measure Bool).prod (Measure.count : Measure Bool)).prod μ let f : ((Bool × Bool) × X) → SelectedCoord X := fun z => (z.2, z.1) let r := selectedCellRatio e q₀ q₁ q₀' q₁' have hf : Measurable f := by fun_prop have hc (p q s : X → ℝ) (hp : Measurable p) (hq : Measurable q) (hs : Measurable s) : Measurable (fun z : SelectedCoord X => cellMass (p z.1) (q z.1) (s z.1) z.2.1 z.2.2) := by unfold cellMass bitMass apply mul · apply Measurable.ite · measurability · exact hp.comp (by fun_prop) · exact measurable_const.sub (hp.comp (by fun_prop)) · apply Measurable.ite · measurability · apply Measurable.ite · measurability · exact hs.comp (by fun_prop) · exact hq.comp (by fun_prop) · exact measurable_const.sub (by apply Measurable.ite · measurability · exact hs.comp (by fun_prop) · exact hq.comp (by fun_prop)) have hd' : Measurable (selectedDensity e q₀' q₁') := by change Measurable (fun z : (Bool × Bool) × X => ofReal (cellMass (e z.2) (q₀' z.2) (q₁' z.2) z.1.1 z.1.2)) simpa [f, Function.comp_def] using (ENNReal.measurable_ofReal.comp (hc e q₀' q₁' he hq₀' hq₁')).comp hf have hr : Measurable r := by unfold r selectedCellRatio exact ENNReal.measurable_ofReal.comp ((hc e q₀ q₁ he hq₀ hq₁).div (hc e q₀' q₁' he hq₀' hq₁')) have hmap (ν : Measure ((Bool × Bool) × X)) : (ν.map f).withDensity r = (ν.withDensity (r ∘ f)).map f := by ext S hS rw [withDensity_apply _ hS, Measure.map_apply hf hS, withDensity_apply _ (hS.preimage hf)] rw [← lintegral_indicator hS, lintegral_map (hr.indicator hS) hf, ← lintegral_indicator (hS.preimage hf)] rfl have hpos (p : ℝ) (hp : p ∈ Icc η (1 - η)) (b : Bool) : 0 < bitMass p b := by cases b with | false => change 0 < 1 - p; linarith [hp.2] | true => change 0 < p; exact lt_of_lt_of_le hη0 hp.1 have hcellpos (x : X) (a y : Bool) : 0 < cellMass (e x) (q₀' x) (q₁' x) a y := by unfold cellMass exact mul_pos (hpos (e x) (heη x) a) (by cases a with | false => exact hpos (q₀' x) (hq₀'η x) y | true => exact hpos (q₁' x) (hq₁'η x) y) have hmul : selectedDensity e q₀' q₁' * (r ∘ f) = selectedDensity e q₀ q₁ := by funext z obtain ⟨⟨a, y⟩, x⟩ := z change ofReal (cellMass (e x) (q₀' x) (q₁' x) a y) * ofReal (cellMass (e x) (q₀ x) (q₁ x) a y / cellMass (e x) (q₀' x) (q₁' x) a y) = ofReal (cellMass (e x) (q₀ x) (q₁ x) a y) rw [ENNReal.ofReal_div_of_pos (hcellpos x a y)] exact ENNReal.mul_div_cancel (by simp [hcellpos x a y]) (by simp) change (ν.withDensity (selectedDensity e q₀ q₁)).map f = ((ν.withDensity (selectedDensity e q₀' q₁')).map f).withDensity r rw [hmap, ← withDensity_mul ν hd' (hr.comp hf), hmul]

theorem selectedLaw_ac {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ q₀' q₁' : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (hq₀' : Measurable q₀') (hq₁' : Measurable q₁') {η : ℝ} (hη0 : 0 < η) (heη : ∀ x, e x ∈ Icc η (1 - η)) (hq₀'η : ∀ x, q₀' x ∈ Icc η (1 - η)) (hq₁'η : ∀ x, q₁' x ∈ Icc η (1 - η)) : selectedLaw μ e q₀ q₁ ≪ selectedLaw μ e q₀' q₁' := by rw [selectedLaw_eq_withDensity μ e q₀ q₁ q₀' q₁' he hq₀ hq₁ hq₀' hq₁' hη0 heη hq₀'η hq₁'η] exact withDensity_absolutelyContinuous _ _

theorem selectedLaw_klDiv_toReal_le_integral_sq {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ q₀' q₁' : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (hq₀' : Measurable q₀') (hq₁' : Measurable q₁') {η : ℝ} (hη0 : 0 < η) (heη : ∀ x, e x ∈ Icc η (1 - η)) (hq₀η : ∀ x, q₀ x ∈ Icc η (1 - η)) (hq₁η : ∀ x, q₁ x ∈ Icc η (1 - η)) (hq₀'η : ∀ x, q₀' x ∈ Icc η (1 - η)) (hq₁'η : ∀ x, q₁' x ∈ Icc η (1 - η)) : (klDiv (selectedLaw μ e q₀ q₁) (selectedLaw μ e q₀' q₁')).toReal ≤ ∫ x, (1 - e x) * ((q₀ x - q₀' x) ^ 2 / η ^ 2) + e x * ((q₁ x - q₁' x) ^ 2 / η ^ 2) ∂μ := by have hηsq : 0 < η ^ 2 := sq_pos_of_pos hη0 have hbound (p q : X → ℝ) (hp : ∀ x, p x ∈ Icc η (1 - η)) (hq : ∀ x, q x ∈ Icc η (1 - η)) (x : X) : 0 ≤ (p x - q x) ^ 2 / η ^ 2 ∧ (p x - q x) ^ 2 / η ^ 2 ≤ 1 / η ^ 2 := by have hdiff : -1 ≤ p x - q x ∧ p x - q x ≤ 1 := by rcases hp x with ⟨hpl, hpu⟩ rcases hq x with ⟨hql, hqu⟩ constructor <;> linarith constructor · positivity · apply (div_le_div_iff₀ hηsq hηsq).2 have hs : (p x - q x) ^ 2 ≤ 1 := by nlinarith [sq_nonneg (p x - q x)] simpa using mul_le_mul_of_nonneg_right hs hηsq.le have hmeas : Measurable (fun x => (1 - e x) * ((q₀ x - q₀' x) ^ 2 / η ^ 2) + e x * ((q₁ x - q₁' x) ^ 2 / η ^ 2)) := by fun_prop have hint : Integrable (fun x => (1 - e x) * ((q₀ x - q₀' x) ^ 2 / η ^ 2) + e x * ((q₁ x - q₁' x) ^ 2 / η ^ 2)) μ := by apply Integrable.of_bound hmeas.aestronglyMeasurable (2 / η ^ 2) filter_upwards [] with x have he0 : 0 ≤ e x ∧ e x ≤ 1 := by rcases heη x with ⟨hl, hu⟩ constructor <;> linarith have h₀ := hbound q₀ q₀' hq₀η hq₀'η x have h₁ := hbound q₁ q₁' hq₁η hq₁'η x have hA : (1 - e x) * ((q₀ x - q₀' x) ^ 2 / η ^ 2) ≤ 1 / η ^ 2 := by calc _ ≤ (1 - e x) * (1 / η ^ 2) := mul_le_mul_of_nonneg_left h₀.2 (by linarith) _ ≤ 1 / η ^ 2 := by exact mul_le_of_le_one_left (by positivity) (by linarith) have hB : e x * ((q₁ x - q₁' x) ^ 2 / η ^ 2) ≤ 1 / η ^ 2 := by calc _ ≤ e x * (1 / η ^ 2) := mul_le_mul_of_nonneg_left h₁.2 he0.1 _ ≤ 1 / η ^ 2 := mul_le_of_le_one_left (by positivity) he0.2 rw [Real.norm_eq_abs, abs_of_nonneg (add_nonneg (mul_nonneg (by linarith) h₀.1) (mul_nonneg he0.1 h₁.1))] calc _ ≤ 1 / η ^ 2 + 1 / η ^ 2 := add_le_add hA hB _ = 2 / η ^ 2 := by ring rw [selectedLaw_klDiv_toReal_eq_integral μ e q₀ q₁ q₀' q₁' he hq₀ hq₁ hq₀' hq₁' hη0 heη hq₀η hq₁η hq₀'η hq₁'η] apply integral_mono_of_nonneg · filter_upwards [] with x have hpos (p q : ℝ) (hp : p ∈ Icc η (1 - η)) (hq : q ∈ Icc η (1 - η)) : 0 ≤ bernoulliKL p q := by unfold bernoulliKL rw [← bernoulliLaw_klDiv_toReal (by linarith [hp.1]) (by linarith [hp.2]) (by linarith [hq.1]) (by linarith [hq.2])] exact ENNReal.toReal_nonneg exact add_nonneg (mul_nonneg (by linarith [(heη x).2]) (hpos _ _ (hq₀η x) (hq₀'η x))) (mul_nonneg (by linarith [(heη x).1]) (hpos _ _ (hq₁η x) (hq₁'η x))) · exact hint · filter_upwards [] with x exact add_le_add (mul_le_mul_of_nonneg_left (bernoulliKL_le_inv_margin_sq hη0 (hq₀η x) (hq₀'η x)) (by linarith [(heη x).2])) (mul_le_mul_of_nonneg_left (bernoulliKL_le_inv_margin_sq hη0 (hq₁η x) (hq₁'η x)) (by linarith [(heη x).1]))

theorem selectedLaw_klDiv_toReal_le_symmetric {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ t : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (htm : Measurable t) {η : ℝ} (hη0 : 0 < η) (heη : ∀ x, e x ∈ Icc η (1 - η)) (hq₀η : ∀ x, q₀ x ∈ Icc η (1 - η)) (hplusη : ∀ x, 1 / 2 + t x ∈ Icc η (1 - η)) (hminusη : ∀ x, 1 / 2 - t x ∈ Icc η (1 - η)) (ht : ∀ x, |t x| ≤ 1 / 32) : (klDiv (selectedLaw μ e q₀ (fun x => 1 / 2 + t x)) (selectedLaw μ e q₀ (fun x => 1 / 2 - t x))).toReal ≤ ∫ x, e x * (4 * ((1 / 2 + t x) - (1 / 2 - t x)) ^ 2) ∂μ := by have hmeas : Measurable (fun x => e x * (4 * ((1 / 2 + t x) - (1 / 2 - t x)) ^ 2)) := by fun_prop have hint : Integrable (fun x => e x * (4 * ((1 / 2 + t x) - (1 / 2 - t x)) ^ 2)) μ := by apply Integrable.of_bound hmeas.aestronglyMeasurable 4 filter_upwards [] with x have he0 : 0 ≤ e x ∧ e x ≤ 1 := by rcases heη x with ⟨hl, hu⟩ constructor <;> linarith have hd : -1 ≤ (1 / 2 + t x) - (1 / 2 - t x) ∧ (1 / 2 + t x) - (1 / 2 - t x) ≤ 1 := by rcases hplusη x with ⟨hpl, hpu⟩ rcases hminusη x with ⟨hml, hmu⟩ constructor <;> linarith have hs : ((1 / 2 + t x) - (1 / 2 - t x)) ^ 2 ≤ 1 := by nlinarith [sq_nonneg ((1 / 2 + t x) - (1 / 2 - t x))] rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg he0.1 (mul_nonneg (by norm_num) (sq_nonneg _)))] calc _ ≤ e x * 4 := mul_le_mul_of_nonneg_left (by nlinarith) he0.1 _ ≤ 4 := by nlinarith rw [selectedLaw_klDiv_toReal_eq_integral μ e q₀ (fun x => 1 / 2 + t x) q₀ (fun x => 1 / 2 - t x) he hq₀ (by fun_prop) hq₀ (by fun_prop) hη0 heη hq₀η hplusη hq₀η hminusη] have hzero (x : X) : bernoulliKL (q₀ x) (q₀ x) = 0 := by have hp0 : q₀ x ≠ 0 := ne_of_gt (lt_of_lt_of_le hη0 (hq₀η x).1) have hp1 : 1 - q₀ x ≠ 0 := ne_of_gt (by linarith [(hq₀η x).2]) simp [bernoulliKL, div_self hp0, div_self hp1] have hpos (x : X) : 0 ≤ bernoulliKL (1 / 2 + t x) (1 / 2 - t x) := by unfold bernoulliKL rw [← bernoulliLaw_klDiv_toReal (by linarith [(hplusη x).1]) (by linarith [(hplusη x).2]) (by linarith [(hminusη x).1]) (by linarith [(hminusη x).2])] exact ENNReal.toReal_nonneg apply integral_mono_of_nonneg · filter_upwards [] with x rw [hzero x, mul_zero, zero_add] exact mul_nonneg (by linarith [(heη x).1]) (hpos x) · exact hint · filter_upwards [] with x rw [hzero x, mul_zero, zero_add] exact mul_le_mul_of_nonneg_left (bernoulliKL_symmetric_le_four (ht x)) (by linarith [(heη x).1])

theorem sum_cellMass_mul_log_ratio_eq_weighted_bernoulliKL {e q₀ q₁ q₀' q₁' : ℝ} (he0 : 0 < e) (he1 : e < 1) : (∑ a : Bool, ∑ y : Bool, cellMass e q₀ q₁ a y * log (cellMass e q₀ q₁ a y / cellMass e q₀' q₁' a y)) = (1 - e) * bernoulliKL q₀ q₀' + e * bernoulliKL q₁ q₁' := by have he' : 1 - e ≠ 0 := ne_of_gt (by linarith : 0 < 1 - e) have he : e ≠ 0 := ne_of_gt he0 simp only [Fintype.sum_bool] dsimp [cellMass, bitMass] simp only [mul_div_mul_left _ _ he, mul_div_mul_left _ _ he'] unfold bernoulliKL ring

theorem selectedLaw_klDiv_toReal_eq_integral {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ q₀' q₁' : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (hq₀' : Measurable q₀') (hq₁' : Measurable q₁') {η : ℝ} (hη0 : 0 < η) (heη : ∀ x, e x ∈ Icc η (1 - η)) (hq₀η : ∀ x, q₀ x ∈ Icc η (1 - η)) (hq₁η : ∀ x, q₁ x ∈ Icc η (1 - η)) (hq₀'η : ∀ x, q₀' x ∈ Icc η (1 - η)) (hq₁'η : ∀ x, q₁' x ∈ Icc η (1 - η)) : (klDiv (selectedLaw μ e q₀ q₁) (selectedLaw μ e q₀' q₁')).toReal = ∫ x, (1 - e x) * bernoulliKL (q₀ x) (q₀' x) + e x * bernoulliKL (q₁ x) (q₁' x) ∂μ := by have h01 (p : X → ℝ) (hp : ∀ x, p x ∈ Icc η (1 - η)) (x : X) : p x ∈ Icc (0 : ℝ) 1 := by rcases hp x with ⟨hl, hu⟩ constructor <;> linarith letI : IsProbabilityMeasure (selectedLaw μ e q₀ q₁) := selectedLaw_probability μ e q₀ q₁ he hq₀ hq₁ (h01 e heη) (h01 q₀ hq₀η) (h01 q₁ hq₁η) letI : IsProbabilityMeasure (selectedLaw μ e q₀' q₁') := selectedLaw_probability μ e q₀' q₁' he hq₀' hq₁' (h01 e heη) (h01 q₀' hq₀'η) (h01 q₁' hq₁'η) have hac := selectedLaw_ac μ e q₀ q₁ q₀' q₁' he hq₀ hq₁ hq₀' hq₁' hη0 heη hq₀'η hq₁'η rw [InformationTheory.toReal_klDiv_of_measure_eq hac (by simp), integral_congr_ae (selectedLaw_llr_ae_eq_cell_log μ e q₀ q₁ q₀' q₁' he hq₀ hq₁ hq₀' hq₁' hη0 heη hq₀'η hq₁'η), selectedLaw_integral_cell_log_eq_sum μ e q₀ q₁ q₀' q₁' he hq₀ hq₁ hq₀' hq₁' hη0 heη hq₀η hq₁η hq₀'η hq₁'η] congr 1 funext x have hpos (p : ℝ) (hp : p ∈ Icc η (1 - η)) : 0 < p ∧ p < 1 := by rcases hp with ⟨hl, hu⟩ constructor <;> linarith exact sum_cellMass_mul_log_ratio_eq_weighted_bernoulliKL (hpos (e x) (heη x)).1 (hpos (e x) (heη x)).2

theorem selectedLaw_integral_cell_log_eq_sum {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ q₀' q₁' : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (hq₀' : Measurable q₀') (hq₁' : Measurable q₁') {η : ℝ} (hη0 : 0 < η) (heη : ∀ x, e x ∈ Icc η (1 - η)) (hq₀η : ∀ x, q₀ x ∈ Icc η (1 - η)) (hq₁η : ∀ x, q₁ x ∈ Icc η (1 - η)) (hq₀'η : ∀ x, q₀' x ∈ Icc η (1 - η)) (hq₁'η : ∀ x, q₁' x ∈ Icc η (1 - η)) : (∫ z, log (selectedCellRatio e q₀ q₁ q₀' q₁' z).toReal ∂selectedLaw μ e q₀ q₁) = ∫ x, ∑ a : Bool, ∑ y : Bool, cellMass (e x) (q₀ x) (q₁ x) a y * log (cellMass (e x) (q₀ x) (q₁ x) a y / cellMass (e x) (q₀' x) (q₁' x) a y) ∂μ := by let ν : Measure ((Bool × Bool) × X) := ((Measure.count : Measure Bool).prod (Measure.count : Measure Bool)).prod μ let f : ((Bool × Bool) × X) → SelectedCoord X := fun z => (z.2, z.1) let g : SelectedCoord X → ℝ := fun z => log (selectedCellRatio e q₀ q₁ q₀' q₁' z).toReal have hf : Measurable f := by fun_prop have hc (p q s : X → ℝ) (hp : Measurable p) (hq : Measurable q) (hs : Measurable s) : Measurable (fun z : SelectedCoord X => cellMass (p z.1) (q z.1) (s z.1) z.2.1 z.2.2) := by unfold cellMass bitMass apply mul · apply Measurable.ite · measurability · exact hp.comp (by fun_prop) · exact measurable_const.sub (hp.comp (by fun_prop)) · apply Measurable.ite · measurability · apply Measurable.ite · measurability · exact hs.comp (by fun_prop) · exact hq.comp (by fun_prop) · exact measurable_const.sub (by apply Measurable.ite · measurability · exact hs.comp (by fun_prop) · exact hq.comp (by fun_prop)) have hg : Measurable g := by unfold g selectedCellRatio exact Real.measurable_log.comp (ENNReal.measurable_toReal.comp (ENNReal.measurable_ofReal.comp ((hc e q₀ q₁ he hq₀ hq₁).div (hc e q₀' q₁' he hq₀' hq₁')))) have hd : Measurable (selectedDensity e q₀ q₁) := by change Measurable (fun z : (Bool × Bool) × X => ofReal (cellMass (e z.2) (q₀ z.2) (q₁ z.2) z.1.1 z.1.2)) simpa [f, Function.comp_def] using (ENNReal.measurable_ofReal.comp (hc e q₀ q₁ he hq₀ hq₁)).comp hf have htop : ∀ᵐ z ∂ν, selectedDensity e q₀ q₁ z < ⊤ := by filter_upwards [] with z simp [selectedDensity] have hgi : Integrable g (selectedLaw μ e q₀ q₁) := selectedCellRatio_log_integrable μ e q₀ q₁ q₀' q₁' he hq₀ hq₁ hq₀' hq₁' hη0 heη hq₀η hq₁η hq₀'η hq₁'η have hwi : Integrable (g ∘ f) (ν.withDensity (selectedDensity e q₀ q₁)) := by exact (integrable_map_measure hg.aestronglyMeasurable hf.aemeasurable).1 hgi have hprod : Integrable (fun z : (Bool × Bool) × X => (selectedDensity e q₀ q₁ z).toReal * g (f z)) ν := by simpa [smul_eq_mul] using (integrable_withDensity_iff_integrable_smul₀' hd.aemeasurable htop).1 hwi have hpos (p : ℝ) (hp : p ∈ Icc η (1 - η)) (b : Bool) : 0 < bitMass p b := by cases b with | false => change 0 < 1 - p; linarith [hp.2] | true => change 0 < p; exact lt_of_lt_of_le hη0 hp.1 have hcellpos (x : X) (a y : Bool) : 0 < cellMass (e x) (q₀ x) (q₁ x) a y ∧ 0 < cellMass (e x) (q₀' x) (q₁' x) a y := by unfold cellMass constructor · exact mul_pos (hpos (e x) (heη x) a) (by cases a with | false => exact hpos (q₀ x) (hq₀η x) y | true => exact hpos (q₁ x) (hq₁η x) y) · exact mul_pos (hpos (e x) (heη x) a) (by cases a with | false => exact hpos (q₀' x) (hq₀'η x) y | true => exact hpos (q₁' x) (hq₁'η x) y) have hpoint (z : (Bool × Bool) × X) : (selectedDensity e q₀ q₁ z).toReal * g (f z) = cellMass (e z.2) (q₀ z.2) (q₁ z.2) z.1.1 z.1.2 * log (cellMass (e z.2) (q₀ z.2) (q₁ z.2) z.1.1 z.1.2 / cellMass (e z.2) (q₀' z.2) (q₁' z.2) z.1.1 z.1.2) := by obtain ⟨⟨a, y⟩, x⟩ := z dsimp [selectedDensity, g, f, selectedCellRatio] rw [ENNReal.toReal_ofReal (hcellpos x a y).1.le, ENNReal.toReal_ofReal (div_pos (hcellpos x a y).1 (hcellpos x a y).2).le] change ∫ z, g z ∂(ν.withDensity (selectedDensity e q₀ q₁)).map f = _ rw [integral_map hf.aemeasurable hg.aestronglyMeasurable, integral_withDensity_eq_integral_toReal_smul₀ hd.aemeasurable htop] simp only [smul_eq_mul] rw [integral_prod_symm _ hprod] congr 1 funext x rw [integral_fintype (hf := Integrable.of_finite)] simp_rw [hpoint] have hm (a y : Bool) : (Measure.count.prod (Measure.count : Measure Bool) : Measure (Bool × Bool)) {(a, y)} = 1 := by rw [show ({(a, y)} : Set (Bool × Bool)) = ({a} : Set Bool) ×ˢ {y} by ext ⟨b, c⟩; simp] rw [Measure.prod_prod] simp simp [measureReal_def, hm, Fintype.sum_prod_type]

theorem selectedCellRatio_log_integrable {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ q₀' q₁' : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (hq₀' : Measurable q₀') (hq₁' : Measurable q₁') {η : ℝ} (hη0 : 0 < η) (heη : ∀ x, e x ∈ Icc η (1 - η)) (hq₀η : ∀ x, q₀ x ∈ Icc η (1 - η)) (hq₁η : ∀ x, q₁ x ∈ Icc η (1 - η)) (hq₀'η : ∀ x, q₀' x ∈ Icc η (1 - η)) (hq₁'η : ∀ x, q₁' x ∈ Icc η (1 - η)) : Integrable (fun z => log (selectedCellRatio e q₀ q₁ q₀' q₁' z).toReal) (selectedLaw μ e q₀ q₁) := by have he01 (x : X) : e x ∈ Icc (0 : ℝ) 1 := by rcases heη x with ⟨hl, hu⟩ constructor <;> linarith have hq₀01 (x : X) : q₀ x ∈ Icc (0 : ℝ) 1 := by rcases hq₀η x with ⟨hl, hu⟩ constructor <;> linarith have hq₁01 (x : X) : q₁ x ∈ Icc (0 : ℝ) 1 := by rcases hq₁η x with ⟨hl, hu⟩ constructor <;> linarith letI : IsProbabilityMeasure (selectedLaw μ e q₀ q₁) := selectedLaw_probability μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01 have hmeas : Measurable (fun z => log (selectedCellRatio e q₀ q₁ q₀' q₁' z).toReal) := Real.measurable_log.comp (ENNReal.measurable_toReal.comp (measurable_selectedCellRatio he hq₀ hq₁ hq₀' hq₁')) apply Integrable.of_mem_Icc (log (η ^ 2)) (-log (η ^ 2)) hmeas.aemeasurable filter_upwards [] with z obtain ⟨x, ⟨a, y⟩⟩ := z have hA := cellMass_mem_Icc hη0 (heη x) (hq₀η x) (hq₁η x) a y have hB := cellMass_mem_Icc hη0 (heη x) (hq₀'η x) (hq₁'η x) a y have hη2 : 0 < η ^ 2 := pow_pos hη0 _ have hApos : 0 < cellMass (e x) (q₀ x) (q₁ x) a y := lt_of_lt_of_le hη2 hA.1 have hBpos : 0 < cellMass (e x) (q₀' x) (q₁' x) a y := lt_of_lt_of_le hη2 hB.1 have hlogA₁ := Real.log_le_log hη2 hA.1 have hlogA₂ := Real.log_le_log hApos hA.2 have hlogB₁ := Real.log_le_log hη2 hB.1 have hlogB₂ := Real.log_le_log hBpos hB.2 change log (ofReal (cellMass (e x) (q₀ x) (q₁ x) a y / cellMass (e x) (q₀' x) (q₁' x) a y)).toReal ∈ Icc (log (η ^ 2)) (-log (η ^ 2)) rw [ENNReal.toReal_ofReal (le_of_lt (div_pos hApos hBpos)), Real.log_div (ne_of_gt hApos) (ne_of_gt hBpos)] simp only [Set.mem_Icc, Real.log_one] at * constructor <;> linarith

theorem selectedLaw_llr_integrable {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ q₀' q₁' : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (hq₀' : Measurable q₀') (hq₁' : Measurable q₁') {η : ℝ} (hη0 : 0 < η) (heη : ∀ x, e x ∈ Icc η (1 - η)) (hq₀η : ∀ x, q₀ x ∈ Icc η (1 - η)) (hq₁η : ∀ x, q₁ x ∈ Icc η (1 - η)) (hq₀'η : ∀ x, q₀' x ∈ Icc η (1 - η)) (hq₁'η : ∀ x, q₁' x ∈ Icc η (1 - η)) : Integrable (llr (selectedLaw μ e q₀ q₁) (selectedLaw μ e q₀' q₁')) (selectedLaw μ e q₀ q₁) := by exact (selectedCellRatio_log_integrable μ e q₀ q₁ q₀' q₁' he hq₀ hq₁ hq₀' hq₁' hη0 heη hq₀η hq₁η hq₀'η hq₁'η).congr (selectedLaw_llr_ae_eq_cell_log μ e q₀ q₁ q₀' q₁' he hq₀ hq₁ hq₀' hq₁' hη0 heη hq₀'η hq₁'η).symm