Stat.Minimax.Mixture

theorem mixture_isProbabilityMeasure (w : ι → ℝ≥0∞) (hw : ∑ i, w i = 1) (P : ι → Measure Ω) [∀ i, IsProbabilityMeasure (P i)] : IsProbabilityMeasure (mixture w P) := by refine ⟨?_⟩ rw [mixture_apply] simp only [measure_univ, mul_one] exact hw

theorem exists_real_ge_mixture [Nonempty ι] (w : ι → ℝ≥0∞) (hw : ∑ i, w i = 1) (P : ι → Measure Ω) [∀ i, IsProbabilityMeasure (P i)] (A : Set Ω) : ∃ i, (mixture w P).real A ≤ (P i).real A := by obtain ⟨i, _, hmax⟩ := Finset.exists_max_image (Finset.univ : Finset ι) (fun i => (P i).real A) univ_nonempty exact ⟨i, mixtureReal_le w hw P A ((P i).real A) (fun j => hmax j (Finset.mem_univ j))⟩

theorem priorPredictive_isProbability (π : Measure Θ) (K : Kernel Θ X) [IsProbabilityMeasure π] (hK : ∀ θ, IsProbabilityMeasure (K θ)) : IsProbabilityMeasure (priorPredictive π K) := by rw [priorPredictive] apply isProbabilityMeasure_iff.mpr rw [Measure.bind_apply MeasurableSet.univ K.aemeasurable] simp_rw [isProbabilityMeasure_iff.mp (hK _)] simp

theorem iidRnDeriv_eq_prod {Ω : Type*} [MeasurableSpace Ω] (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hQ : Q ≪ P) (n : ℕ) : (Measure.pi (fun _ : Fin n => Q)).rnDeriv (Measure.pi (fun _ : Fin n => P)) =ᵐ[Measure.pi (fun _ : Fin n => P)] (fun x => ∏ i : Fin n, Q.rnDeriv P (x i)) := by induction n with | zero => have heq : Measure.pi (fun _ : Fin 0 => Q) = Measure.pi (fun _ : Fin 0 => P) := by rw [Measure.pi_of_empty, Measure.pi_of_empty] rw [heq] simpa using (Measure.rnDeriv_self (Measure.pi (fun _ : Fin 0 => P))) | succ n ih => let e := piFinSuccAbove (fun _ : Fin (n + 1) => Ω) 0 have hQmap := measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => Q) 0 have hPmap := measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => P) 0 have htail : Measure.pi (fun _ : Fin n => Q) ≪ Measure.pi (fun _ : Fin n => P) := pi_iid_absolutelyContinuous Q P hQ n have hb := rnDeriv_prod_eq Q P (Measure.pi (fun _ : Fin n => Q)) (Measure.pi (fun _ : Fin n => P)) hQ htail have hitail := (Measure.quasiMeasurePreserving_snd (μ := P) (ν := Measure.pi (fun _ : Fin n => P))).ae_eq_comp ih have hprod : (Q.prod (Measure.pi (fun _ : Fin n => Q))).rnDeriv (P.prod (Measure.pi (fun _ : Fin n => P))) =ᵐ[ P.prod (Measure.pi (fun _ : Fin n => P))] fun z => Q.rnDeriv P z.1 * ∏ i, Q.rnDeriv P (z.2 i) := by filter_upwards [hb, hitail] with z hz ht simp only [Function.comp_apply] at ht rw [hz, ht] have hpull := hPmap.quasiMeasurePreserving.ae_eq_comp hprod have hmap := e.measurableEmbedding.rnDeriv_map (Measure.pi (fun _ : Fin (n + 1) => Q)) (Measure.pi (fun _ : Fin (n + 1) => P)) filter_upwards [hmap, hpull] with x hm hp simp only [Function.comp_apply] at hp rw [← hm, hQmap.map_eq, hPmap.map_eq, hp, Fin.prod_univ_succ] congr 1

theorem iidRnDeriv_toReal_eq_prod {Ω : Type*} [MeasurableSpace Ω] (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hQ : Q ≪ P) (n : ℕ) : (fun x => ((Measure.pi (fun _ : Fin n => Q)).rnDeriv (Measure.pi (fun _ : Fin n => P)) x).toReal) =ᵐ[ Measure.pi (fun _ : Fin n => P)] (fun x => ∏ i : Fin n, (Q.rnDeriv P (x i)).toReal) := by filter_upwards [iidRnDeriv_eq_prod P Q hQ n] with x hx simpa only [hx, ENNReal.toReal_prod]

theorem uniformMixture_isProbability {Ω S : Type*} [MeasurableSpace Ω] [Fintype S] [Nonempty S] (Q : S → Measure Ω) [∀ s, IsProbabilityMeasure (Q s)] : IsProbabilityMeasure (uniformMixture Q) := by apply Causalean.Stat.mixture_isProbabilityMeasure have hc : (Fintype.card S : ℝ≥0∞) ≠ 0 := by exact_mod_cast Fintype.card_ne_zero rw [Finset.sum_const, nsmul_eq_mul] exact ENNReal.mul_inv_cancel hc (by simp)

theorem uniformMixture_absolutelyContinuous {Ω S : Type*} [MeasurableSpace Ω] [Fintype S] [Nonempty S] (Q : S → Measure Ω) (P : Measure Ω) (hac : ∀ s, Q s ≪ P) : uniformMixture Q ≪ P := by unfold uniformMixture mixture have h (t : Finset S) : t.sum (fun s => (Fintype.card S : ℝ≥0∞)⁻¹ • Q s) ≪ P := by classical induction t using Finset.induction_on with | empty => simp | @insert s t hs ih => simpa [Finset.sum_insert hs] using Measure.AbsolutelyContinuous.add_left ((hac s).smul_left ((Fintype.card S : ℝ≥0∞)⁻¹)) ih exact h univ

theorem uniformMixture_rnDeriv {Ω S : Type*} [MeasurableSpace Ω] [Fintype S] [Nonempty S] (Q : S → Measure Ω) (P : Measure Ω) [IsProbabilityMeasure P] [∀ s, IsProbabilityMeasure (Q s)] : (fun x => ((uniformMixture Q).rnDeriv P x).toReal) =ᵐ[P] (fun x => (∑ s, ((Q s).rnDeriv P x).toReal) / (Fintype.card S : ℝ)) := by classical let w : ℝ≥0∞ := (Fintype.card S : ℝ≥0∞)⁻¹ have hw : w ≠ ⊤ := by simp [w] haveI (s : S) : IsFiniteMeasure (w • Q s) := (Q s).smul_finite hw have hrn (t : Finset S) : (t.sum (fun s => w • Q s)).rnDeriv P =ᵐ[P] fun x => t.sum (fun s => w * (Q s).rnDeriv P x) := by induction t using Finset.induction_on with | empty => filter_upwards [Measure.rnDeriv_zero P] with x hx simpa using hx | @insert s t hs ih => haveI : IsFiniteMeasure (t.sum (fun s => w • Q s)) := inferInstance have hadd := Measure.rnDeriv_add (w • Q s) (t.sum (fun s => w • Q s)) P have hsmul := Measure.rnDeriv_smul_left_of_ne_top (Q s) P hw filter_upwards [hadd, hsmul, ih] with x hx ha hb simpa [Finset.sum_insert hs, Pi.add_apply, Pi.smul_apply, smul_eq_mul, ha, hb] using hx have hfinite : ∀ᵐ x ∂P, ∀ s : S, (Q s).rnDeriv P x ≠ ⊤ := by rw [Filter.eventually_all] intro s exact (Measure.rnDeriv_lt_top (Q s) P).mono (fun x hx => ne_of_lt hx) filter_upwards [hrn univ, hfinite] with x hx hfx change ((Finset.univ.sum (fun s => w • Q s)).rnDeriv P x).toReal = (∑ s, ((Q s).rnDeriv P x).toReal) / (Fintype.card S : ℝ) rw [hx, ENNReal.toReal_sum (fun s _ => ENNReal.mul_ne_top hw (hfx s))] simp_rw [ENNReal.toReal_mul] simp [w, ENNReal.toReal_inv, ENNReal.toReal_natCast, div_eq_mul_inv, Finset.mul_sum, mul_comm]

theorem one_add_chiSqDiv_uniformMixture {Ω S : Type*} [MeasurableSpace Ω] [Fintype S] [Nonempty S] (Q : S → Measure Ω) (P : Measure Ω) [IsProbabilityMeasure P] [∀ s, IsProbabilityMeasure (Q s)] (hac : ∀ s, Q s ≪ P) (hpair : ∀ s t, Integrable (fun x => ((Q s).rnDeriv P x).toReal * ((Q t).rnDeriv P x).toReal) P) : 1 + chiSqDiv (uniformMixture Q) P = (∑ s : S, ∑ t : S, ∫ x, ((Q s).rnDeriv P x).toReal * ((Q t).rnDeriv P x).toReal ∂P) / (Fintype.card S : ℝ) ^ 2 := by classical haveI : IsProbabilityMeasure (uniformMixture Q) := uniformMixture_isProbability Q let d (s : S) (x : Ω) : ℝ := ((Q s).rnDeriv P x).toReal let p (x : Ω) : ℝ := ((uniformMixture Q).rnDeriv P x).toReal let n : ℝ := Fintype.card S have hdouble : Integrable (fun x => ∑ s : S, ∑ t : S, d s x * d t x) P := by apply integrable_finsetSum Finset.univ intro s _ apply integrable_finsetSum Finset.univ intro t _ exact hpair s t have hpoint : ∀ᵐ x ∂P, p x ^ 2 = (∑ s : S, ∑ t : S, d s x * d t x) / n ^ 2 := by filter_upwards [uniformMixture_rnDeriv Q P] with x hx change p x = (∑ s : S, d s x) / n at hx rw [hx, div_pow, sq, Finset.sum_mul_sum] have hsq : Integrable (fun x => p x ^ 2) P := by exact (hdouble.div_const (n ^ 2)).congr (hpoint.mono fun x hx => hx.symm) have hp : Integrable p P := Measure.integrable_toReal_rnDeriv have hdev : Integrable (fun x => (p x - 1) ^ 2) P := by have heq : (fun x => (p x - 1) ^ 2) = (fun x => p x ^ 2 - 2 * p x + 1) := by funext x; ring rw [heq] exact (hsq.sub (hp.const_mul 2)).add (integrable_const 1) have hint : (∫ x, p x ^ 2 ∂P) = (∑ s : S, ∑ t : S, ∫ x, d s x * d t x ∂P) / n ^ 2 := by calc (∫ x, p x ^ 2 ∂P) = ∫ x, (∑ s : S, ∑ t : S, d s x * d t x) / n ^ 2 ∂P := integral_congr_ae hpoint _ = (∫ x, ∑ s : S, ∑ t : S, d s x * d t x ∂P) / n ^ 2 := integral_div _ _ _ = (∑ s : S, ∑ t : S, ∫ x, d s x * d t x ∂P) / n ^ 2 := by rw [integral_finsetSum] · congr 1 apply Finset.sum_congr rfl intro s _ rw [integral_finsetSum] intro t _ exact hpair s t · intro s _ apply integrable_finsetSum Finset.univ intro t _ exact hpair s t have hchi := chiSqDiv_eq (uniformMixture_absolutelyContinuous Q P hac) hdev change chiSqDiv (uniformMixture Q) P = (∫ x, p x ^ 2 ∂P) - 1 at hchi rw [hchi, hint] ring

theorem iidPairIntegrable {Ω : Type*} [MeasurableSpace Ω] (P Q R : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [IsProbabilityMeasure R] (hQ : Q ≪ P) (hR : R ≪ P) (hint : Integrable (fun x => (Q.rnDeriv P x).toReal * (R.rnDeriv P x).toReal) P) (n : ℕ) : Integrable (fun x => (((Measure.pi (fun _ : Fin n => Q)).rnDeriv (Measure.pi (fun _ : Fin n => P)) x).toReal) * (((Measure.pi (fun _ : Fin n => R)).rnDeriv (Measure.pi (fun _ : Fin n => P)) x).toReal)) (Measure.pi (fun _ : Fin n => P)) := by have hprod : Integrable (fun x : Fin n → Ω => ∏ i : Fin n, (Q.rnDeriv P (x i)).toReal * (R.rnDeriv P (x i)).toReal) (Measure.pi (fun _ : Fin n => P)) := Integrable.fin_nat_prod (fun _ => hint) have heq : (fun x => (((Measure.pi (fun _ : Fin n => Q)).rnDeriv (Measure.pi (fun _ : Fin n => P)) x).toReal) * (((Measure.pi (fun _ : Fin n => R)).rnDeriv (Measure.pi (fun _ : Fin n => P)) x).toReal)) =ᵐ[ Measure.pi (fun _ : Fin n => P)] (fun x => ∏ i : Fin n, (Q.rnDeriv P (x i)).toReal * (R.rnDeriv P (x i)).toReal) := by filter_upwards [iidRnDeriv_toReal_eq_prod P Q hQ n, iidRnDeriv_toReal_eq_prod P R hR n] with x hqx hrx rw [hqx, hrx, ← Finset.prod_mul_distrib] exact hprod.congr heq.symm

theorem iidPairOverlap {Ω : Type*} [MeasurableSpace Ω] (P Q R : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [IsProbabilityMeasure R] (hQ : Q ≪ P) (hR : R ≪ P) (n : ℕ) : (∫ x, (((Measure.pi (fun _ : Fin n => Q)).rnDeriv (Measure.pi (fun _ : Fin n => P)) x).toReal) * (((Measure.pi (fun _ : Fin n => R)).rnDeriv (Measure.pi (fun _ : Fin n => P)) x).toReal) ∂(Measure.pi (fun _ : Fin n => P))) = (∫ x, (Q.rnDeriv P x).toReal * (R.rnDeriv P x).toReal ∂P) ^ n := by have heq : (fun x => (((Measure.pi (fun _ : Fin n => Q)).rnDeriv (Measure.pi (fun _ : Fin n => P)) x).toReal) * (((Measure.pi (fun _ : Fin n => R)).rnDeriv (Measure.pi (fun _ : Fin n => P)) x).toReal)) =ᵐ[ Measure.pi (fun _ : Fin n => P)] (fun x => ∏ i : Fin n, (Q.rnDeriv P (x i)).toReal * (R.rnDeriv P (x i)).toReal) := by filter_upwards [iidRnDeriv_toReal_eq_prod P Q hQ n, iidRnDeriv_toReal_eq_prod P R hR n] with x hqx hrx rw [hqx, hrx, ← Finset.prod_mul_distrib] rw [integral_congr_ae heq] simpa using (integral_fintype_prod_eq_pow (ι := Fin n) (μ := P) (fun x => (Q.rnDeriv P x).toReal * (R.rnDeriv P x).toReal))

theorem iid_absolutelyContinuous_of_likelihood {Ω : Type*} [MeasurableSpace Ω] (μ Q : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure Q] (L : Ω → ℝ) (hQ : Q = μ.withDensity (fun x => ofReal (L x))) (n : ℕ) : Measure.pi (fun _ : Fin n => Q) ≪ Measure.pi (fun _ : Fin n => μ) := by apply pi_iid_absolutelyContinuous Q μ _ n rw [hQ] exact withDensity_absolutelyContinuous μ _

theorem iid_pair_integrable_of_likelihood {Ω : Type*} [MeasurableSpace Ω] (μ Q R : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure Q] [IsProbabilityMeasure R] (L M : Ω → ℝ) (hL : Measurable L) (hM : Measurable M) (hL0 : ∀ x, 0 ≤ L x) (hM0 : ∀ x, 0 ≤ M x) (hQ : Q = μ.withDensity (fun x => ofReal (L x))) (hR : R = μ.withDensity (fun x => ofReal (M x))) (hpairInt : Integrable (fun x => L x * M x) μ) (n : ℕ) : Integrable (fun x => (((Measure.pi (fun _ : Fin n => Q)).rnDeriv (Measure.pi (fun _ : Fin n => μ)) x).toReal) * (((Measure.pi (fun _ : Fin n => R)).rnDeriv (Measure.pi (fun _ : Fin n => μ)) x).toReal)) (Measure.pi (fun _ : Fin n => μ)) := by have hLeq : (fun x => (Q.rnDeriv μ x).toReal) =ᵐ[μ] L := by rw [hQ] filter_upwards [Measure.rnDeriv_withDensity μ hL.ennreal_ofReal] with x hx simp [hx, ENNReal.toReal_ofReal (hL0 x)] have hMeq : (fun x => (R.rnDeriv μ x).toReal) =ᵐ[μ] M := by rw [hR] filter_upwards [Measure.rnDeriv_withDensity μ hM.ennreal_ofReal] with x hx simp [hx, ENNReal.toReal_ofReal (hM0 x)] have hprod : (fun x => (Q.rnDeriv μ x).toReal * (R.rnDeriv μ x).toReal) =ᵐ[μ] (fun x => L x * M x) := by filter_upwards [hLeq, hMeq] with x hx hy simp [hx, hy] have hacQ : Q ≪ μ := by rw [hQ] exact withDensity_absolutelyContinuous μ _ have hacR : R ≪ μ := by rw [hR] exact withDensity_absolutelyContinuous μ _ have hint : Integrable (fun x => (Q.rnDeriv μ x).toReal * (R.rnDeriv μ x).toReal) μ := hpairInt.congr hprod.symm exact iidPairIntegrable μ Q R hacQ hacR hint n

theorem product_pair_integrable {Ω₁ Ω₂ : Type*} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] (P₁ Q₁ R₁ : Measure Ω₁) (P₂ Q₂ R₂ : Measure Ω₂) [IsProbabilityMeasure P₁] [IsProbabilityMeasure Q₁] [IsProbabilityMeasure R₁] [IsProbabilityMeasure P₂] [IsProbabilityMeasure Q₂] [IsProbabilityMeasure R₂] (hQ₁ : Q₁ ≪ P₁) (hR₁ : R₁ ≪ P₁) (hQ₂ : Q₂ ≪ P₂) (hR₂ : R₂ ≪ P₂) (hInt₁ : Integrable (fun x => (Q₁.rnDeriv P₁ x).toReal * (R₁.rnDeriv P₁ x).toReal) P₁) (hInt₂ : Integrable (fun x => (Q₂.rnDeriv P₂ x).toReal * (R₂.rnDeriv P₂ x).toReal) P₂) : Integrable (fun z => ((Q₁.prod Q₂).rnDeriv (P₁.prod P₂) z).toReal * ((R₁.prod R₂).rnDeriv (P₁.prod P₂) z).toReal) (P₁.prod P₂) := by have hQ := Causalean.Mathlib.Probability.ProductAbsolutelyContinuous.rnDeriv_prod_eq Q₁ P₁ Q₂ P₂ hQ₁ hQ₂ have hR := Causalean.Mathlib.Probability.ProductAbsolutelyContinuous.rnDeriv_prod_eq R₁ P₁ R₂ P₂ hR₁ hR₂ have hEq : (fun z => ((Q₁.prod Q₂).rnDeriv (P₁.prod P₂) z).toReal * ((R₁.prod R₂).rnDeriv (P₁.prod P₂) z).toReal) =ᵐ[P₁.prod P₂] (fun z => ((Q₁.rnDeriv P₁ z.1).toReal * (R₁.rnDeriv P₁ z.1).toReal) * ((Q₂.rnDeriv P₂ z.2).toReal * (R₂.rnDeriv P₂ z.2).toReal)) := by filter_upwards [hQ, hR] with z hzQ hzR simp only [hzQ, hzR, ENNReal.toReal_mul] ring exact (Integrable.mul_prod hInt₁ hInt₂).congr hEq.symm

theorem sign_twoPower_pointwise_le_exp (n₁ n₂ : ℕ) (ρ₁ ρ₂ x : ℝ) (hbase₁ : 0 ≤ 1 + ρ₁ * x) (hbase₂ : 0 ≤ 1 + ρ₂ * x) : (1 + ρ₁ * x) ^ n₁ * (1 + ρ₂ * x) ^ n₂ ≤ exp (((n₁ : ℝ) * ρ₁ + (n₂ : ℝ) * ρ₂) * x) := by have h₁ : (1 + ρ₁ * x) ^ n₁ ≤ (exp (ρ₁ * x)) ^ n₁ := pow_le_pow_left₀ hbase₁ (by simpa [add_comm] using Real.add_one_le_exp (ρ₁ * x)) _ have h₂ : (1 + ρ₂ * x) ^ n₂ ≤ (exp (ρ₂ * x)) ^ n₂ := pow_le_pow_left₀ hbase₂ (by simpa [add_comm] using Real.add_one_le_exp (ρ₂ * x)) _ calc (1 + ρ₁ * x) ^ n₁ * (1 + ρ₂ * x) ^ n₂ ≤ (exp (ρ₁ * x)) ^ n₁ * (exp (ρ₂ * x)) ^ n₂ := mul_le_mul h₁ h₂ (pow_nonneg hbase₂ _) (pow_nonneg (Real.exp_pos _).le _) _ = exp (((n₁ : ℝ) * ρ₁ + (n₂ : ℝ) * ρ₂) * x) := by rw [← Real.exp_nat_mul, ← Real.exp_nat_mul, ← Real.exp_add] congr 1 ring

theorem uniform_innerSign_exp_le (K : ℕ) [NeZero K] (t : ℝ) : (∑ s : Fin K → Bool, ∑ u : Fin K → Bool, exp (t * innerSign s u / (K : ℝ))) / (card (Fin K → Bool) : ℝ) ^ 2 ≤ exp (t ^ 2 / (2 * (K : ℝ))) := by classical have hK : (K : ℝ) ≠ 0 := by exact_mod_cast (NeZero.ne K) have hcard : (card (Fin K → Bool) : ℝ) = (2 : ℝ) ^ K := by simp [Fintype.card_bool] have hinner (s : Fin K → Bool) : (∑ u : Fin K → Bool, exp (t * innerSign s u / (K : ℝ))) / (card (Fin K → Bool) : ℝ) ≤ exp (t ^ 2 / (2 * (K : ℝ))) := by have hswap (u : Fin K → Bool) : innerSign s u = ∑ j : Fin K, (if u j then (1 : ℝ) else -1) * (if s j then (1 : ℝ) else -1) := by unfold innerSign apply Finset.sum_congr rfl intro j hj ring have hsquares : (∑ j : Fin K, (if s j then (1 : ℝ) else -1) ^ 2) = (K : ℝ) := by simp have hm := signMGF_le (fun j : Fin K => if s j then (1 : ℝ) else -1) (t / (K : ℝ)) convert hm using 1 · rw [hcard] congr 1 apply Finset.sum_congr rfl intro u hu congr 1 rw [hswap] ring · rw [hsquares] field_simp calc (∑ s : Fin K → Bool, ∑ u : Fin K → Bool, exp (t * innerSign s u / (K : ℝ))) / (card (Fin K → Bool) : ℝ) ^ 2 = (∑ s : Fin K → Bool, (∑ u : Fin K → Bool, exp (t * innerSign s u / (K : ℝ))) / (card (Fin K → Bool) : ℝ)) / (card (Fin K → Bool) : ℝ) := by simp only [Finset.sum_div] apply Finset.sum_congr rfl intro s hs apply Finset.sum_congr rfl intro u hu ring _ ≤ (∑ _s : Fin K → Bool, exp (t ^ 2 / (2 * (K : ℝ)))) / (card (Fin K → Bool) : ℝ) := by apply div_le_div_of_nonneg_right · exact Finset.sum_le_sum fun s _ => hinner s · rw [hcard] positivity _ = exp (t ^ 2 / (2 * (K : ℝ))) := by simp [Fintype.card_bool]

theorem isProbability_of_cellSetMass {X C : Type*} [MeasurableSpace X] [MeasurableSpace C] [Fintype C] (ν : Measure X) [IsProbabilityMeasure ν] (Q : Measure (X × C)) (q : X → C → ℝ≥0∞) (hQ : ∀ A, MeasurableSet A → Q A = cellSetMass ν q A) (hsum : ∀ x, ∑ c : C, q x c = 1) : IsProbabilityMeasure Q := by apply isProbabilityMeasure_iff.mpr rw [hQ univ MeasurableSet.univ] simp [cellSetMass, hsum]

theorem bind_latent_map_cellSetMass {X C Z : Type*} [MeasurableSpace X] [MeasurableSpace C] [Fintype C] [DecidableEq C] [Fintype Z] (ν : Measure X) (w : X → Z → ℝ≥0∞) (obs : X → Z → C) (hw : ∀ z, Measurable fun x => w x z) (hobs : ∀ z, Measurable fun x => obs x z) : ∀ A, MeasurableSet A → (ν.bind (fun x => ∑ z : Z, w x z • Measure.dirac (x, obs x z))) A = cellSetMass ν (fun x c => ∑ z : Z, if obs x z = c then w x z else 0) A := by intro A hA have hk : Measurable (fun x => ∑ z : Z, w x z • Measure.dirac (x, obs x z)) := by classical refine Measure.measurable_of_measurable_coe _ fun s hs => ?_ simp only [Measure.finsetSum_apply] apply Finset.measurable_fun_sum intro z hz simp only [Measure.smul_apply, smul_eq_mul, Measure.dirac_apply' _ hs] exact (hw z).mul (measurable_one.indicator (hs.preimage (measurable_id.prodMk (hobs z)))) rw [Measure.bind_apply hA hk.aemeasurable] unfold cellSetMass apply lintegral_congr intro x classical simp only [Measure.finsetSum_apply, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply' _ hA] calc (∑ z : Z, w x z * A.indicator 1 (x, obs x z)) = ∑ z : Z, if (x, obs x z) ∈ A then w x z else 0 := by apply Finset.sum_congr rfl intro z hz simp [indicator, mul_ite] _ = ∑ z : Z, ∑ c : C, if (x, c) ∈ A then (if obs x z = c then w x z else 0) else 0 := by apply Finset.sum_congr rfl intro z hz calc (if (x, obs x z) ∈ A then w x z else 0) = ∑ c : C, if obs x z = c then (if (x, c) ∈ A then w x z else 0) else 0 := by simp _ = ∑ c : C, if (x, c) ∈ A then (if obs x z = c then w x z else 0) else 0 := by apply Finset.sum_congr rfl intro c hc split_ifs <;> simp_all _ = ∑ c : C, ∑ z : Z, if (x, c) ∈ A then (if obs x z = c then w x z else 0) else 0 := Finset.sum_comm _ = ∑ c : C, if (x, c) ∈ A then (∑ z : Z, if obs x z = c then w x z else 0) else 0 := by apply Finset.sum_congr rfl intro c hc split_ifs <;> simp

theorem bind_cells_eq_withDensity {X C : Type*} [MeasurableSpace X] [MeasurableSpace C] [Fintype C] (ν : Measure X) (p q : X → C → ℝ≥0∞) (L : X × C → ℝ) (hp : ∀ c, Measurable fun x => p x c) (hq : ∀ c, Measurable fun x => q x c) (hL : Measurable L) (hratio : ∀ x c, q x c = p x c * ofReal (L (x, c))) : ν.bind (fun x => ∑ c : C, q x c • Measure.dirac (x, c)) = (ν.bind (fun x => ∑ c : C, p x c • Measure.dirac (x, c))).withDensity (fun z => ofReal (L z)) := by classical apply eq_withDensity_of_cellSetMass ν _ _ p q L hp hL · intro A hA rw [bind_latent_map_cellSetMass ν p (fun _ c => c) hp (fun _ => measurable_const) A hA] unfold cellSetMass apply lintegral_congr intro x apply Finset.sum_congr rfl intro c hc simp · intro A hA rw [bind_latent_map_cellSetMass ν q (fun _ c => c) hq (fun _ => measurable_const) A hA] unfold cellSetMass apply lintegral_congr intro x apply Finset.sum_congr rfl intro c hc simp · exact hratio

theorem integral_likelihood_eq_one {Ω : Type*} [MeasurableSpace Ω] (μ Q : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure Q] (L : Ω → ℝ) (hL : Measurable L) (hL0 : ∀ x, 0 ≤ L x) (hQ : Q = μ.withDensity (fun x => ofReal (L x))) : ∫ x, L x ∂μ = 1 := by have hLeq : (fun x => (Q.rnDeriv μ x).toReal) =ᵐ[μ] L := by rw [hQ] filter_upwards [Measure.rnDeriv_withDensity μ hL.ennreal_ofReal] with x hx simp [hx, ENNReal.toReal_ofReal (hL0 x)] have hac : Q ≪ μ := by rw [hQ] exact withDensity_absolutelyContinuous μ _ calc ∫ x, L x ∂μ = ∫ x, (Q.rnDeriv μ x).toReal ∂μ := integral_congr_ae hLeq.symm _ = 1 := by simpa using (Measure.integral_toReal_rnDeriv hac)

theorem iid_pair_overlap_of_likelihood {Ω : Type*} [MeasurableSpace Ω] (μ Q R : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure Q] [IsProbabilityMeasure R] (L M : Ω → ℝ) (hL : Measurable L) (hM : Measurable M) (hL0 : ∀ x, 0 ≤ L x) (hM0 : ∀ x, 0 ≤ M x) (hQ : Q = μ.withDensity (fun x => ofReal (L x))) (hR : R = μ.withDensity (fun x => ofReal (M x))) (hpairInt : Integrable (fun x => L x * M x) μ) (n : ℕ) : (∫ x, (((Measure.pi (fun _ : Fin n => Q)).rnDeriv (Measure.pi (fun _ : Fin n => μ)) x).toReal) * (((Measure.pi (fun _ : Fin n => R)).rnDeriv (Measure.pi (fun _ : Fin n => μ)) x).toReal) ∂(Measure.pi (fun _ : Fin n => μ))) = (∫ x, L x * M x ∂μ) ^ n := by have hLeq : (fun x => (Q.rnDeriv μ x).toReal) =ᵐ[μ] L := by rw [hQ] filter_upwards [Measure.rnDeriv_withDensity μ hL.ennreal_ofReal] with x hx simp [hx, ENNReal.toReal_ofReal (hL0 x)] have hMeq : (fun x => (R.rnDeriv μ x).toReal) =ᵐ[μ] M := by rw [hR] filter_upwards [Measure.rnDeriv_withDensity μ hM.ennreal_ofReal] with x hx simp [hx, ENNReal.toReal_ofReal (hM0 x)] have hprod : (fun x => (Q.rnDeriv μ x).toReal * (R.rnDeriv μ x).toReal) =ᵐ[μ] (fun x => L x * M x) := by filter_upwards [hLeq, hMeq] with x hx hy simp [hx, hy] have hacQ : Q ≪ μ := by rw [hQ] exact withDensity_absolutelyContinuous μ _ have hacR : R ≪ μ := by rw [hR] exact withDensity_absolutelyContinuous μ _ have hint : Integrable (fun x => (Q.rnDeriv μ x).toReal * (R.rnDeriv μ x).toReal) μ := hpairInt.congr hprod.symm rw [iidPairOverlap μ Q R hacQ hacR n] congr 1 exact integral_congr_ae hprod

theorem two_channel_pair_overlap {Ω₁ Ω₂ : Type*} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (Q₁ R₁ : Measure Ω₁) (Q₂ R₂ : Measure Ω₂) [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂] [IsProbabilityMeasure Q₁] [IsProbabilityMeasure R₁] [IsProbabilityMeasure Q₂] [IsProbabilityMeasure R₂] (L₁ M₁ : Ω₁ → ℝ) (L₂ M₂ : Ω₂ → ℝ) (hL₁ : Measurable L₁) (hM₁ : Measurable M₁) (hL₂ : Measurable L₂) (hM₂ : Measurable M₂) (hL₁0 : ∀ x, 0 ≤ L₁ x) (hM₁0 : ∀ x, 0 ≤ M₁ x) (hL₂0 : ∀ x, 0 ≤ L₂ x) (hM₂0 : ∀ x, 0 ≤ M₂ x) (hQ₁ : Q₁ = μ₁.withDensity (fun x => ofReal (L₁ x))) (hR₁ : R₁ = μ₁.withDensity (fun x => ofReal (M₁ x))) (hQ₂ : Q₂ = μ₂.withDensity (fun x => ofReal (L₂ x))) (hR₂ : R₂ = μ₂.withDensity (fun x => ofReal (M₂ x))) (hInt₁ : Integrable (fun x => L₁ x * M₁ x) μ₁) (hInt₂ : Integrable (fun x => L₂ x * M₂ x) μ₂) (n₁ n₂ : ℕ) : (∫ x, ((((Measure.pi (fun _ : Fin n₁ => Q₁)).prod (Measure.pi (fun _ : Fin n₂ => Q₂))).rnDeriv ((Measure.pi (fun _ : Fin n₁ => μ₁)).prod (Measure.pi (fun _ : Fin n₂ => μ₂))) x).toReal) * ((((Measure.pi (fun _ : Fin n₁ => R₁)).prod (Measure.pi (fun _ : Fin n₂ => R₂))).rnDeriv ((Measure.pi (fun _ : Fin n₁ => μ₁)).prod (Measure.pi (fun _ : Fin n₂ => μ₂))) x).toReal) ∂((Measure.pi (fun _ : Fin n₁ => μ₁)).prod (Measure.pi (fun _ : Fin n₂ => μ₂)))) = (∫ x, L₁ x * M₁ x ∂μ₁) ^ n₁ * (∫ x, L₂ x * M₂ x ∂μ₂) ^ n₂ := by have hQ₁' := iid_absolutelyContinuous_of_likelihood μ₁ Q₁ L₁ hQ₁ n₁ have hR₁' := iid_absolutelyContinuous_of_likelihood μ₁ R₁ M₁ hR₁ n₁ have hQ₂' := iid_absolutelyContinuous_of_likelihood μ₂ Q₂ L₂ hQ₂ n₂ have hR₂' := iid_absolutelyContinuous_of_likelihood μ₂ R₂ M₂ hR₂ n₂ have hInt₁' := iid_pair_integrable_of_likelihood μ₁ Q₁ R₁ L₁ M₁ hL₁ hM₁ hL₁0 hM₁0 hQ₁ hR₁ hInt₁ n₁ have hInt₂' := iid_pair_integrable_of_likelihood μ₂ Q₂ R₂ L₂ M₂ hL₂ hM₂ hL₂0 hM₂0 hQ₂ hR₂ hInt₂ n₂ rw [product_pair_overlap (Measure.pi (fun _ : Fin n₁ => μ₁)) (Measure.pi (fun _ : Fin n₁ => Q₁)) (Measure.pi (fun _ : Fin n₁ => R₁)) (Measure.pi (fun _ : Fin n₂ => μ₂)) (Measure.pi (fun _ : Fin n₂ => Q₂)) (Measure.pi (fun _ : Fin n₂ => R₂)) hQ₁' hR₁' hQ₂' hR₂', iid_pair_overlap_of_likelihood μ₁ Q₁ R₁ L₁ M₁ hL₁ hM₁ hL₁0 hM₁0 hQ₁ hR₁ hInt₁ n₁, iid_pair_overlap_of_likelihood μ₂ Q₂ R₂ L₂ M₂ hL₂ hM₂ hL₂0 hM₂0 hQ₂ hR₂ hInt₂ n₂]

theorem one_add_chiSqDiv_uniformMixture_twoChannel_sign {Ω₁ Ω₂ : Type*} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] (K n₁ n₂ : ℕ) [NeZero K] (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (Q₁ : (Fin K → Bool) → Measure Ω₁) (Q₂ : (Fin K → Bool) → Measure Ω₂) [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂] [∀ s, IsProbabilityMeasure (Q₁ s)] [∀ s, IsProbabilityMeasure (Q₂ s)] (L₁ : (Fin K → Bool) → Ω₁ → ℝ) (L₂ : (Fin K → Bool) → Ω₂ → ℝ) (hL₁ : ∀ s, Measurable (L₁ s)) (hL₂ : ∀ s, Measurable (L₂ s)) (hL₁0 : ∀ s x, 0 ≤ L₁ s x) (hL₂0 : ∀ s x, 0 ≤ L₂ s x) (hQ₁ : ∀ s, Q₁ s = μ₁.withDensity (fun x => ofReal (L₁ s x))) (hQ₂ : ∀ s, Q₂ s = μ₂.withDensity (fun x => ofReal (L₂ s x))) (hInt₁ : ∀ s t, Integrable (fun x => L₁ s x * L₁ t x) μ₁) (hInt₂ : ∀ s t, Integrable (fun x => L₂ s x * L₂ t x) μ₂) (ρ₁ ρ₂ : ℝ) (hPair₁ : ∀ s t, (∫ x, L₁ s x * L₁ t x ∂μ₁) = 1 + ρ₁ * innerSign s t / (K : ℝ)) (hPair₂ : ∀ s t, (∫ x, L₂ s x * L₂ t x ∂μ₂) = 1 + ρ₂ * innerSign s t / (K : ℝ)) : 1 + chiSqDiv (uniformMixture (fun s => (Measure.pi (fun _ : Fin n₁ => Q₁ s)).prod (Measure.pi (fun _ : Fin n₂ => Q₂ s)))) ((Measure.pi (fun _ : Fin n₁ => μ₁)).prod (Measure.pi (fun _ : Fin n₂ => μ₂))) = (∑ s : Fin K → Bool, ∑ t : Fin K → Bool, (1 + ρ₁ * innerSign s t / (K : ℝ)) ^ n₁ * (1 + ρ₂ * innerSign s t / (K : ℝ)) ^ n₂) / (card (Fin K → Bool) : ℝ) ^ 2 := by classical have hac (s : Fin K → Bool) : (Measure.pi (fun _ : Fin n₁ => Q₁ s)).prod (Measure.pi (fun _ : Fin n₂ => Q₂ s)) ≪ (Measure.pi (fun _ : Fin n₁ => μ₁)).prod (Measure.pi (fun _ : Fin n₂ => μ₂)) := (iid_absolutelyContinuous_of_likelihood μ₁ (Q₁ s) (L₁ s) (hQ₁ s) n₁).prod (iid_absolutelyContinuous_of_likelihood μ₂ (Q₂ s) (L₂ s) (hQ₂ s) n₂) have hpair (s t : Fin K → Bool) : Integrable (fun x => (((Measure.pi (fun _ : Fin n₁ => Q₁ s)).prod (Measure.pi (fun _ : Fin n₂ => Q₂ s))).rnDeriv ((Measure.pi (fun _ : Fin n₁ => μ₁)).prod (Measure.pi (fun _ : Fin n₂ => μ₂))) x).toReal * (((Measure.pi (fun _ : Fin n₁ => Q₁ t)).prod (Measure.pi (fun _ : Fin n₂ => Q₂ t))).rnDeriv ((Measure.pi (fun _ : Fin n₁ => μ₁)).prod (Measure.pi (fun _ : Fin n₂ => μ₂))) x).toReal) ((Measure.pi (fun _ : Fin n₁ => μ₁)).prod (Measure.pi (fun _ : Fin n₂ => μ₂))) := by exact product_pair_integrable (Measure.pi (fun _ : Fin n₁ => μ₁)) (Measure.pi (fun _ : Fin n₁ => Q₁ s)) (Measure.pi (fun _ : Fin n₁ => Q₁ t)) (Measure.pi (fun _ : Fin n₂ => μ₂)) (Measure.pi (fun _ : Fin n₂ => Q₂ s)) (Measure.pi (fun _ : Fin n₂ => Q₂ t)) (iid_absolutelyContinuous_of_likelihood μ₁ (Q₁ s) (L₁ s) (hQ₁ s) n₁) (iid_absolutelyContinuous_of_likelihood μ₁ (Q₁ t) (L₁ t) (hQ₁ t) n₁) (iid_absolutelyContinuous_of_likelihood μ₂ (Q₂ s) (L₂ s) (hQ₂ s) n₂) (iid_absolutelyContinuous_of_likelihood μ₂ (Q₂ t) (L₂ t) (hQ₂ t) n₂) (iid_pair_integrable_of_likelihood μ₁ (Q₁ s) (Q₁ t) (L₁ s) (L₁ t) (hL₁ s) (hL₁ t) (hL₁0 s) (hL₁0 t) (hQ₁ s) (hQ₁ t) (hInt₁ s t) n₁) (iid_pair_integrable_of_likelihood μ₂ (Q₂ s) (Q₂ t) (L₂ s) (L₂ t) (hL₂ s) (hL₂ t) (hL₂0 s) (hL₂0 t) (hQ₂ s) (hQ₂ t) (hInt₂ s t) n₂) rw [one_add_chiSqDiv_uniformMixture (fun s => (Measure.pi (fun _ : Fin n₁ => Q₁ s)).prod (Measure.pi (fun _ : Fin n₂ => Q₂ s))) ((Measure.pi (fun _ : Fin n₁ => μ₁)).prod (Measure.pi (fun _ : Fin n₂ => μ₂))) hac hpair] congr 1 apply Finset.sum_congr rfl intro s _ apply Finset.sum_congr rfl intro t _ rw [two_channel_pair_overlap μ₁ μ₂ (Q₁ s) (Q₁ t) (Q₂ s) (Q₂ t) (L₁ s) (L₁ t) (L₂ s) (L₂ t) (hL₁ s) (hL₁ t) (hL₂ s) (hL₂ t) (hL₁0 s) (hL₁0 t) (hL₂0 s) (hL₂0 t) (hQ₁ s) (hQ₁ t) (hQ₂ s) (hQ₂ t) (hInt₁ s t) (hInt₂ s t) n₁ n₂, hPair₁ s t, hPair₂ s t]