Mathlib.Probability.Poisson.Pair­Second­Moment

theorem pairSum_sq_le_count_mul_sum_sq (K : X → Y → ℝ) (s : FiniteSample X) (t : FiniteSample Y) : pairSum K s t ^ 2 ≤ (s.1 : ℝ) * (t.1 : ℝ) * (∑ i : Fin s.1, ∑ j : Fin t.1, K (s.2 i) (t.2 j) ^ 2) := by -- Apply `sq_sum_le_card_mul_sum_sq` to the product of the two index -- finsets. Rewrite the product sum with `Finset.sum_product'`, and its -- cardinality with `Finset.card_product` and `Fintype.card_fin`. have h := sq_sum_le_card_mul_sum_sq (s := univ) (f := fun p : Fin s.1 × Fin t.1 => K (s.2 p.1) (t.2 p.2)) rw [← Finset.univ_product_univ, Finset.sum_product] at h rw [Finset.sum_product] at h simpa [pairSum, Finset.card_product, Fintype.card_fin, mul_assoc] using h

theorem integral_bilinearSum_sq_eq_coincidence {Ω ι κ : Type*} [MeasurableSpace Ω] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (μ : Measure Ω) (K : ι → κ → Ω → ℝ) (hK : ∀ i j k l, Integrable (fun ω => K i j ω * K k l ω) μ) : ∫ ω, (∑ i, ∑ j, K i j ω) ^ 2 ∂μ = (∑ i, ∑ j, ∫ ω, K i j ω * K i j ω ∂μ) + (∑ i, ∑ j, ∑ l ∈ (Finset.univ.erase j), ∫ ω, K i j ω * K i l ω ∂μ) + (∑ i, ∑ j, ∑ k ∈ (Finset.univ.erase i), ∫ ω, K i j ω * K k j ω ∂μ) + (∑ i, ∑ j, ∑ k ∈ (Finset.univ.erase i), ∑ l ∈ (Finset.univ.erase j), ∫ ω, K i j ω * K k l ω ∂μ) := by rw [integral_congr_ae (Filter.Eventually.of_forall fun ω => bilinearSum_sq_eq_coincidence (fun i j => K i j ω))] let A := fun ω => ∑ i, ∑ j, K i j ω * K i j ω let B := fun ω => ∑ i, ∑ j, ∑ l ∈ (Finset.univ.erase j), K i j ω * K i l ω let C := fun ω => ∑ i, ∑ j, ∑ k ∈ (Finset.univ.erase i), K i j ω * K k j ω let D := fun ω => ∑ i, ∑ j, ∑ k ∈ (Finset.univ.erase i), ∑ l ∈ (Finset.univ.erase j), K i j ω * K k l ω have hA : Integrable A μ := by dsimp only [A] apply integrable_finsetSum intro i _ apply integrable_finsetSum intro j _ exact hK i j i j have hB : Integrable B μ := by dsimp only [B] apply integrable_finsetSum intro i _ apply integrable_finsetSum intro j _ apply integrable_finsetSum intro l _ exact hK i j i l have hC : Integrable C μ := by dsimp only [C] apply integrable_finsetSum intro i _ apply integrable_finsetSum intro j _ apply integrable_finsetSum intro k _ exact hK i j k j have hD : Integrable D μ := by dsimp only [D] apply integrable_finsetSum intro i _ apply integrable_finsetSum intro j _ apply integrable_finsetSum intro k _ apply integrable_finsetSum intro l _ exact hK i j k l change ∫ ω, ((A ω + B ω) + C ω) + D ω ∂μ = _ have hAB := integral_add hA hB have hABC := integral_add (hA.add hB) hC have hABCD := integral_add ((hA.add hB).add hC) hD have hAB' : (∫ ω, (A + B) ω ∂μ) = (∫ ω, A ω ∂μ) + (∫ ω, B ω ∂μ) := by simpa only [Pi.add_apply] using hAB have hABC' : (∫ ω, (A + B + C) ω ∂μ) = (∫ ω, (A + B) ω ∂μ) + (∫ ω, C ω ∂μ) := by simpa only [Pi.add_apply] using hABC have eA : (∫ ω, A ω ∂μ) = ∑ i, ∑ j, ∫ ω, K i j ω * K i j ω ∂μ := by dsimp only [A] rw [integral_finsetSum univ (fun i _ => integrable_finsetSum univ (fun j _ => hK i j i j))] apply Finset.sum_congr rfl intro i _ rw [integral_finsetSum univ (fun j _ => hK i j i j)] have eB : (∫ ω, B ω ∂μ) = ∑ i, ∑ j, ∑ l ∈ (Finset.univ.erase j), ∫ ω, K i j ω * K i l ω ∂μ := by dsimp only [B] rw [integral_finsetSum univ (fun i _ => integrable_finsetSum univ (fun j _ => integrable_finsetSum (Finset.univ.erase j) (fun l _ => hK i j i l)))] apply Finset.sum_congr rfl intro i _ rw [integral_finsetSum univ (fun j _ => integrable_finsetSum (Finset.univ.erase j) (fun l _ => hK i j i l))] apply Finset.sum_congr rfl intro j _ rw [integral_finsetSum (Finset.univ.erase j) (fun l _ => hK i j i l)] have eC : (∫ ω, C ω ∂μ) = ∑ i, ∑ j, ∑ k ∈ (Finset.univ.erase i), ∫ ω, K i j ω * K k j ω ∂μ := by dsimp only [C] rw [integral_finsetSum univ (fun i _ => integrable_finsetSum univ (fun j _ => integrable_finsetSum (Finset.univ.erase i) (fun k _ => hK i j k j)))] apply Finset.sum_congr rfl intro i _ rw [integral_finsetSum univ (fun j _ => integrable_finsetSum (Finset.univ.erase i) (fun k _ => hK i j k j))] apply Finset.sum_congr rfl intro j _ rw [integral_finsetSum (Finset.univ.erase i) (fun k _ => hK i j k j)] have eD : (∫ ω, D ω ∂μ) = ∑ i, ∑ j, ∑ k ∈ (Finset.univ.erase i), ∑ l ∈ (Finset.univ.erase j), ∫ ω, K i j ω * K k l ω ∂μ := by dsimp only [D] rw [integral_finsetSum univ (fun i _ => integrable_finsetSum univ (fun j _ => integrable_finsetSum (Finset.univ.erase i) (fun k _ => integrable_finsetSum (Finset.univ.erase j) (fun l _ => hK i j k l))))] apply Finset.sum_congr rfl intro i _ rw [integral_finsetSum univ (fun j _ => integrable_finsetSum (Finset.univ.erase i) (fun k _ => integrable_finsetSum (Finset.univ.erase j) (fun l _ => hK i j k l)))] apply Finset.sum_congr rfl intro j _ rw [integral_finsetSum (Finset.univ.erase i) (fun k _ => integrable_finsetSum (Finset.univ.erase j) (fun l _ => hK i j k l))] apply Finset.sum_congr rfl intro k _ rw [integral_finsetSum (Finset.univ.erase j) (fun l _ => hK i j k l)] calc _ = (∫ ω, (A + B + C) ω ∂μ) + (∫ ω, D ω ∂μ) := by simpa only [Pi.add_apply] using hABCD _ = ((∫ ω, (A + B) ω ∂μ) + (∫ ω, C ω ∂μ)) + (∫ ω, D ω ∂μ) := by rw [hABC'] _ = (((∫ ω, A ω ∂μ) + (∫ ω, B ω ∂μ)) + (∫ ω, C ω ∂μ)) + (∫ ω, D ω ∂μ) := by rw [hAB'] _ = _ := by rw [eA, eB, eC, eD]

theorem integral_fixedCount_both_distinct (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (K : X → Y → ℝ) (m n : ℕ) (hK : Measurable (uncurry K)) (hK2 : Integrable (fun p : X × Y => K p.1 p.2 ^ 2) (P.prod Q)) (i k : Fin m) (j l : Fin n) (hik : i ≠ k) (hjl : j ≠ l) : (∫ p : (Fin m → X) × (Fin n → Y), K (p.1 i) (p.2 j) * K (p.1 k) (p.2 l) ∂((Measure.pi fun _ : Fin m => P).prod (Measure.pi fun _ : Fin n => Q))) = ∫ x, ∫ x', ∫ y, ∫ y', K x y * K x' y' ∂Q ∂Q ∂P ∂P := by let μ := (Measure.pi fun _ : Fin m => P).prod (Measure.pi fun _ : Fin n => Q) let φ : ((Fin m → X) × (Fin n → Y)) → (X × X) × (Y × Y) := fun p => ((p.1 i, p.1 k), (p.2 j, p.2 l)) let F : (X × X) × (Y × Y) → ℝ := fun z => K z.1.1 z.2.1 * K z.1.2 z.2.2 have hφ : MeasurePreserving φ μ ((P.prod P).prod (Q.prod Q)) := by convert (measurePreserving_fixedCount_two P m i k hik).prod (measurePreserving_fixedCount_two Q n j l hjl) using 1 rfl have hFmeas : Measurable F := by have h₁ : Measurable (fun z : (X × X) × (Y × Y) => (z.1.1, z.2.1)) := by fun_prop have h₂ : Measurable (fun z : (X × X) × (Y × Y) => (z.1.2, z.2.2)) := by fun_prop exact (hK.comp h₁).mul (hK.comp h₂) have hI := integrable_fixedCount_kernelProduct P Q K m n hK hK2 i k j l have hF : Integrable F ((P.prod P).prod (Q.prod Q)) := by apply (hφ.integrable_comp hFmeas.aestronglyMeasurable).mp exact hI have houter : (∫ p, F (φ p) ∂μ) = ∫ z, F z ∂((P.prod P).prod (Q.prod Q)) := by have e := integral_map (μ := μ) (φ := φ) hφ.measurable.aemeasurable (f := F) hFmeas.aestronglyMeasurable rw [hφ.map_eq] at e exact e.symm have hinner : ∀ᵐ p : X × X ∂(P.prod P), (∫ q : Y × Y, F (p, q) ∂(Q.prod Q)) = ∫ y, ∫ y', K p.1 y * K p.2 y' ∂Q ∂Q := by filter_upwards [hF.prod_right_ae] with p hp exact integral_prod _ hp have hG : Integrable (fun p : X × X => ∫ y, ∫ y', K p.1 y * K p.2 y' ∂Q ∂Q) (P.prod P) := hF.integral_prod_left.congr hinner change (∫ p, F (φ p) ∂μ) = _ calc (∫ p, F (φ p) ∂μ) = ∫ p : X × X, ∫ q : Y × Y, F (p, q) ∂(Q.prod Q) ∂(P.prod P) := by rw [houter, integral_prod _ hF] _ = ∫ p : X × X, ∫ y, ∫ y', K p.1 y * K p.2 y' ∂Q ∂Q ∂(P.prod P) := integral_congr_ae hinner _ = _ := integral_prod _ hG

theorem poisson_pair_count_sq_series_lt_top (rateA rateB : ℝ≥0) : (∑' m : ℕ, ∑' n : ℕ, (poissonMeasure rateA) ({m} : Set ℕ) * (poissonMeasure rateB) ({n} : Set ℕ) * ((m : ℝ≥0∞) ^ 2 * (n : ℝ≥0∞) ^ 2)) < ⊤ := by have scalar (rate : ℝ≥0) : (∑' n : ℕ, (poissonMeasure rate) ({n} : Set ℕ) * (n : ℝ≥0∞) ^ 2) < ⊤ := by have h := (integrable_poisson_count_sq rate).lintegral_lt_top rw [lintegral_countable'] at h simp_rw [ENNReal.ofReal_pow (Nat.cast_nonneg _) 2, ENNReal.ofReal_natCast] at h simpa only [mul_comm] using h calc (∑' m : ℕ, ∑' n : ℕ, (poissonMeasure rateA) ({m} : Set ℕ) * (poissonMeasure rateB) ({n} : Set ℕ) * ((m : ℝ≥0∞) ^ 2 * (n : ℝ≥0∞) ^ 2)) = ∑' m : ℕ, ∑' n : ℕ, ((poissonMeasure rateA) ({m} : Set ℕ) * (m : ℝ≥0∞) ^ 2) * ((poissonMeasure rateB) ({n} : Set ℕ) * (n : ℝ≥0∞) ^ 2) := by congr 1 funext m congr 1 funext n ac_rfl _ = ∑' m : ℕ, ((poissonMeasure rateA) ({m} : Set ℕ) * (m : ℝ≥0∞) ^ 2) * (∑' n : ℕ, (poissonMeasure rateB) ({n} : Set ℕ) * (n : ℝ≥0∞) ^ 2) := by simp_rw [ENNReal.tsum_mul_left] _ = (∑' m : ℕ, (poissonMeasure rateA) ({m} : Set ℕ) * (m : ℝ≥0∞) ^ 2) * (∑' n : ℕ, (poissonMeasure rateB) ({n} : Set ℕ) * (n : ℝ≥0∞) ^ 2) := by rw [ENNReal.tsum_mul_right] _ < ⊤ := ENNReal.mul_lt_top (scalar rateA) (scalar rateB)

theorem integral_fixedCount_pairSum_sq (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (K : X → Y → ℝ) (m n : ℕ) (hK : Measurable (uncurry K)) (hK2 : Integrable (fun p : X × Y => K p.1 p.2 ^ 2) (P.prod Q)) : (∫ p : (Fin m → X) × (Fin n → Y), (∑ i : Fin m, ∑ j : Fin n, K (p.1 i) (p.2 j)) ^ 2 ∂((Measure.pi fun _ : Fin m => P).prod (Measure.pi fun _ : Fin n => Q))) = (m : ℝ) * (n : ℝ) * (∫ x, ∫ y, K x y * K x y ∂Q ∂P) + (m : ℝ) * ((n : ℝ) * ((n : ℝ) - 1)) * (∫ x, ∫ y, ∫ y', K x y * K x y' ∂Q ∂Q ∂P) + ((m : ℝ) * ((m : ℝ) - 1)) * (n : ℝ) * (∫ x, ∫ x', ∫ y, K x y * K x' y ∂Q ∂P ∂P) + ((m : ℝ) * ((m : ℝ) - 1)) * ((n : ℝ) * ((n : ℝ) - 1)) * (∫ x, ∫ x', ∫ y, ∫ y', K x y * K x' y' ∂Q ∂Q ∂P ∂P) := by classical let μ := (Measure.pi fun _ : Fin m => P).prod (Measure.pi fun _ : Fin n => Q) have hprod (i k : Fin m) (j l : Fin n) := integrable_fixedCount_kernelProduct P Q K m n hK hK2 i k j l change (∫ p, (∑ i, ∑ j, K (p.1 i) (p.2 j)) ^ 2 ∂μ) = _ rw [integral_bilinearSum_sq_eq_coincidence μ (fun i j p => K (p.1 i) (p.2 j)) (fun i j k l => hprod i k j l)] dsimp only [μ] simp_rw [integral_fixedCount_both_equal P Q K m n hK hK2] have hB : (∑ i : Fin m, ∑ j : Fin n, ∑ l ∈ Finset.univ.erase j, ∫ p, K (p.1 i) (p.2 j) * K (p.1 i) (p.2 l) ∂μ) = ∑ i : Fin m, ∑ j : Fin n, ∑ l ∈ Finset.univ.erase j, ∫ x, ∫ y, ∫ y', K x y * K x y' ∂Q ∂Q ∂P := by apply Finset.sum_congr rfl; intro i _ apply Finset.sum_congr rfl; intro j _ apply Finset.sum_congr rfl; intro l hl exact integral_fixedCount_shared_left P Q K m n hK hK2 i j l ((Finset.mem_erase.mp hl).1.symm) have hC : (∑ i : Fin m, ∑ j : Fin n, ∑ k ∈ Finset.univ.erase i, ∫ p, K (p.1 i) (p.2 j) * K (p.1 k) (p.2 j) ∂μ) = ∑ i : Fin m, ∑ j : Fin n, ∑ k ∈ Finset.univ.erase i, ∫ x, ∫ x', ∫ y, K x y * K x' y ∂Q ∂P ∂P := by apply Finset.sum_congr rfl; intro i _ apply Finset.sum_congr rfl; intro j _ apply Finset.sum_congr rfl; intro k hk exact integral_fixedCount_shared_right P Q K m n hK hK2 i k j ((Finset.mem_erase.mp hk).1.symm) have hD : (∑ i : Fin m, ∑ j : Fin n, ∑ k ∈ Finset.univ.erase i, ∑ l ∈ Finset.univ.erase j, ∫ p, K (p.1 i) (p.2 j) * K (p.1 k) (p.2 l) ∂μ) = ∑ i : Fin m, ∑ j : Fin n, ∑ k ∈ Finset.univ.erase i, ∑ l ∈ Finset.univ.erase j, ∫ x, ∫ x', ∫ y, ∫ y', K x y * K x' y' ∂Q ∂Q ∂P ∂P := by apply Finset.sum_congr rfl; intro i _ apply Finset.sum_congr rfl; intro j _ apply Finset.sum_congr rfl; intro k hk apply Finset.sum_congr rfl; intro l hl exact integral_fixedCount_both_distinct P Q K m n hK hK2 i k j l ((Finset.mem_erase.mp hk).1.symm) ((Finset.mem_erase.mp hl).1.symm) rw [hB, hC, hD] simp only [Finset.sum_const, nsmul_eq_mul, Finset.card_univ, Fintype.card_fin] simp only [Finset.cast_card_erase_of_mem (Finset.mem_univ _)] simp only [Finset.sum_const, nsmul_eq_mul, Finset.card_univ, Fintype.card_fin] ring

theorem lintegral_pairSum_sq_lt_top (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (rateA rateB : ℝ≥0) (K : X → Y → ℝ) (hK : Measurable (uncurry K)) (hK2 : Integrable (fun p : X × Y => K p.1 p.2 ^ 2) (P.prod Q)) : (∫⁻ p : FiniteSample X × FiniteSample Y, ofReal (pairSum K p.1 p.2 ^ 2) ∂((finitePoissonSampleLaw P rateA).prod (finitePoissonSampleLaw Q rateB))) < ⊤ := by -- Expand by `lintegral_pair_count_mixture`. Apply -- `lintegral_fixedCount_pairSum_sq_le` termwise, factor the constant -- one-pair lintegral out of the double series, and apply -- `poisson_pair_count_sq_series_lt_top`. Measurability of the ENNReal -- integrand follows from `measurable_pairSum K hK`, `Measurable.pow_const`, -- and `ENNReal.measurable_ofReal`. The one-pair lintegral is finite by -- `hK2.lintegral_lt_top`; handle a zero value before cancelling or -- reassociating an infinite ENNReal factor. let C : ℝ≥0∞ := ∫⁻ p : X × Y, ofReal (K p.1 p.2 ^ 2) ∂(P.prod Q) have hC : C < ⊤ := by have h := hK2.lintegral_lt_top exact h have hmeas : Measurable (fun p : FiniteSample X × FiniteSample Y => ofReal (pairSum K p.1 p.2 ^ 2)) := ENNReal.measurable_ofReal.comp ((measurable_pairSum K hK).pow_const 2) rw [lintegral_pair_count_mixture P Q rateA rateB _ hmeas] have hbound (m n : ℕ) : (poissonMeasure rateA) ({m} : Set ℕ) * (poissonMeasure rateB) ({n} : Set ℕ) * (∫⁻ p : (Fin m → X) × (Fin n → Y), ofReal (pairSum K ⟨m, p.1⟩ ⟨n, p.2⟩ ^ 2) ∂((Measure.pi fun _ : Fin m => P).prod (Measure.pi fun _ : Fin n => Q))) ≤ ((poissonMeasure rateA) ({m} : Set ℕ) * (poissonMeasure rateB) ({n} : Set ℕ) * ((m : ℝ≥0∞) ^ 2 * (n : ℝ≥0∞) ^ 2)) * C := by have h := lintegral_fixedCount_pairSum_sq_le P Q K m n hK hK2 dsimp only [pairSum] calc _ ≤ (poissonMeasure rateA) ({m} : Set ℕ) * (poissonMeasure rateB) ({n} : Set ℕ) * ((m : ℝ≥0∞) ^ 2 * (n : ℝ≥0∞) ^ 2 * C) := by gcongr _ = _ := by ac_rfl have hsum := poisson_pair_count_sq_series_lt_top rateA rateB have hle : (∑' m : ℕ, ∑' n : ℕ, (poissonMeasure rateA) ({m} : Set ℕ) * (poissonMeasure rateB) ({n} : Set ℕ) * (∫⁻ p : (Fin m → X) × (Fin n → Y), ofReal (pairSum K ⟨m, p.1⟩ ⟨n, p.2⟩ ^ 2) ∂((Measure.pi fun _ : Fin m => P).prod (Measure.pi fun _ : Fin n => Q)))) ≤ (∑' m : ℕ, ∑' n : ℕ, (poissonMeasure rateA) ({m} : Set ℕ) * (poissonMeasure rateB) ({n} : Set ℕ) * ((m : ℝ≥0∞) ^ 2 * (n : ℝ≥0∞) ^ 2)) * C := by calc _ ≤ ∑' m : ℕ, ∑' n : ℕ, ((poissonMeasure rateA) ({m} : Set ℕ) * (poissonMeasure rateB) ({n} : Set ℕ) * ((m : ℝ≥0∞) ^ 2 * (n : ℝ≥0∞) ^ 2)) * C := by exact ENNReal.tsum_le_tsum fun m => ENNReal.tsum_le_tsum fun n => hbound m n _ = _ := by simp_rw [ENNReal.tsum_mul_right] exact lt_of_le_of_lt hle (ENNReal.mul_lt_top hsum hC)

theorem integral_pairSum_sq (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (rateA rateB : ℝ≥0) (K : X → Y → ℝ) (hK : Measurable (uncurry K)) (hK2 : Integrable (fun p : X × Y => K p.1 p.2 ^ 2) (P.prod Q)) : (∫ p : FiniteSample X × FiniteSample Y, pairSum K p.1 p.2 ^ 2 ∂((finitePoissonSampleLaw P rateA).prod (finitePoissonSampleLaw Q rateB))) = (rateA : ℝ) * (rateB : ℝ) * (∫ x, ∫ y, K x y * K x y ∂Q ∂P) + (rateA : ℝ) * (rateB : ℝ) ^ 2 * (∫ x, ∫ y, ∫ y', K x y * K x y' ∂Q ∂Q ∂P) + (rateA : ℝ) ^ 2 * (rateB : ℝ) * (∫ x, ∫ x', ∫ y, K x y * K x' y ∂Q ∂P ∂P) + (rateA : ℝ) ^ 2 * (rateB : ℝ) ^ 2 * (∫ x, ∫ x', ∫ y, ∫ y', K x y * K x' y' ∂Q ∂Q ∂P ∂P) := by let f (m : ℕ) : ℝ := m let g (m : ℕ) : ℝ := (m : ℝ) * ((m : ℝ) - 1) let c₀ : ℝ := ∫ x, ∫ y, K x y * K x y ∂Q ∂P let c₁ : ℝ := ∫ x, ∫ y, ∫ y', K x y * K x y' ∂Q ∂Q ∂P let c₂ : ℝ := ∫ x, ∫ x', ∫ y, K x y * K x' y ∂Q ∂P ∂P let c₃ : ℝ := ∫ x, ∫ x', ∫ y, ∫ y', K x y * K x' y' ∂Q ∂Q ∂P ∂P let wA (m : ℕ) : ℝ := ((poissonMeasure rateA) ({m} : Set ℕ)).toReal let wB (n : ℕ) : ℝ := ((poissonMeasure rateB) ({n} : Set ℕ)).toReal let term (u v : ℕ → ℝ) (c : ℝ) (p : ℕ × ℕ) : ℝ := wA p.1 * wB p.2 * (u p.1 * v p.2 * c) have hfA : Integrable f (poissonMeasure rateA) := (poisson_natCast_memLp_two rateA).integrable (by norm_num) have hfB : Integrable f (poissonMeasure rateB) := (poisson_natCast_memLp_two rateB).integrable (by norm_num) have hgA : Integrable g (poissonMeasure rateA) := integrable_poisson_ordered_pairs rateA have hgB : Integrable g (poissonMeasure rateB) := integrable_poisson_ordered_pairs rateB have h₀ : Summable (term f f c₀) := summable_poisson_pair_product rateA rateB f f c₀ hfA hfB have h₁ : Summable (term f g c₁) := summable_poisson_pair_product rateA rateB f g c₁ hfA hgB have h₂ : Summable (term g f c₂) := summable_poisson_pair_product rateA rateB g f c₂ hgA hfB have h₃ : Summable (term g g c₃) := summable_poisson_pair_product rateA rateB g g c₃ hgA hgB rw [integral_pair_count_mixture P Q rateA rateB _ (integrable_pairSum_sq P Q rateA rateB K hK hK2)] have hfixed (m n : ℕ) : (∫ p : (Fin m → X) × (Fin n → Y), pairSum K ⟨m, p.1⟩ ⟨n, p.2⟩ ^ 2 ∂((Measure.pi fun _ : Fin m => P).prod (Measure.pi fun _ : Fin n => Q))) = f m * f n * c₀ + f m * g n * c₁ + g m * f n * c₂ + g m * g n * c₃ := by simpa only [pairSum, f, g, c₀, c₁, c₂, c₃] using integral_fixedCount_pairSum_sq P Q K m n hK hK2 simp_rw [hfixed] have hsum : Summable (fun p => term f f c₀ p + term f g c₁ p + term g f c₂ p + term g g c₃ p) := ((h₀.add h₁).add h₂).add h₃ calc (∑' m : ℕ, ∑' n : ℕ, wA m * wB n * (f m * f n * c₀ + f m * g n * c₁ + g m * f n * c₂ + g m * g n * c₃)) = ∑' p : ℕ × ℕ, (term f f c₀ p + term f g c₁ p + term g f c₂ p + term g g c₃ p) := by rw [hsum.tsum_prod] congr 1 funext m congr 1 funext n dsimp [term] ring _ = (∑' p : ℕ × ℕ, term f f c₀ p) + (∑' p : ℕ × ℕ, term f g c₁ p) + (∑' p : ℕ × ℕ, term g f c₂ p) + (∑' p : ℕ × ℕ, term g g c₃ p) := by rw [(h₀.add h₁).add h₂ |>.tsum_add h₃, (h₀.add h₁).tsum_add h₂, h₀.tsum_add h₁] _ = _ := by have hfactor (u v : ℕ → ℝ) (c : ℝ) (hu : Integrable u (poissonMeasure rateA)) (hv : Integrable v (poissonMeasure rateB)) (_hs : Summable (term u v c)) : (∑' p : ℕ × ℕ, term u v c p) = (∫ m : ℕ, u m ∂poissonMeasure rateA) * (∫ n : ℕ, v n ∂poissonMeasure rateB) * c := by have hsbase := summable_poisson_pair_product rateA rateB u v 1 hu hv have h := poisson_pair_weighted_tsum_mul rateA rateB u v hu hv calc _ = (∑' p : ℕ × ℕ, term u v 1 p) * c := by rw [← hsbase.tsum_mul_right c] congr 1 funext p dsimp [term] ring _ = (∑' m : ℕ, ∑' n : ℕ, wA m * wB n * (u m * v n)) * c := by rw [hsbase.tsum_prod] simp only [wA, wB, mul_one] _ = _ := by simpa only [wA, wB] using congrArg (· * c) h rw [hfactor f f c₀ hfA hfB h₀, hfactor f g c₁ hfA hgB h₁, hfactor g f c₂ hgA hfB h₂, hfactor g g c₃ hgA hgB h₃] simp only [f, g, c₀, c₁, c₂, c₃, poisson_count_first_moment, poisson_ordered_pairs_second_moment]

theorem integral_pair_count_mixture (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (rateA rateB : ℝ≥0) (f : FiniteSample X × FiniteSample Y → ℝ) (hf : Integrable f ((finitePoissonSampleLaw P rateA).prod (finitePoissonSampleLaw Q rateB))) : (∫ p, f p ∂((finitePoissonSampleLaw P rateA).prod (finitePoissonSampleLaw Q rateB))) = ∑' m : ℕ, ∑' n : ℕ, ((poissonMeasure rateA) ({m} : Set ℕ)).toReal * ((poissonMeasure rateB) ({n} : Set ℕ)).toReal * (∫ p : (Fin m → X) × (Fin n → Y), f (⟨m, p.1⟩, ⟨n, p.2⟩) ∂((Measure.pi fun _ : Fin m => P).prod (Measure.pi fun _ : Fin n => Q))) := by -- Expand both laws by their disjoint count fibres as in the preceding -- nonnegative theorem. Use `integral_sum_measure hf` twice; integrability -- descends to each fibre by `Integrable.mono_measure`. Then rewrite each -- fibre with `finitePoissonSampleLaw_restrict_count_eq`, map-product -- compatibility, and `integral_smul_measure`. let μA := finitePoissonSampleLaw P rateA let μB := finitePoissonSampleLaw Q rateB change Integrable f (μA.prod μB) at hf change ∫ p, f p ∂(μA.prod μB) = _ rw [finiteSample_count_sum μA, finiteSample_count_sum μB, Measure.prod_sum] at hf ⊢ rw [integral_sum_measure hf] rw [(hasSum_integral_measure hf).summable.tsum_prod] congr 1 funext m congr 1 funext n rw [finitePoissonSampleLaw_restrict_count_eq, finitePoissonSampleLaw_restrict_count_eq, Measure.prod_smul_left, Measure.prod_smul_right, Measure.map_prod_map _ _ (measurable_fixedSizeEmbed m) (measurable_fixedSizeEmbed n), integral_smul_measure, integral_smul_measure] by_cases hA : (poissonMeasure rateA) ({m} : Set ℕ) = 0 · simp [hA] by_cases hB : (poissonMeasure rateB) ({n} : Set ℕ) = 0 · simp [hB] have hFibre : Integrable f ((μA.restrict (FiniteSample.count ⁻¹' ({m} : Set ℕ))).prod (μB.restrict (FiniteSample.count ⁻¹' ({n} : Set ℕ)))) := by apply hf.mono_measure exact Measure.le_sum _ (m, n) rw [finitePoissonSampleLaw_restrict_count_eq, finitePoissonSampleLaw_restrict_count_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul, Measure.map_prod_map _ _ (measurable_fixedSizeEmbed m) (measurable_fixedSizeEmbed n)] at hFibre have hmap : AEStronglyMeasurable f (Measure.map (map (fixedSizeEmbed m) (fixedSizeEmbed n)) ((Measure.pi fun _ : Fin m => P).prod (Measure.pi fun _ : Fin n => Q))) := ((aemeasurable_smul_measure_iff (mul_ne_zero hA hB)).mp hFibre.aestronglyMeasurable.aemeasurable).aestronglyMeasurable rw [integral_map ((measurable_fixedSizeEmbed m).prodMap (measurable_fixedSizeEmbed n)).aemeasurable hmap] simp only [smul_eq_mul, map, fixedSizeEmbed, mul_assoc]

theorem poisson_ordered_pairs_second_moment (rate : ℝ≥0) : (∫ n : ℕ, (n : ℝ) * ((n : ℝ) - 1) ∂poissonMeasure rate) = (rate : ℝ) ^ 2 := by rw [show (fun n : ℕ => (n : ℝ) * ((n : ℝ) - 1)) = fun n => (n.descFactorial 2 : ℝ) by funext n simp only [Nat.cast_descFactorial_two]] rw [integral_poissonMeasure] simp only [smul_eq_mul] let f : ℕ → ℝ := fun n => exp (-(rate : ℝ)) * (rate : ℝ) ^ n / (n.factorial : ℝ) * (n.descFactorial 2 : ℝ) have hshift : Summable (fun k => f (k + 2)) := by apply Summable.congr ((NormedSpace.expSeries_div_hasSum_exp (rate : ℝ)).summable.mul_left ((rate : ℝ) ^ 2 * exp (-(rate : ℝ)))) intro k exact (poisson_descFactorial_two_shift rate k).symm have hprefix : ∑ k ∈ range 2, f k = 0 := by apply Finset.sum_eq_zero intro k hk have hklt : k < 2 := Finset.mem_range.mp hk have hzero : k.descFactorial 2 = 0 := Nat.descFactorial_eq_zero_iff_lt.mpr hklt simp only [f, hzero, Nat.cast_zero, mul_zero] calc ∑' n, exp (-(rate : ℝ)) * (rate : ℝ) ^ n / ↑n.factorial * ↑(n.descFactorial 2) = ∑' n, f n := by rfl _ = ∑ k ∈ range 2, f k + ∑' k, f (k + 2) := (hshift.sum_add_tsum_nat_add').symm _ = ∑' k, (((rate : ℝ) ^ 2 * exp (-(rate : ℝ))) * ((rate : ℝ) ^ k / (k.factorial : ℝ))) := by rw [hprefix, zero_add] congr 1 funext k exact poisson_descFactorial_two_shift rate k _ = ((rate : ℝ) ^ 2 * exp (-(rate : ℝ))) * exp (rate : ℝ) := by rw [tsum_mul_left] simpa only [Real.exp_eq_exp_ℝ] using congrArg (fun z : ℝ => ((rate : ℝ) ^ 2 * exp (-(rate : ℝ))) * z) (NormedSpace.expSeries_div_hasSum_exp (rate : ℝ)).tsum_eq _ = (rate : ℝ) ^ 2 := by rw [mul_assoc, ← Real.exp_add] ring_nf simp

theorem poisson_pair_weighted_tsum_mul (rateA rateB : ℝ≥0) (f g : ℕ → ℝ) (hf : Integrable f (poissonMeasure rateA)) (hg : Integrable g (poissonMeasure rateB)) : (∑' m : ℕ, ∑' n : ℕ, ((poissonMeasure rateA) ({m} : Set ℕ)).toReal * ((poissonMeasure rateB) ({n} : Set ℕ)).toReal * (f m * g n)) = (∫ m : ℕ, f m ∂poissonMeasure rateA) * (∫ n : ℕ, g n ∂poissonMeasure rateB) := by -- Apply `integral_countable` to each scalar law, using `hf` and `hg`. -- The weighted series is absolutely summable by the integrability of -- `(fun p : ℕ × ℕ => f p.1 * g p.2)` under the product measure; -- `Summable.tsum_prod` (or two `tsum_mul_*` rewrites) then separates it. let a (m : ℕ) : ℝ := ((poissonMeasure rateA) ({m} : Set ℕ)).toReal * f m let b (n : ℕ) : ℝ := ((poissonMeasure rateB) ({n} : Set ℕ)).toReal * g n have ha : Summable a := by have hdirac : Integrable f (Measure.sum fun m : ℕ => (poissonMeasure rateA) ({m} : Set ℕ) • Measure.dirac m) := by simpa only [Measure.sum_smul_dirac] using hf apply Summable.of_norm simpa only [a, norm_mul, Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg] using hdirac.summable_of_dirac have hb : Summable b := by have hdirac : Integrable g (Measure.sum fun n : ℕ => (poissonMeasure rateB) ({n} : Set ℕ) • Measure.dirac n) := by simpa only [Measure.sum_smul_dirac] using hg apply Summable.of_norm simpa only [b, norm_mul, Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg] using hdirac.summable_of_dirac have hfa : (∫ m : ℕ, f m ∂poissonMeasure rateA) = ∑' m, a m := by simpa only [a, smul_eq_mul, measureReal_def] using integral_countable hf have hgb : (∫ n : ℕ, g n ∂poissonMeasure rateB) = ∑' n, b n := by simpa only [b, smul_eq_mul, measureReal_def] using integral_countable hg rw [hfa, hgb] calc _ = ∑' m : ℕ, ∑' n : ℕ, a m * b n := by congr 1 funext m congr 1 funext n dsimp [a, b] ring _ = (∑' m : ℕ, a m) * (∑' n : ℕ, b n) := by simpa only [Summable.tsum_mul_left _ hb] using (Summable.tsum_mul_right (∑' n : ℕ, b n) ha)