Stat.Minimax.Mixture.Poisson­Latent­Sign

theorem factor_bounds {τ u ell σ : ℝ} (hτ : |τ| ≤ 1 / 4) (hu : |u| ≤ 1) (hell : |ell| = 1) (hσ : |σ| = 1) : 3 / 4 ≤ 1 + τ * ell * u * σ ∧ 1 + τ * ell * u * σ ≤ 5 / 4 := by have hmul : |τ * ell * u * σ| ≤ 1 / 4 := by simp only [abs_mul, hell, hσ, mul_one] exact (mul_le_mul_of_nonneg_left hu (abs_nonneg τ)).trans (by simpa using hτ) have hb := abs_le.mp hmul constructor <;> linarith

theorem denominator_lower {m : ℕ} {τ : ℝ} {c : Cell m} (hτ : |τ| ≤ 1 / 4) (hu : ∀ i, |c.1 i| ≤ 1) : 2 * (3 / 4 : ℝ) ^ m ≤ denominator τ c := by have hl (ell : ℝ) (hell : |ell| = 1) : (3 / 4 : ℝ) ^ m ≤ signLikelihood τ c ell := by have hs (i : Fin m) : |sign (c.2.1 i)| = 1 := by cases c.2.1 i <;> simp [sign] simpa only [signLikelihood, Finset.prod_const, Finset.card_univ, Fintype.card_fin] using (Finset.prod_le_prod (s := univ) (f := fun _ : Fin m => (3 / 4 : ℝ)) (by intros; norm_num) (fun i _ => (factor_bounds hτ (hu i) hell (hs i)).1)) have hp := hl 1 (by norm_num) have hn := hl (-1) (by norm_num) unfold denominator linarith

theorem denominator_pos {m : ℕ} {τ : ℝ} {c : Cell m} (hτ : |τ| ≤ 1 / 4) (hu : ∀ i, |c.1 i| ≤ 1) : 0 < denominator τ c := by have h := denominator_lower hτ hu have hp : 0 < 2 * (3 / 4 : ℝ) ^ m := by positivity linarith

theorem posterior_empty {m : ℕ} {τ : ℝ} {c : Cell m} (hτ : |τ| ≤ 1 / 4) (hu : ∀ i, |c.1 i| ≤ 1) : posterior τ c ∅ = 1 := by have hn := ne_of_gt (denominator_pos hτ hu) unfold posterior simp only [Finset.prod_empty, mul_one] change denominator τ c / denominator τ c = 1 exact div_self hn

theorem posterior_singleton_cancel {m : ℕ} {τ : ℝ} {c : Cell m} (hτ : |τ| ≤ 1 / 4) (hu : ∀ i, |c.1 i| ≤ 1) {i : Fin m} (hi : i ∈ active c) : posterior τ c {i} = c.1 i * ((∏ j ∈ Finset.univ.erase i, (1 + τ * c.1 j * sign (c.2.1 j))) - (∏ j ∈ Finset.univ.erase i, (1 - τ * c.1 j * sign (c.2.1 j)))) / denominator τ c := by have hai : c.2.1 i = true := (Finset.mem_filter.mp hi).2 have hp : 1 + τ * c.1 i ≠ 0 := by have h := (factor_bounds hτ (hu i) (ell := 1) (σ := 1) (by norm_num) (by norm_num)).1 simp only [mul_one] at h linarith have hn : 1 - τ * c.1 i ≠ 0 := by have h := (factor_bounds hτ (hu i) (ell := -1) (σ := 1) (by norm_num) (by norm_num)).1 simp only [mul_one, mul_neg_one, neg_mul] at h linarith have hsign : sign (c.2.1 i) = 1 := by simp [sign, hai] have hplus : signLikelihood τ c 1 = (1 + τ * c.1 i) * ∏ j ∈ Finset.univ.erase i, (1 + τ * c.1 j * sign (c.2.1 j)) := by simpa only [signLikelihood, mul_one, hsign] using (Finset.mul_prod_erase (s := univ) (f := fun j => 1 + τ * c.1 j * sign (c.2.1 j)) (Finset.mem_univ i)).symm have hminus : signLikelihood τ c (-1) = (1 - τ * c.1 i) * ∏ j ∈ Finset.univ.erase i, (1 - τ * c.1 j * sign (c.2.1 j)) := by simpa only [signLikelihood, mul_neg_one, neg_mul, ← sub_eq_add_neg, hsign, mul_one] using (Finset.mul_prod_erase (s := univ) (f := fun j => 1 - τ * c.1 j * sign (c.2.1 j)) (Finset.mem_univ i)).symm unfold posterior simp only [Finset.prod_singleton] rw [hplus, hminus] congr 1 field_simp [hp, hn] ring

theorem opposite_products_bound {ι : Type*} (s : Finset ι) (v : ι → ℝ) {τ : ℝ} (hτ : |τ| ≤ 1 / 4) (hv : ∀ i ∈ s, |v i| ≤ 1) : |(∏ i ∈ s, (1 + τ * v i)) - (∏ i ∈ s, (1 - τ * v i))| ≤ 2 * |τ| * (s.card : ℝ) * (5 / 4 : ℝ) ^ s.card := by classical have hfactor (i : ι) (hi : i ∈ s) : |1 + τ * v i| ≤ 5 / 4 ∧ |1 - τ * v i| ≤ 5 / 4 := by have hp := factor_bounds hτ (hv i hi) (ell := 1) (σ := 1) (by norm_num) (by norm_num) have hn := factor_bounds hτ (hv i hi) (ell := -1) (σ := 1) (by norm_num) (by norm_num) simp only [mul_one, mul_neg_one, neg_mul, ← sub_eq_add_neg] at hp hn constructor <;> rw [abs_of_nonneg (by linarith)] <;> linarith have hprod (t : Finset ι) (ht : t ⊆ s) : |∏ i ∈ t, (1 - τ * v i)| ≤ (5 / 4 : ℝ) ^ t.card := by rw [Finset.abs_prod] simpa only [Finset.prod_const] using (Finset.prod_le_prod (fun _ _ => abs_nonneg _) (fun i hi => (hfactor i (ht hi)).2)) induction s using Finset.induction_on with | empty => simp | @insert a t ha ih => have hva := hv a (Finset.mem_insert_self a t) have hvt : ∀ i ∈ t, |v i| ≤ 1 := fun i hi => hv i (Finset.mem_insert_of_mem hi) have hd := ih hvt (fun i hi => hfactor i (Finset.mem_insert_of_mem hi)) (fun u hu => hprod u (hu.trans (Finset.subset_insert a t))) have hpa := (hfactor a (Finset.mem_insert_self a t)).1 have hpt := hprod t (Finset.subset_insert a t) have hdiff : |2 * τ * v a| ≤ 2 * |τ| := by rw [abs_mul, abs_mul] norm_num exact mul_le_of_le_one_right (by positivity) hva rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.card_insert_of_notMem ha, Nat.cast_add, Nat.cast_one, pow_succ] calc |(1 + τ * v a) * (∏ i ∈ t, (1 + τ * v i)) - (1 - τ * v a) * (∏ i ∈ t, (1 - τ * v i))| = |(1 + τ * v a) * ((∏ i ∈ t, (1 + τ * v i)) - (∏ i ∈ t, (1 - τ * v i))) + (2 * τ * v a) * (∏ i ∈ t, (1 - τ * v i))| := by congr 1; ring _ ≤ |1 + τ * v a| * |(∏ i ∈ t, (1 + τ * v i)) - (∏ i ∈ t, (1 - τ * v i))| + |2 * τ * v a| * |∏ i ∈ t, (1 - τ * v i)| := by simpa only [abs_mul] using abs_add_le ((1 + τ * v a) * ((∏ i ∈ t, (1 + τ * v i)) - (∏ i ∈ t, (1 - τ * v i)))) ((2 * τ * v a) * (∏ i ∈ t, (1 - τ * v i))) _ ≤ (5 / 4) * (2 * |τ| * (t.card : ℝ) * (5 / 4 : ℝ) ^ t.card) + (2 * |τ|) * (5 / 4 : ℝ) ^ t.card := by exact add_le_add (mul_le_mul hpa hd (abs_nonneg _) (by norm_num)) (mul_le_mul hdiff hpt (abs_nonneg _) (by positivity)) _ ≤ 2 * |τ| * ((t.card : ℝ) + 1) * ((5 / 4 : ℝ) ^ t.card * (5 / 4)) := by have hp : 0 ≤ |τ| * (5 / 4 : ℝ) ^ t.card := by positivity nlinarith

theorem posterior_singleton_bound {m : ℕ} {τ : ℝ} {c : Cell m} (hτ : |τ| ≤ 1 / 4) (hu : ∀ i, |c.1 i| ≤ 1) {i : Fin m} (hi : i ∈ active c) : |posterior τ c {i}| ≤ |τ| * ((m - 1 : ℕ) : ℝ) * (5 / 3 : ℝ) ^ m := by have hs (j : Fin m) : |sign (c.2.1 j)| = 1 := by cases c.2.1 j <;> simp [sign] have hv (j : Fin m) : |c.1 j * sign (c.2.1 j)| ≤ 1 := by simpa only [abs_mul, hs j, mul_one] using hu j have hb := opposite_products_bound (Finset.univ.erase i) (fun j => c.1 j * sign (c.2.1 j)) hτ (fun j _ => hv j) have hcard : (Finset.univ.erase i).card = m - 1 := by simp simp only [hcard, ← mul_assoc] at hb have hpow : (5 / 4 : ℝ) ^ (m - 1) ≤ (5 / 4 : ℝ) ^ m := pow_le_pow_right₀ (by norm_num) (sub_le m 1) have hb' := hb.trans (mul_le_mul_of_nonneg_left hpow (by positivity : 0 ≤ 2 * |τ| * ((m - 1 : ℕ) : ℝ))) rw [posterior_singleton_cancel hτ hu hi, abs_div, abs_mul, abs_of_pos (denominator_pos hτ hu)] apply (div_le_iff₀ (denominator_pos hτ hu)).2 calc |c.1 i| * |(∏ j ∈ Finset.univ.erase i, (1 + τ * c.1 j * sign (c.2.1 j))) - (∏ j ∈ Finset.univ.erase i, (1 - τ * c.1 j * sign (c.2.1 j)))| ≤ 2 * |τ| * ((m - 1 : ℕ) : ℝ) * (5 / 4 : ℝ) ^ m := (mul_le_of_le_one_left (abs_nonneg _) (hu i)).trans hb' _ = (|τ| * ((m - 1 : ℕ) : ℝ) * (5 / 3 : ℝ) ^ m) * (2 * (3 / 4 : ℝ) ^ m) := by have he : (5 / 3 : ℝ) ^ m * (3 / 4 : ℝ) ^ m = (5 / 4 : ℝ) ^ m := by rw [← mul_pow]; norm_num calc _ = 2 * |τ| * ((m - 1 : ℕ) : ℝ) * ((5 / 3 : ℝ) ^ m * (3 / 4 : ℝ) ^ m) := by rw [he] _ = _ := by ring _ ≤ (|τ| * ((m - 1 : ℕ) : ℝ) * (5 / 3 : ℝ) ^ m) * denominator τ c := mul_le_mul_of_nonneg_left (denominator_lower hτ hu) (by positivity)

theorem posterior_singleton_one {τ : ℝ} {c : Cell 1} (hτ : |τ| ≤ 1 / 4) (hu : ∀ i, |c.1 i| ≤ 1) {i : Fin 1} (hi : i ∈ active c) : posterior τ c {i} = 0 := by have h := posterior_singleton_bound hτ hu hi simpa using abs_nonpos_iff.mp (by simpa using h)

theorem posterior_subset_bound {m : ℕ} {τ : ℝ} {c : Cell m} (hτ : |τ| ≤ 1 / 4) (hu : ∀ i, |c.1 i| ≤ 1) (S : Finset (Fin m)) : |posterior τ c S| ≤ (2 : ℝ) ^ S.card := by have hf (i : Fin m) : |c.1 i / (1 + τ * c.1 i)| ≤ 2 ∧ |(-c.1 i) / (1 - τ * c.1 i)| ≤ 2 := by have hp := (factor_bounds hτ (hu i) (ell := 1) (σ := 1) (by norm_num) (by norm_num)).1 have hn := (factor_bounds hτ (hu i) (ell := -1) (σ := 1) (by norm_num) (by norm_num)).1 simp only [mul_one, mul_neg_one, neg_mul, ← sub_eq_add_neg] at hp hn have hpp : 0 < 1 + τ * c.1 i := by linarith have hnp : 0 < 1 - τ * c.1 i := by linarith constructor · rw [abs_div, abs_of_pos hpp] apply (div_le_iff₀ hpp).2 linarith [hu i] · rw [abs_div, abs_neg, abs_of_pos hnp] apply (div_le_iff₀ hnp).2 linarith [hu i] have hp : |∏ i ∈ S, c.1 i / (1 + τ * c.1 i)| ≤ (2 : ℝ) ^ S.card := by rw [Finset.abs_prod] simpa only [Finset.prod_const] using (Finset.prod_le_prod (fun _ _ => abs_nonneg _) (fun i _ => (hf i).1)) have hn : |∏ i ∈ S, (-c.1 i) / (1 - τ * c.1 i)| ≤ (2 : ℝ) ^ S.card := by rw [Finset.abs_prod] simpa only [Finset.prod_const] using (Finset.prod_le_prod (fun _ _ => abs_nonneg _) (fun i _ => (hf i).2)) have hL (ell : ℝ) (hell : |ell| = 1) : 0 ≤ signLikelihood τ c ell := by apply Finset.prod_nonneg intro i _ have hs : |sign (c.2.1 i)| = 1 := by cases c.2.1 i <;> simp [sign] have h := (factor_bounds hτ (hu i) hell hs).1 linarith have hLp := hL 1 (by norm_num) have hLn := hL (-1) (by norm_num) unfold posterior rw [abs_div, abs_of_pos (denominator_pos hτ hu)] apply (div_le_iff₀ (denominator_pos hτ hu)).2 calc _ ≤ |signLikelihood τ c 1 * (∏ i ∈ S, c.1 i / (1 + τ * c.1 i))| + |signLikelihood τ c (-1) * (∏ i ∈ S, (-c.1 i) / (1 - τ * c.1 i))| := abs_add_le _ _ _ = signLikelihood τ c 1 * |∏ i ∈ S, c.1 i / (1 + τ * c.1 i)| + signLikelihood τ c (-1) * |∏ i ∈ S, (-c.1 i) / (1 - τ * c.1 i)| := by rw [abs_mul, abs_mul, abs_of_nonneg hLp, abs_of_nonneg hLn] _ ≤ signLikelihood τ c 1 * (2 : ℝ) ^ S.card + signLikelihood τ c (-1) * (2 : ℝ) ^ S.card := add_le_add (mul_le_mul_of_nonneg_left hp hLp) (mul_le_mul_of_nonneg_left hn hLn) _ = (2 : ℝ) ^ S.card * denominator τ c := by unfold denominator; ring

theorem subsetEnergy_le_choose {m : ℕ} {τ : ℝ} {c : Cell m} (hτ : |τ| ≤ 1 / 4) (hu : ∀ i, |c.1 i| ≤ 1) (d : ℕ) : subsetEnergy τ c d ≤ (4 : ℝ) ^ d * (m.choose d : ℝ) := by have hcount : ((selected c).powersetCard d).card ≤ m.choose d := by simpa only [Finset.card_powersetCard, Finset.card_univ, Fintype.card_fin] using (Finset.card_le_card (Finset.powersetCard_mono (Finset.subset_univ (selected c)))) have hterm (S : Finset (Fin m)) (hS : S ∈ (selected c).powersetCard d) : (posterior τ c S) ^ 2 ≤ (4 : ℝ) ^ d := by have hcard := (Finset.mem_powersetCard.mp hS).2 have h := (sq_le_sq₀ (abs_nonneg (posterior τ c S)) (by positivity : 0 ≤ (2 : ℝ) ^ S.card)).2 (posterior_subset_bound hτ hu S) rw [sq_abs, ← pow_mul, Nat.mul_comm, pow_mul, hcard] at h norm_num at h ⊢ exact h calc subsetEnergy τ c d ≤ ∑ S ∈ (selected c).powersetCard d, (4 : ℝ) ^ d := Finset.sum_le_sum hterm _ = (((selected c).powersetCard d).card : ℝ) * (4 : ℝ) ^ d := by simp only [Finset.sum_const, nsmul_eq_mul] _ ≤ (m.choose d : ℝ) * (4 : ℝ) ^ d := mul_le_mul_of_nonneg_right (by exact_mod_cast hcount) (by positivity) _ = (4 : ℝ) ^ d * (m.choose d : ℝ) := mul_comm _ _

@[fun_prop] theorem measurable_subsetEnergy (m d : ℕ) (τ : ℝ) : Measurable (fun c : Cell m => subsetEnergy τ c d) := by classical have hsign : Measurable sign := measurable_of_countable sign have hp (S : Finset (Fin m)) : Measurable (fun c : Cell m => (posterior τ c S) ^ 2) := by unfold posterior denominator signLikelihood fun_prop have hsel (S : Finset (Fin m)) : MeasurableSet {c : Cell m | S ⊆ selected c} := by have hflags : Measurable (fun c : Cell m => c.2.2) := measurable_snd.comp measurable_snd have hset : MeasurableSet {b : Fin m → Bool | S ⊆ Finset.univ.filter (fun i => b i = true)} := (Set.to_countable _).measurableSet exact hset.preimage hflags have heq (c : Cell m) : subsetEnergy τ c d = ∑ S ∈ (Finset.univ : Finset (Fin m)).powersetCard d, if S ⊆ selected c then (posterior τ c S) ^ 2 else 0 := by rw [← Finset.sum_filter] unfold subsetEnergy congr 1 ext S simp only [mem_filter, Finset.mem_powersetCard, Finset.subset_univ, true_and] exact and_comm simp_rw [heq] apply Finset.measurable_sum intro S _ exact Measurable.ite (hsel S) (hp S) measurable_const

theorem overlapSeries_summable_abs {t : ℕ → ℝ} {b : ℝ} (ht : ∀ d, 1 ≤ d → 0 ≤ t d ∧ t d ≤ b ^ d / (d.factorial : ℝ)) (z : ℝ) : Summable (fun d : ℕ => |t (d + 1) * z ^ (d + 1)|) := by have hs := (summable_nat_add_iff 1).2 (Real.summable_pow_div_factorial (b * |z|)) refine hs.of_nonneg_of_le (fun _ => abs_nonneg _) (fun d => ?_) rw [abs_mul, abs_of_nonneg (ht (d + 1) (by omega)).1, abs_pow] calc t (d + 1) * |z| ^ (d + 1) ≤ (b ^ (d + 1) / ((d + 1).factorial : ℝ)) * |z| ^ (d + 1) := mul_le_mul_of_nonneg_right (ht (d + 1) (by omega)).2 (by positivity) _ = (b * |z|) ^ (d + 1) / ((d + 1).factorial : ℝ) := by rw [mul_pow]; ring

theorem overlapSeries_remainder {t : ℕ → ℝ} {b z : ℝ} (hb : 0 ≤ b) (ht : ∀ d, 1 ≤ d → 0 ≤ t d ∧ t d ≤ b ^ d / (d.factorial : ℝ)) (hr : b * |z| ≤ 1 / 2) : |overlapSeries t z - 1 - t 1 * z| ≤ b ^ 2 * z ^ 2 := by -- The d≥2 tail is at most r² ∑n r^n/(n+2)! ≤ r² for r≤1/2. have hsabs := overlapSeries_summable_abs ht z have hs : Summable (fun d : ℕ => t (d + 1) * z ^ (d + 1)) := by exact (by simpa only [Real.norm_eq_abs] using hsabs : Summable (fun d : ℕ => ‖t (d + 1) * z ^ (d + 1)‖)).of_norm have hsplit := hs.sum_add_tsum_nat_add 1 simp only [Finset.sum_range_one, zero_add, pow_one, Nat.add_assoc] at hsplit have heq : overlapSeries t z - 1 - t 1 * z = ∑' d : ℕ, t (d + 2) * z ^ (d + 2) := by unfold overlapSeries linarith rw [heq] have htail : Summable (fun d : ℕ => |t (d + 2) * z ^ (d + 2)|) := by simpa only [Nat.add_assoc] using (summable_nat_add_iff 1).2 hsabs have hgeom : Summable (fun d : ℕ => (b * |z|) ^ 2 / 2 * (1 / 2 : ℝ) ^ d) := (summable_geometric_of_abs_lt_one (by norm_num : |(1 / 2 : ℝ)| < 1)).mul_left _ have hbound : ∀ d : ℕ, |t (d + 2) * z ^ (d + 2)| ≤ (b * |z|) ^ 2 / 2 * (1 / 2 : ℝ) ^ d := by intro d have hf : (2 : ℝ) ≤ ((d + 2).factorial : ℝ) := by exact_mod_cast (show 2 ≤ (d + 2).factorial from by simpa using Nat.factorial_le (show 2 ≤ d + 2 by omega)) rw [abs_mul, abs_of_nonneg (ht (d + 2) (by omega)).1, abs_pow] calc t (d + 2) * |z| ^ (d + 2) ≤ (b ^ (d + 2) / ((d + 2).factorial : ℝ)) * |z| ^ (d + 2) := mul_le_mul_of_nonneg_right (ht (d + 2) (by omega)).2 (by positivity) _ = (b * |z|) ^ (d + 2) / ((d + 2).factorial : ℝ) := by rw [mul_pow]; ring _ ≤ (b * |z|) ^ (d + 2) / 2 := div_le_div_of_nonneg_left (by positivity) (by norm_num) hf _ = (b * |z|) ^ 2 / 2 * (b * |z|) ^ d := by rw [pow_add]; ring _ ≤ (b * |z|) ^ 2 / 2 * (1 / 2 : ℝ) ^ d := mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (by positivity) hr d) (by positivity) calc |∑' d : ℕ, t (d + 2) * z ^ (d + 2)| ≤ ∑' d : ℕ, |t (d + 2) * z ^ (d + 2)| := by simpa only [Real.norm_eq_abs] using norm_tsum_le_tsum_norm (f := fun d : ℕ => t (d + 2) * z ^ (d + 2)) (by simpa only [Real.norm_eq_abs] using htail) _ ≤ ∑' d : ℕ, (b * |z|) ^ 2 / 2 * (1 / 2 : ℝ) ^ d := htail.tsum_le_tsum hbound hgeom _ = b ^ 2 * z ^ 2 := by rw [tsum_mul_left, tsum_geometric_of_abs_lt_one (by norm_num)] simp only [mul_pow, sq_abs] ring

theorem overlapSeries_pos {t : ℕ → ℝ} {b z : ℝ} (hb : 0 ≤ b) (ht : ∀ d, 1 ≤ d → 0 ≤ t d ∧ t d ≤ b ^ d / (d.factorial : ℝ)) (hr : b * |z| ≤ 1 / 2) : 0 < overlapSeries t z := by -- Use the remainder bound and |t₁z|≤r: K≥1-r-r²≥1/4. have ht1 := ht 1 (by omega) simp only [pow_one, Nat.factorial_one, Nat.cast_one, div_one] at ht1 have hlin : |t 1 * z| ≤ b * |z| := by rw [abs_mul, abs_of_nonneg ht1.1] exact mul_le_mul_of_nonneg_right ht1.2 (abs_nonneg z) have hrem := (abs_le.mp (overlapSeries_remainder hb ht hr)).1 have hlinlow := (abs_le.mp hlin).1 have hr0 : 0 ≤ b * |z| := mul_nonneg hb (abs_nonneg z) have hsq : b ^ 2 * z ^ 2 = (b * |z|) ^ 2 := by rw [mul_pow, sq_abs] rw [hsq] at hrem nlinarith

theorem integrable_subsetEnergy (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] {τ : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (m d : ℕ) : Integrable (fun c => subsetEnergy τ c d) (ν m) := by -- Dominate by 4^d * choose m d, using measurable_subsetEnergy. refine (integrable_const ((4 : ℝ) ^ d * (m.choose d : ℝ))).mono' (measurable_subsetEnergy m d τ).aestronglyMeasurable ?_ filter_upwards [hν m] with c hc simpa only [Real.norm_eq_abs, abs_of_nonneg (subsetEnergy_nonneg τ c d)] using subsetEnergy_le_choose hτ hc.1 d

theorem integrable_conditionalEnergy (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] (ξ : NNReal) {τ : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (d : ℕ) : Integrable (fun m => conditionalEnergy ν τ m d) (poissonMeasure ξ) := by -- First bound each conditional integral between zero and 4^d * choose m d. -- Its measurability follows from the discrete Nat domain. Apply Integrable.mono' -- with (integrable_poisson_choose ξ d).const_mul (4^d). refine ((integrable_poisson_choose ξ d).const_mul ((4 : ℝ) ^ d)).mono' (measurable_of_countable _).aestronglyMeasurable ?_ apply Filter.Eventually.of_forall intro m have hn : 0 ≤ conditionalEnergy ν τ m d := integral_nonneg (fun c => subsetEnergy_nonneg τ c d) simpa only [Real.norm_eq_abs, abs_of_nonneg hn] using conditionalEnergy_le_choose ν hτ hν m d

theorem coefficient_nonneg (ν : ∀ m, Measure (Cell m)) (ξ : NNReal) (τ γ : ℝ) (d : ℕ) : 0 ≤ coefficient ν ξ τ γ d := by unfold coefficient conditionalEnergy apply mul_nonneg · rw [mul_comm 2 d, pow_mul] exact sq_nonneg _ · exact integral_nonneg (fun _ => integral_nonneg (fun _ => subsetEnergy_nonneg _ _ _))

theorem coefficient_le_factorial (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] (ξ : NNReal) {τ : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (γ : ℝ) (d : ℕ) : coefficient ν ξ τ γ d ≤ (4 * (ξ : ℝ) * γ ^ 2) ^ d / (d.factorial : ℝ) := by -- Apply integral_mono_ae at each conditional law and then at poissonMeasure ξ. -- Use the two integrability receipts above and integral_poisson_choose. -- Normalize γ^(2*d)=(γ^2)^d only after multiplying the nonnegative bound. have hb : (∫ m : ℕ, conditionalEnergy ν τ m d ∂poissonMeasure ξ) ≤ (4 : ℝ) ^ d * ((ξ : ℝ) ^ d / (d.factorial : ℝ)) := by calc _ ≤ ∫ m : ℕ, (4 : ℝ) ^ d * (m.choose d : ℝ) ∂poissonMeasure ξ := integral_mono_ae (integrable_conditionalEnergy ν ξ hτ hν d) ((integrable_poisson_choose ξ d).const_mul _) <| Filter.Eventually.of_forall (fun m => conditionalEnergy_le_choose ν hτ hν m d) _ = _ := by rw [integral_const_mul, integral_poisson_choose] have hg : 0 ≤ γ ^ (2 * d) := by rw [pow_mul] positivity unfold coefficient calc _ ≤ γ ^ (2 * d) * ((4 : ℝ) ^ d * ((ξ : ℝ) ^ d / (d.factorial : ℝ))) := mul_le_mul_of_nonneg_left hb hg _ = _ := by rw [pow_mul, mul_pow, mul_pow]; ring

theorem coefficient_summable_abs (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] (ξ : NNReal) {τ : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (γ z : ℝ) : Summable (fun d : ℕ => |coefficient ν ξ τ γ (d + 1) * z ^ (d + 1)|) := by exact overlapSeries_summable_abs (b := 4 * (ξ : ℝ) * γ ^ 2) (fun d _ => ⟨coefficient_nonneg ν ξ τ γ d, coefficient_le_factorial ν ξ hτ hν γ d⟩) z

theorem summable_integral_abs_energy_terms (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] (ξ : NNReal) {τ : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (γ z : ℝ) : Summable (fun d : ℕ => ∫ m : ℕ, ∫ c, |γ ^ (2 * (d + 1)) * subsetEnergy τ c (d + 1) * z ^ (d + 1)| ∂ν m ∂poissonMeasure ξ) := by -- Nonnegative energy gives |γ^(2*d)*energy*z^d| = γ^(2*d)*energy*|z|^d. -- Pull constants through both integrals to identify the summand with -- |coefficient ν ξ τ γ (d+1) * z^(d+1)|; use coefficient_summable_abs. apply (coefficient_summable_abs ν ξ hτ hν γ z).congr intro d have hg : 0 ≤ γ ^ (2 * (d + 1)) := by rw [pow_mul]; positivity have hc (m : ℕ) := integrable_subsetEnergy ν hτ hν m (d + 1) have hm := integrable_conditionalEnergy ν ξ hτ hν (d + 1) have he (m : ℕ) : (∫ c, |γ ^ (2 * (d + 1)) * subsetEnergy τ c (d + 1) * z ^ (d + 1)| ∂ν m) = |z| ^ (d + 1) * (γ ^ (2 * (d + 1)) * conditionalEnergy ν τ m (d + 1)) := by simp_rw [abs_mul, abs_of_nonneg hg, abs_of_nonneg (subsetEnergy_nonneg τ _ _), abs_pow] calc _ = ∫ c, |z| ^ (d + 1) • (γ ^ (2 * (d + 1)) • subsetEnergy τ c (d + 1)) ∂ν m := by congr 1 funext c simp only [smul_eq_mul] ring _ = _ := by have hγ := (hc m).integral_smul (γ ^ (2 * (d + 1))) have hz := ((hc m).const_mul (γ ^ (2 * (d + 1)))).integral_smul (|z| ^ (d + 1)) simp only [smul_eq_mul] at hγ hz ⊢ rw [hz, hγ] rfl simp_rw [he] have hz := (hm.const_mul (γ ^ (2 * (d + 1)))).integral_smul (|z| ^ (d + 1)) have hγ := hm.integral_smul (γ ^ (2 * (d + 1))) simp only [smul_eq_mul] at hz hγ rw [hz] change |coefficient ν ξ τ γ (d + 1) * z ^ (d + 1)| = _ rw [abs_mul, abs_of_nonneg (coefficient_nonneg ν ξ τ γ (d + 1)), abs_pow] unfold coefficient rw [hγ] ring

theorem poisson_overlap_pos (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] (ξ : NNReal) {τ γ z : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (hr : 4 * (ξ : ℝ) * γ ^ 2 * |z| ≤ 1 / 2) : 0 < overlapSeries (coefficient ν ξ τ γ) z := by exact overlapSeries_pos (b := 4 * (ξ : ℝ) * γ ^ 2) (by positivity) (fun d _ => ⟨coefficient_nonneg ν ξ τ γ d, coefficient_le_factorial ν ξ hτ hν γ d⟩) hr

theorem outcomeLikelihood_expansion {m : ℕ} (τ γ : ℝ) (c : Cell m) (v : Fin m → ℝ) : outcomeLikelihood τ γ c v = ∑ S ∈ (selected c).powerset, γ ^ S.card * posterior τ c S * ∏ i ∈ S, v i := by -- Finset.prod_one_add followed by distributing the posterior weights. -- This algebraic identity needs no denominator nonzero assumption: distribute -- division across the finite sum rather than canceling the denominator. classical unfold outcomeLikelihood posterior simp only [Finset.prod_one_add, Finset.prod_mul_distrib, Finset.prod_const, Finset.mul_sum] rw [← Finset.sum_add_distrib, Finset.sum_div] apply Finset.sum_congr rfl intro S _ ring

theorem integrable_subset_pair {ι Ω : Type*} [MeasurableSpace Ω] {ρ : Measure Ω} [IsProbabilityMeasure ρ] {v w : ι → Ω → ℝ} {z : ℝ} (h : CenteredOutcomePair ρ v w z) (S R : Finset ι) : Integrable (fun ω => (∏ i ∈ S, v i ω) * ∏ i ∈ R, w i ω) ρ := by -- Regroup as a product on S∪R of v, w, or vw; reuse independent integration. -- Use the measurable map (x,y) ↦ (if i∈S then x else 1) * -- (if i∈R then y else 1) on each jointly independent pair. The integrability -- fields cover all membership cases; restrict the resulting family to S∪R. classical simp_rw [subset_pair_regroup S R] exact integrable_independent_finset (independent_union_factors h S R) (integrable_union_factor h S R) (S ∪ R)

theorem integral_subset_pair {ι Ω : Type*} [DecidableEq ι] [MeasurableSpace Ω] {ρ : Measure Ω} [IsProbabilityMeasure ρ] {v w : ι → Ω → ℝ} {z : ℝ} (h : CenteredOutcomePair ρ v w z) (S R : Finset ι) : (∫ ω, (∏ i ∈ S, v i ω) * ∏ i ∈ R, w i ω ∂ρ) = if S = R then z ^ S.card else 0 := by -- For the same regrouped union product, use -- iIndepFun.integral_fun_prod_eq_prod_integral on the union subtype. -- When S≠R, a symmetric-difference index contributes a centered zero factor. classical let f : ι → Ω → ℝ := fun i ω => (if i ∈ S then v i ω else 1) * (if i ∈ R then w i ω else 1) have hi : ∀ i, Integrable (f i) ρ := integrable_union_factor h S R have hind : iIndepFun f ρ := independent_union_factors h S R have hfactor : (∫ ω, (∏ i ∈ S, v i ω) * ∏ i ∈ R, w i ω ∂ρ) = ∏ i ∈ S ∪ R, ∫ ω, f i ω ∂ρ := by simp_rw [subset_pair_regroup S R] have hind' := hind.precomp (g := fun i : ↥(S ∪ R) => (i : ι)) val_injective change (∫ ω, ∏ i ∈ S ∪ R, f i ω ∂ρ) = _ simp_rw [← Finset.prod_coe_sort (S ∪ R)] exact hind'.integral_fun_prod_eq_prod_integral (fun i => (hi i).aestronglyMeasurable) rw [hfactor] by_cases heq : S = R · subst R simp only [Finset.union_self] calc (∏ i ∈ S, ∫ ω, f i ω ∂ρ) = ∏ _i ∈ S, z := by apply Finset.prod_congr rfl intro i hiS simpa [f, hiS] using h.overlap i _ = z ^ S.card := Finset.prod_const _ · rw [if_neg heq] have hex : ∃ i, (i ∈ S ∧ i ∉ R) ∨ (i ∈ R ∧ i ∉ S) := by by_contra hn apply heq ext i have hh := (not_exists.mp hn) i constructor <;> intro hi · by_contra hr; exact hh (inl ⟨hi, hr⟩) · by_contra hs; exact hh (inr ⟨hi, hs⟩) obtain ⟨i, hi⟩ := hex apply Finset.prod_eq_zero (i := i) · rcases hi with hi | hi · exact mem_union_left R hi.1 · exact mem_union_right S hi.1 · rcases hi with hi | hi · simpa [f, hi.1, hi.2] using h.centered_left i · simpa [f, hi.1, hi.2] using h.centered_right i

theorem integrable_outcomeLikelihood_pair {m : ℕ} {Ω : Type*} [MeasurableSpace Ω] {ρ : Measure Ω} [IsProbabilityMeasure ρ] {v w : Fin m → Ω → ℝ} {z : ℝ} (h : CenteredOutcomePair ρ v w z) (τ γ : ℝ) (c : Cell m) : Integrable (fun ω => outcomeLikelihood τ γ c (fun i => v i ω) * outcomeLikelihood τ γ c (fun i => w i ω)) ρ := by -- Expand both finite likelihood sums and use integrable_subset_pair for each -- double-sum term. No boundedness of outcome scores is needed. classical simp_rw [outcomeLikelihood_expansion, Finset.sum_mul, Finset.mul_sum] apply integrable_finsetSum intro S _ apply integrable_finsetSum intro R _ convert (integrable_subset_pair h S R).const_mul ((γ ^ S.card * posterior τ c S) * (γ ^ R.card * posterior τ c R)) using 1 <;> first | rfl | (funext ω; ring)

theorem integral_outcomeLikelihood_pair {m : ℕ} {Ω : Type*} [MeasurableSpace Ω] {ρ : Measure Ω} [IsProbabilityMeasure ρ] {v w : Fin m → Ω → ℝ} {z : ℝ} (h : CenteredOutcomePair ρ v w z) (τ γ : ℝ) (c : Cell m) : (∫ ω, outcomeLikelihood τ γ c (fun i => v i ω) * outcomeLikelihood τ γ c (fun i => w i ω) ∂ρ) = ∑ S ∈ (selected c).powerset, γ ^ (2 * S.card) * posterior τ c S ^ 2 * z ^ S.card := by -- Integrate the finite double expansion using its termwise receipts, then -- integral_subset_pair eliminates every off-diagonal term. classical let a : Finset (Fin m) → ℝ := fun S => γ ^ S.card * posterior τ c S have ht (S R : Finset (Fin m)) : Integrable (fun ω => (a S * ∏ i ∈ S, v i ω) * (a R * ∏ i ∈ R, w i ω)) ρ := by convert (integrable_subset_pair h S R).const_mul (a S * a R) using 1 funext ω ring have hint (S R : Finset (Fin m)) : (∫ ω, (a S * ∏ i ∈ S, v i ω) * (a R * ∏ i ∈ R, w i ω) ∂ρ) = (a S * a R) * (if S = R then z ^ S.card else 0) := by have heq : (fun ω => (a S * ∏ i ∈ S, v i ω) * (a R * ∏ i ∈ R, w i ω)) = (fun ω => (a S * a R) * ((∏ i ∈ S, v i ω) * ∏ i ∈ R, w i ω)) := by funext ω ring rw [heq, integral_const_mul, integral_subset_pair h S R] simp_rw [outcomeLikelihood_expansion, Finset.sum_mul, Finset.mul_sum] change (∫ ω, ∑ S ∈ (selected c).powerset, ∑ R ∈ (selected c).powerset, (a S * ∏ i ∈ S, v i ω) * (a R * ∏ i ∈ R, w i ω) ∂ρ) = _ rw [integral_finsetSum _ (fun S _ => integrable_finsetSum _ (fun R _ => ht S R))] apply Finset.sum_congr rfl intro S hS rw [integral_finsetSum _ (fun R _ => ht S R)] simp_rw [hint] rw [Finset.sum_eq_single S] · dsimp [a] simp only [if_true, pow_mul, pow_two] ring · intro R _ hRS rw [if_neg (Ne.symm hRS), mul_zero] · intro hnot exact (hnot hS).elim

theorem subsetEnergy_eq_zero_of_lt {m d : ℕ} (τ : ℝ) (c : Cell m) (hd : m < d) : subsetEnergy τ c d = 0 := by have hc : (selected c).card ≤ m := by simpa using Finset.card_le_card (Finset.subset_univ (selected c)) simp [subsetEnergy, Finset.powersetCard_eq_empty.mpr (lt_of_le_of_lt hc hd)]

theorem integrable_cellOverlap (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] {τ : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (γ z : ℝ) (m : ℕ) : Integrable (fun c => cellOverlap τ γ z c) (ν m) := by unfold cellOverlap apply (integrable_const 1).add apply integrable_finsetSum intro d _ exact ((integrable_subsetEnergy ν hτ hν m (d + 1)).const_mul (γ ^ (2 * (d + 1)))).mul_const (z ^ (d + 1))

theorem integrable_conditional_cellOverlap (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] (ξ : NNReal) {τ : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (γ z : ℝ) : Integrable (fun m : ℕ => ∫ c, cellOverlap τ γ z c ∂ν m) (poissonMeasure ξ) := by have hb : Integrable (fun m : ℕ => (1 + 4 * γ ^ 2 * |z|) ^ m) (poissonMeasure ξ) := by simpa using integrable_poisson_tilted_factorial ξ (by positivity : 0 ≤ 1 + 4 * γ ^ 2 * |z|) 0 refine hb.mono' (measurable_of_countable _).aestronglyMeasurable ?_ apply Filter.Eventually.of_forall intro m calc _ ≤ ∫ c, ‖cellOverlap τ γ z c‖ ∂ν m := norm_integral_le_integral_norm _ _ ≤ ∫ _c : Cell m, (1 + 4 * γ ^ 2 * |z|) ^ m ∂ν m := by apply integral_mono_ae (integrable_cellOverlap ν hτ hν γ z m).norm (integrable_const _) filter_upwards [hν m] with c hc exact norm_cellOverlap_le hτ γ z c hc _ = _ := by simp

theorem integral_cellOverlap_eq_series (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] (ξ : NNReal) {τ : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (γ z : ℝ) : (∫ m : ℕ, ∫ c, cellOverlap τ γ z c ∂ν m ∂poissonMeasure ξ) = overlapSeries (coefficient ν ξ τ γ) z := by let F : ℕ → ℕ → ℝ := fun d m => γ ^ (2 * (d + 1)) * conditionalEnergy ν τ m (d + 1) * z ^ (d + 1) have hi (d : ℕ) : Integrable (F d) (poissonMeasure ξ) := ((integrable_conditionalEnergy ν ξ hτ hν (d + 1)).const_mul (γ ^ (2 * (d + 1)))).mul_const (z ^ (d + 1)) have hs : Summable (fun d => ∫ m, ‖F d m‖ ∂poissonMeasure ξ) := by apply (coefficient_summable_abs ν ξ hτ hν γ z).congr intro d have hg : 0 ≤ γ ^ (2 * (d + 1)) := by rw [pow_mul]; positivity have hn (m : ℕ) : 0 ≤ conditionalEnergy ν τ m (d + 1) := integral_nonneg (fun c => subsetEnergy_nonneg τ c _) simp only [F, Real.norm_eq_abs, abs_mul, abs_of_nonneg hg, abs_of_nonneg (hn _), abs_pow] rw [integral_mul_const, integral_const_mul] rw [abs_of_nonneg (coefficient_nonneg ν ξ τ γ _)] rfl have ht : Integrable (fun m => ∑' d, F d m) (poissonMeasure ξ) := by apply (integrable_conditional_cellOverlap ν ξ hτ hν γ z).sub (integrable_const 1) |>.congr apply Filter.Eventually.of_forall intro m change (∫ c, cellOverlap τ γ z c ∂ν m) - 1 = ∑' d, F d m rw [integral_cellOverlap_eq_tsum ν hτ hν γ z m] dsimp [F] ring simp_rw [integral_cellOverlap_eq_tsum ν hτ hν γ z] rw [integral_add (integrable_const 1) ht] rw [← integral_tsum_of_summable_integral_norm hi hs] simp only [integral_const, probReal_univ, smul_eq_mul, one_mul] unfold overlapSeries congr 1 apply tsum_congr intro d dsimp [F] rw [integral_mul_const, integral_const_mul] rfl

theorem conditionalCrossMoment_eq_cellOverlap {Ω : Type*} [MeasurableSpace Ω] (ρ : ∀ m, Cell m → Measure Ω) [∀ m c, IsProbabilityMeasure (ρ m c)] (v w : ∀ m, Cell m → Fin m → Ω → ℝ) {τ z : ℝ} (hτ : |τ| ≤ 1 / 4) {m : ℕ} {c : Cell m} (hu : ∀ i, |c.1 i| ≤ 1) (hout : CenteredOutcomePair (ρ m c) (v m c) (w m c) z) (γ : ℝ) : conditionalCrossMoment ρ v w τ γ m c = cellOverlap τ γ z c := by exact integral_outcomeLikelihood_pair_by_card hout hτ hu γ

theorem integrable_conditionalCrossMoment {Ω : Type*} [MeasurableSpace Ω] (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] (ρ : ∀ m, Cell m → Measure Ω) [∀ m c, IsProbabilityMeasure (ρ m c)] (v w : ∀ m, Cell m → Fin m → Ω → ℝ) {τ z : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (hout : ∀ m, ∀ᵐ c ∂ν m, CenteredOutcomePair (ρ m c) (v m c) (w m c) z) (γ : ℝ) (m : ℕ) : Integrable (conditionalCrossMoment ρ v w τ γ m) (ν m) := by -- Equality almost everywhere with the measurable finite cellOverlap avoids -- requiring a measurable outcome kernel as an additional input. apply (integrable_cellOverlap ν hτ hν γ z m).congr filter_upwards [hν m, hout m] with c hc ho exact (conditionalCrossMoment_eq_cellOverlap ρ v w hτ hc.1 ho γ).symm

theorem integrable_poisson_crossMoment {Ω : Type*} [MeasurableSpace Ω] (ν : ∀ m, Measure (Cell m)) [∀ m, IsProbabilityMeasure (ν m)] (ρ : ∀ m, Cell m → Measure Ω) [∀ m c, IsProbabilityMeasure (ρ m c)] (v w : ∀ m, Cell m → Fin m → Ω → ℝ) (ξ : NNReal) {τ z : ℝ} (hτ : |τ| ≤ 1 / 4) (hν : ∀ m, ∀ᵐ c ∂ν m, Valid c) (hout : ∀ m, ∀ᵐ c ∂ν m, CenteredOutcomePair (ρ m c) (v m c) (w m c) z) (γ : ℝ) : Integrable (fun m : ℕ => ∫ c, conditionalCrossMoment ρ v w τ γ m c ∂ν m) (poissonMeasure ξ) := by apply (integrable_conditional_cellOverlap ν ξ hτ hν γ z).congr apply Filter.Eventually.of_forall intro m apply integral_congr_ae filter_upwards [hν m, hout m] with c hc ho exact (conditionalCrossMoment_eq_cellOverlap ρ v w hτ hc.1 ho γ).symm

theorem integrable_poisson_choose (ξ : NNReal) (d : ℕ) : Integrable (fun m : ℕ => (m.choose d : ℝ)) (poissonMeasure ξ) := by have h := (poisson_descFactorial_integrable ξ d).div_const (d.factorial : ℝ) convert h using 1 funext m rw [Nat.descFactorial_eq_factorial_mul_choose, Nat.cast_mul] simp [Nat.factorial_ne_zero]

theorem integral_poisson_choose (ξ : NNReal) (d : ℕ) : (∫ m : ℕ, (m.choose d : ℝ) ∂poissonMeasure ξ) = (ξ : ℝ) ^ d / (d.factorial : ℝ) := by calc (∫ m : ℕ, (m.choose d : ℝ) ∂poissonMeasure ξ) = ∫ m : ℕ, (m.descFactorial d : ℝ) / (d.factorial : ℝ) ∂poissonMeasure ξ := by congr 1 funext m rw [Nat.descFactorial_eq_factorial_mul_choose, Nat.cast_mul] simp [Nat.factorial_ne_zero] _ = _ := by rw [integral_div, poisson_descFactorial_moment]

theorem integrable_poisson_tilted_factorial (ξ : NNReal) {a : ℝ} (ha : 0 ≤ a) (d : ℕ) : Integrable (fun m : ℕ => (m.descFactorial d : ℝ) * a ^ m) (poissonMeasure ξ) := by let b : NNReal := ⟨a, ha⟩ have hs := integrable_poissonMeasure_iff.mp (poisson_descFactorial_integrable (ξ * b) d) rw [integrable_poissonMeasure_iff] apply (hs.mul_left (exp ((ξ : ℝ) * (a - 1)))).congr intro m simp only [Real.norm_eq_abs] rw [abs_of_nonneg (by positivity : 0 ≤ (m.descFactorial d : ℝ) * a ^ m), abs_of_nonneg (Nat.cast_nonneg _)] have hw := poisson_weight_tilt ξ b m change _ * a ^ m = exp ((ξ : ℝ) * (a - 1)) * (exp (-((ξ * b : NNReal) : ℝ)) * ((ξ * b : NNReal) : ℝ) ^ m / (m.factorial : ℝ)) at hw calc _ = (exp ((ξ : ℝ) * (a - 1)) * (exp (-((ξ * b : NNReal) : ℝ)) * ((ξ * b : NNReal) : ℝ) ^ m / (m.factorial : ℝ))) * (m.descFactorial d : ℝ) := by ring _ = _ := by rw [← hw]; ring

theorem integral_poisson_tilted_factorial (ξ : NNReal) {a : ℝ} (ha : 0 ≤ a) (d : ℕ) : (∫ m : ℕ, (m.descFactorial d : ℝ) * a ^ m ∂poissonMeasure ξ) = ((ξ : ℝ) * a) ^ d * exp ((ξ : ℝ) * (a - 1)) := by let b : NNReal := ⟨a, ha⟩ rw [integral_poissonMeasure] simp only [smul_eq_mul] calc _ = exp ((ξ : ℝ) * (a - 1)) * ∑' m : ℕ, exp (-((ξ * b : NNReal) : ℝ)) * ((ξ * b : NNReal) : ℝ) ^ m / (m.factorial : ℝ) * (m.descFactorial d : ℝ) := by rw [← tsum_mul_left] apply tsum_congr intro m have hw := poisson_weight_tilt ξ b m change _ * a ^ m = exp ((ξ : ℝ) * (a - 1)) * (exp (-((ξ * b : NNReal) : ℝ)) * ((ξ * b : NNReal) : ℝ) ^ m / (m.factorial : ℝ)) at hw calc _ = (exp (-(ξ : ℝ)) * (ξ : ℝ) ^ m / (m.factorial : ℝ) * a ^ m) * (m.descFactorial d : ℝ) := by ring _ = _ := by rw [hw]; ring _ = _ := by have hm := poisson_descFactorial_moment (ξ * b) d rw [integral_poissonMeasure] at hm simp only [smul_eq_mul] at hm rw [hm] simp only [NNReal.coe_mul] change exp ((ξ : ℝ) * (a - 1)) * ((ξ : ℝ) * a) ^ d = _ ring

theorem integrable_poisson_collision_tilt (ξ : NNReal) {a : ℝ} (ha : 0 ≤ a) : Integrable (fun m : ℕ => (m : ℝ) * ((m - 1 : ℕ) : ℝ) ^ 2 * a ^ m) (poissonMeasure ξ) := by simp_rw [collision_factorial_identity, add_mul] exact (integrable_poisson_tilted_factorial ξ ha 3).add (integrable_poisson_tilted_factorial ξ ha 2)

theorem integral_poisson_collision_tilt (ξ : NNReal) {a : ℝ} (ha : 0 ≤ a) : (∫ m : ℕ, (m : ℝ) * ((m - 1 : ℕ) : ℝ) ^ 2 * a ^ m ∂poissonMeasure ξ) = (((ξ : ℝ) * a) ^ 3 + ((ξ : ℝ) * a) ^ 2) * exp ((ξ : ℝ) * (a - 1)) := by simp_rw [collision_factorial_identity, add_mul] rw [integral_add (integrable_poisson_tilted_factorial ξ ha 3) (integrable_poisson_tilted_factorial ξ ha 2), integral_poisson_tilted_factorial ξ ha 3, integral_poisson_tilted_factorial ξ ha 2]