Mathlib.Probability.Poisson.Poincare

theorem variance_pi_le_sum_integral_coordinateVariance {iota : Type*} [Fintype iota] [DecidableEq iota] {X : iota → Type*} [(i : iota) → MeasurableSpace (X i)] (mu : (i : iota) → Measure (X i)) [∀ i, IsProbabilityMeasure (mu i)] (F : ((i : iota) → X i) → Real) (hF : MemLp F 2 (Measure.pi mu)) : variance F (Measure.pi mu) ≤ ∑ i : iota, ∫ x, variance (fun y ↦ F (coordinateReplace i x y)) (mu i) ∂(Measure.pi mu) := by classical let e : Fin (card iota) ≃ iota := (Fintype.equivFin iota).symm let phi := MeasurableEquiv.piCongrLeft X e let nu : (k : Fin (card iota)) → Measure (X (e k)) := fun k ↦ mu (e k) let G : ((k : Fin (card iota)) → X (e k)) → Real := F ∘ phi have hmp := measurePreserving_piCongrLeft mu e have hG : MemLp G 2 (Measure.pi nu) := by exact hF.comp_measurePreserving hmp have h := variance_pi_fin (card iota) nu G hG have hvar := hmp.variance_fun_comp hF.aemeasurable rw [show variance F (Measure.pi mu) = variance G (Measure.pi nu) by exact hvar.symm] calc variance G (Measure.pi nu) ≤ ∑ k, ∫ z, variance (fun y ↦ G (update z k y)) (nu k) ∂(Measure.pi nu) := h _ = ∑ k, ∫ x, variance (fun y ↦ F (coordinateReplace (e k) x y)) (mu (e k)) ∂(Measure.pi mu) := by apply Finset.sum_congr rfl intro k _ rw [← hmp.integral_comp'] apply integral_congr_ae filter_upwards with z congr 1 funext y apply congrArg F funext a obtain ⟨j, rfl⟩ := e.surjective a by_cases hj : j = k · subst j simp [phi, coordinateReplace, MeasurableEquiv.piCongrLeft_apply_apply] · simp [phi, coordinateReplace, MeasurableEquiv.piCongrLeft_apply_apply, hj] _ = _ := e.sum_comp (fun i ↦ ∫ x, variance (fun y ↦ F (coordinateReplace i x y)) (mu i) ∂(Measure.pi mu))

theorem nestedPairedPoisson_addOne_poincare {iota kappa : Type*} [Fintype iota] [DecidableEq iota] [Fintype kappa] [DecidableEq kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) (F : (iota → kappa → Nat × Nat) → Real) (hF : MemLp F 2 (nestedPairedPoissonMeasure lambda₁ lambda₂)) (hD₁ : ∀ i j, MemLp (nestedPairAddOneFst (iota := iota) (kappa := kappa) i j F) 2 (nestedPairedPoissonMeasure lambda₁ lambda₂)) (hD₂ : ∀ i j, MemLp (nestedPairAddOneSnd (iota := iota) (kappa := kappa) i j F) 2 (nestedPairedPoissonMeasure lambda₁ lambda₂)) : variance F (nestedPairedPoissonMeasure lambda₁ lambda₂) ≤ Finset.univ.sum (fun i : iota ↦ Finset.univ.sum (fun j : kappa ↦ ((lambda₁ i j : Real) * ∫ x : iota → kappa → Nat × Nat, (nestedPairAddOneFst (iota := iota) (kappa := kappa) (i : iota) (j : kappa) F x) ^ 2 ∂(nestedPairedPoissonMeasure lambda₁ lambda₂)) + ((lambda₂ i j : Real) * ∫ x : iota → kappa → Nat × Nat, (nestedPairAddOneSnd (iota := iota) (kappa := kappa) (i : iota) (j : kappa) F x) ^ 2 ∂(nestedPairedPoissonMeasure lambda₁ lambda₂)))) := by classical let flatIndex := Sigma fun _ : iota ↦ Sigma fun _ : kappa ↦ Fin 2 let flatLambda : flatIndex → NNReal := fun p ↦ Fin.cases (lambda₁ p.1 p.2.1) (fun _ ↦ lambda₂ p.1 p.2.1) p.2.2 let e₁ := piCurry (fun (_ : iota) (_ : Sigma fun _ : kappa ↦ Fin 2) ↦ Nat) let e₂ := MeasurableEquiv.piCongrRight (fun _ : iota ↦ piCurry (fun (_ : kappa) (_ : Fin 2) ↦ Nat)) let e₃ := MeasurableEquiv.piCongrRight (fun _ : iota ↦ MeasurableEquiv.piCongrRight (fun _ : kappa ↦ MeasurableEquiv.piFinTwo (fun _ : Fin 2 ↦ Nat))) let e := e₁.trans (e₂.trans e₃) let mu₀ : Measure (flatIndex → Nat) := poissonPi flatLambda let mu₁ : Measure (iota → (Sigma fun _ : kappa ↦ Fin 2) → Nat) := Measure.pi fun i ↦ Measure.pi fun q ↦ poissonMeasure (flatLambda ⟨i, q⟩) let mu₂ : Measure (iota → kappa → Fin 2 → Nat) := Measure.pi fun i ↦ Measure.pi fun j ↦ Measure.pi fun b ↦ poissonMeasure (flatLambda ⟨i, ⟨j, b⟩⟩) let mu₃ : Measure (iota → kappa → Nat × Nat) := nestedPairedPoissonMeasure lambda₁ lambda₂ have hmp₁ : MeasurePreserving e₁ mu₀ mu₁ := by simpa [e₁, mu₀, mu₁, poissonPi, flatIndex] using (measurePreserving_piCurry_probability (fun (i : iota) (q : Sigma fun _ : kappa ↦ Fin 2) ↦ poissonMeasure (flatLambda ⟨i, q⟩))) have hmp₂ : MeasurePreserving e₂ mu₁ mu₂ := by apply measurePreserving_piCongrRight_probability intro i simpa [mu₁, mu₂, e₂] using (measurePreserving_piCurry_probability (fun (j : kappa) (b : Fin 2) ↦ poissonMeasure (flatLambda ⟨i, ⟨j, b⟩⟩))) have hmp₃ : MeasurePreserving e₃ mu₂ mu₃ := by apply measurePreserving_piCongrRight_probability intro i apply measurePreserving_piCongrRight_probability intro j convert (measurePreserving_piFinTwo (fun b : Fin 2 ↦ poissonMeasure (Fin.cases (lambda₁ i j) (fun _ ↦ lambda₂ i j) b))) using 1 · simp [mu₂, mu₃, e₃, nestedPairedPoissonMeasure, flatLambda] congr 2 have hmp : MeasurePreserving e mu₀ mu₃ := by exact hmp₃.comp (hmp₂.comp hmp₁) have he_apply (z : flatIndex → Nat) (i : iota) (j : kappa) : e z i j = (z ⟨i, ⟨j, 0⟩⟩, z ⟨i, ⟨j, 1⟩⟩) := by rfl have he_update_fst (z : flatIndex → Nat) (i : iota) (j : kappa) : e (update z ⟨i, ⟨j, 0⟩⟩ (z ⟨i, ⟨j, 0⟩⟩ + 1)) = update (e z) i (update (e z i) j ((e z i j).1 + 1, (e z i j).2)) := by funext i' j' rw [he_apply] by_cases hi : i' = i <;> by_cases hj : j' = j · subst i' subst j' simp [he_apply] · subst i' simp [he_apply, hj] · simp [he_apply, hi] · simp [he_apply, hi] have he_update_snd (z : flatIndex → Nat) (i : iota) (j : kappa) : e (update z ⟨i, ⟨j, 1⟩⟩ (z ⟨i, ⟨j, 1⟩⟩ + 1)) = update (e z) i (update (e z i) j ((e z i j).1, (e z i j).2 + 1)) := by funext i' j' rw [he_apply] by_cases hi : i' = i <;> by_cases hj : j' = j · subst i' subst j' simp [he_apply] · subst i' simp [he_apply, hj] · simp [he_apply, hi] · simp [he_apply, hi] let G : (flatIndex → Nat) → Real := F ∘ e have hG : MemLp G 2 mu₀ := hF.comp_measurePreserving hmp have hDpoint_fst (i : iota) (j : kappa) : coordinateAddOne ⟨i, ⟨j, 0⟩⟩ G = nestedPairAddOneFst i j F ∘ e := by funext z simp only [coordinateAddOne, G, Function.comp_apply, nestedPairAddOneFst] rw [he_update_fst] have hDpoint_snd (i : iota) (j : kappa) : coordinateAddOne ⟨i, ⟨j, 1⟩⟩ G = nestedPairAddOneSnd i j F ∘ e := by funext z simp only [coordinateAddOne, G, Function.comp_apply, nestedPairAddOneSnd] rw [he_update_snd] have hDG (p : flatIndex) : MemLp (coordinateAddOne p G) 2 mu₀ := by rcases p with ⟨i, j, b⟩ have hb : b = 0 ∨ b = 1 := by omega rcases hb with rfl | rfl · rw [hDpoint_fst] exact (hD₁ i j).comp_measurePreserving hmp · rw [hDpoint_snd] exact (hD₂ i j).comp_measurePreserving hmp have hflat := poissonPi_addOne_poincare flatLambda G hG hDG have henergy_fst (i : iota) (j : kappa) : (∫ z, (coordinateAddOne ⟨i, ⟨j, 0⟩⟩ G z) ^ 2 ∂mu₀) = ∫ x, (nestedPairAddOneFst i j F x) ^ 2 ∂mu₃ := by rw [← hmp.integral_comp'] apply integral_congr_ae filter_upwards with z rw [congrFun (hDpoint_fst i j) z] rfl have henergy_snd (i : iota) (j : kappa) : (∫ z, (coordinateAddOne ⟨i, ⟨j, 1⟩⟩ G z) ^ 2 ∂mu₀) = ∫ x, (nestedPairAddOneSnd i j F x) ^ 2 ∂mu₃ := by rw [← hmp.integral_comp'] apply integral_congr_ae filter_upwards with z rw [congrFun (hDpoint_snd i j) z] rfl have hvar := hmp.variance_fun_comp hF.aemeasurable rw [show variance F mu₃ = variance G mu₀ by exact hvar.symm] calc variance G mu₀ ≤ ∑ p : flatIndex, (flatLambda p : Real) * ∫ z, (coordinateAddOne p G z) ^ 2 ∂mu₀ := hflat _ = _ := by rw [Fintype.sum_sigma] apply Finset.sum_congr rfl intro i _ rw [Fintype.sum_sigma] apply Finset.sum_congr rfl intro j _ rw [Fin.sum_univ_two, henergy_fst, henergy_snd] congr 2

lemma supportTruncation_finiteSupport (K : Nat) (f : Nat → Real) : (support (supportTruncation K f)).Finite := by refine (Set.finite_Iio K).subset ?_ intro n hn simp only [Function.mem_support] at hn by_contra hnot have hkn : ¬ n < K := by simpa using hnot exact hn (by simp [supportTruncation, hkn])

lemma memLp_poissonMeasure_of_finiteSupport (lambda : NNReal) (f : Nat → Real) (hf : (support f).Finite) : MemLp f 2 (poissonMeasure lambda) := by -- On the discrete domain measurability is automatic. Use the explicit Poisson -- integrability criterion; a series supported on the finite support of `f` is summable. refine (memLp_two_iff_integrable_sq (measurable_of_countable _).aestronglyMeasurable).2 ?_ rw [integrable_poissonMeasure_iff] apply summable_of_hasFiniteSupport refine hf.subset ?_ intro n hn simp only [Function.mem_support] at hn ⊢ intro hfn simp [hfn] at hn

lemma finiteSupport_addOne (f : Nat → Real) (hf : (support f).Finite) : (support (addOne f)).Finite := by -- The support is contained in `support f ∪ {n | n+1 ∈ support f}`; the successor -- preimage of a finite set is finite. have hpre : ((fun n : Nat ↦ n + 1) ⁻¹' support f).Finite := hf.preimage (Nat.succ_injective.injOn) refine (hf.union hpre).subset ?_ intro n hn simp only [Function.mem_support, Set.mem_union, Set.mem_preimage] at hn ⊢ by_contra hnot simp only [not_or, not_not] at hnot exact hn (by simp [addOne, hnot.1, hnot.2])

theorem supportTruncation_integral_sq_tendsto_zero (lambda : NNReal) (f : Nat → Real) (hf : MemLp f 2 (poissonMeasure lambda)) : Tendsto (fun K ↦ ∫ n, (supportTruncation K f n - f n) ^ 2 ∂(poissonMeasure lambda)) atTop (nhds 0) := by -- Rewrite the integral as the weighted series and identify it with the tail of the -- summable nonnegative series supplied by `hf.integrable_sq`. let a : Nat → Real := fun n ↦ exp (-(lambda : Real)) * (lambda : Real) ^ n / factorial n * f n ^ 2 have htail : Tendsto (fun K ↦ ∑' (n : {n // n ∉ (Finset.range K : Set Nat)}), a n) atTop (nhds 0) := (tendsto_tsum_compl_atTop_zero a).comp tendsto_finset_range convert htail using 1 funext K have hInt : Integrable (fun n ↦ (supportTruncation K f n - f n) ^ 2) (poissonMeasure lambda) := by refine hf.integrable_sq.mono (measurable_of_countable _).aestronglyMeasurable ?_ filter_upwards with n by_cases hn : n < K · simp [supportTruncation, hn, sq_nonneg] · simp [supportTruncation, hn] rw [integral_poissonMeasure' hInt] calc _ = ∑' n : Nat, ({n : Nat | n ∉ (Finset.range K : Set Nat)}).indicator a n := by apply tsum_congr intro n by_cases hn : n < K <;> simp [a, indicator, supportTruncation, hn] _ = _ := (tsum_subtype ({n : Nat | n ∉ (Finset.range K : Set Nat)}) a).symm

theorem supportTruncation_addOne_integral_sq_tendsto_zero (lambda : NNReal) (f : Nat → Real) (hf : MemLp f 2 (poissonMeasure lambda)) (hdf : MemLp (addOne f) 2 (poissonMeasure lambda)) : Tendsto (fun K ↦ ∫ n, (addOne (supportTruncation K f) n - addOne f n) ^ 2 ∂(poissonMeasure lambda)) atTop (nhds 0) := by -- The identity `f (n+1) = addOne f n + f n` makes the shifted sequence square-integrable. -- Its squared norm, together with that of `f`, dominates every truncated add-one error; -- pointwise the error is eventually zero, so dominated convergence applies. have hshift : MemLp (fun n ↦ f (n + 1)) 2 (poissonMeasure lambda) := by have h := hdf.add hf convert h using 1 ext n simp [addOne] have hbound : Integrable (fun n ↦ 2 * (f (n + 1) ^ 2 + f n ^ 2)) (poissonMeasure lambda) := (hshift.integrable_sq.add hf.integrable_sq).const_mul 2 simpa only [integral_zero] using (tendsto_integral_of_dominated_convergence (μ := poissonMeasure lambda) (F := fun K n ↦ (addOne (supportTruncation K f) n - addOne f n) ^ 2) (f := fun _ ↦ (0 : Real)) (fun n ↦ 2 * (f (n + 1) ^ 2 + f n ^ 2)) (fun K ↦ (measurable_of_countable _).aestronglyMeasurable) hbound (fun K ↦ by filter_upwards with n simp only [Real.norm_eq_abs, abs_sq] by_cases hn : n < K <;> by_cases hsn : n + 1 < K <;> simp [addOne, supportTruncation, hn, hsn] <;> nlinarith [sq_nonneg (f n), sq_nonneg (f (n + 1)), sq_nonneg (f n + f (n + 1))]) (by filter_upwards with n apply tendsto_atTop_of_eventually_const (i₀ := n + 2) intro K hK have hn : n < K := by omega have hsn : n + 1 < K := by omega simp [addOne, supportTruncation, hn, hsn]))

theorem variance_tendsto_of_integral_sq_sub_tendsto_zero {alpha : Type*} [MeasurableSpace alpha] (mu : Measure alpha) [IsProbabilityMeasure mu] (f : Nat → alpha → Real) (g : alpha → Real) (hf : ∀ K, MemLp (f K) 2 mu) (hg : MemLp g 2 mu) (hconv : Tendsto (fun K ↦ ∫ x, (f K x - g x) ^ 2 ∂mu) atTop (nhds 0)) : Tendsto (fun K ↦ variance (f K) mu) atTop (nhds (variance g mu)) := by -- Squared L² convergence implies convergence of means and second moments by -- Cauchy–Schwarz on a probability space; conclude from `variance_eq_sub`. let d : Nat → alpha → Real := fun K x ↦ f K x - g x have hd (K : Nat) : MemLp (d K) 2 mu := by have h := (hf K).sub hg convert h using 1 ext x rfl have hCS (u v : alpha → Real) (hu : MemLp u 2 mu) (hv : MemLp v 2 mu) : |∫ x, u x * v x ∂mu| ≤ sqrt (∫ x, u x ^ 2 ∂mu) * sqrt (∫ x, v x ^ 2 ∂mu) := by calc |∫ x, u x * v x ∂mu| = ‖∫ x, u x * v x ∂mu‖ := by rw [Real.norm_eq_abs] _ ≤ ∫ x, ‖u x * v x‖ ∂mu := norm_integral_le_integral_norm _ _ = ∫ x, ‖u x‖ * ‖v x‖ ∂mu := by apply integral_congr_ae filter_upwards with x rw [norm_mul] _ ≤ (∫ x, ‖u x‖ ^ (2 : Real) ∂mu) ^ ((1 : Real) / 2) * (∫ x, ‖v x‖ ^ (2 : Real) ∂mu) ^ ((1 : Real) / 2) := integral_mul_norm_le_Lp_mul_Lq Real.HolderConjugate.two_two (by simpa using hu) (by simpa using hv) _ = _ := by rw [← Real.sqrt_eq_rpow, ← Real.sqrt_eq_rpow] congr 2 <;> apply integral_congr_ae <;> filter_upwards with x <;> simp [sq_abs] have hsqrt : Tendsto (fun K ↦ sqrt (∫ x, d K x ^ 2 ∂mu)) atTop (nhds 0) := by have := Real.continuous_sqrt.continuousAt.tendsto.comp hconv convert this using 1 · funext K rfl · simp have hdconv : Tendsto (fun K ↦ ∫ x, d K x ^ 2 ∂mu) atTop (nhds 0) := by simpa [d] using hconv have hmeanDiff : Tendsto (fun K ↦ ∫ x, d K x ∂mu) atTop (nhds 0) := by refine squeeze_zero_norm (a := fun K ↦ sqrt (∫ x, d K x ^ 2 ∂mu)) ?_ hsqrt · intro K simpa using (hCS (d K) (fun _ ↦ (1 : Real)) (hd K) (memLp_const 1)) have hcross : Tendsto (fun K ↦ ∫ x, g x * d K x ∂mu) atTop (nhds 0) := by refine squeeze_zero_norm (a := fun K ↦ sqrt (∫ x, g x ^ 2 ∂mu) * sqrt (∫ x, d K x ^ 2 ∂mu)) ?_ ?_ · intro K simpa [mul_comm] using hCS g (d K) hg (hd K) · simpa using ((tendsto_const_nhds : Tendsto (fun _ : Nat ↦ sqrt (∫ x, g x ^ 2 ∂mu)) atTop (nhds (sqrt (∫ x, g x ^ 2 ∂mu)))).mul hsqrt) have hmean : Tendsto (fun K ↦ ∫ x, f K x ∂mu) atTop (nhds (∫ x, g x ∂mu)) := by convert (tendsto_const_nhds.add hmeanDiff) using 1 · funext K rw [← integral_add (hg.integrable one_le_two) ((hd K).integrable one_le_two)] apply integral_congr_ae filter_upwards with x simp [d] · simp have hsecond : Tendsto (fun K ↦ ∫ x, (f K x) ^ 2 ∂mu) atTop (nhds (∫ x, g x ^ 2 ∂mu)) := by convert ((tendsto_const_nhds : Tendsto (fun _ : Nat ↦ ∫ x, g x ^ 2 ∂mu) atTop (nhds (∫ x, g x ^ 2 ∂mu))).add (hdconv.add (hcross.const_mul 2))) using 1 · funext K calc (∫ x, f K x ^ 2 ∂mu) = ∫ x, g x ^ 2 + (d K x ^ 2 + 2 * (g x * d K x)) ∂mu := by apply integral_congr_ae filter_upwards with x simp [d] ring _ = (∫ x, g x ^ 2 ∂mu) + ∫ x, d K x ^ 2 + 2 * (g x * d K x) ∂mu := integral_add hg.integrable_sq ((hd K).integrable_sq.add ((MemLp.integrable_mul hg (hd K)).const_mul 2)) _ = _ := by congr 1 calc (∫ x, d K x ^ 2 + 2 * (g x * d K x) ∂mu) = (∫ x, d K x ^ 2 ∂mu) + ∫ x, 2 * (g x * d K x) ∂mu := integral_add (hd K).integrable_sq ((MemLp.integrable_mul hg (hd K)).const_mul 2) _ = _ := by rw [integral_const_mul] · simp convert hsecond.sub (hmean.pow 2) using 1 · funext K rw [variance_eq_sub (hf K)] rfl · rw [variance_eq_sub hg] rfl

theorem measurePreserving_piCurry_probability {alpha : Type*} {beta : alpha → Type*} [Fintype alpha] [∀ i, Fintype (beta i)] {X : (i : alpha) → beta i → Type*} [∀ i j, MeasurableSpace (X i j)] (mu : (i : alpha) → (j : beta i) → Measure (X i j)) [∀ i j, IsProbabilityMeasure (mu i j)] : MeasurePreserving (piCurry X) (Measure.pi fun p : Sigma beta => mu p.1 p.2) (Measure.pi fun i => Measure.pi (mu i)) := by refine ⟨(piCurry X).measurable, ?_⟩ simpa only [Measure.infinitePi_eq_pi] using Measure.infinitePi_map_piCurry mu

@[simp] theorem nestedPairedPoissonUnflattening_apply {iota kappa : Type*} [Fintype iota] [Fintype kappa] (z : NestedPairedPoissonIndex iota kappa → Nat) (i : iota) (j : kappa) : nestedPairedPoissonUnflattening iota kappa z i j = (z ⟨i, ⟨j, 0⟩⟩, z ⟨i, ⟨j, 1⟩⟩) := by rfl

@[simp] theorem nestedPairedPoissonFlattening_apply_zero {iota kappa : Type*} [Fintype iota] [Fintype kappa] (x : iota → kappa → Nat × Nat) (i : iota) (j : kappa) : nestedPairedPoissonFlattening iota kappa x ⟨i, ⟨j, 0⟩⟩ = (x i j).1 := by rfl

@[simp] theorem nestedPairedPoissonFlattening_apply_one {iota kappa : Type*} [Fintype iota] [Fintype kappa] (x : iota → kappa → Nat × Nat) (i : iota) (j : kappa) : nestedPairedPoissonFlattening iota kappa x ⟨i, ⟨j, 1⟩⟩ = (x i j).2 := by rfl

theorem measurePreserving_nestedPairedPoissonUnflattening {iota kappa : Type*} [Fintype iota] [Fintype kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) : MeasurePreserving (nestedPairedPoissonUnflattening iota kappa) (poissonPi (nestedPairedPoissonRates lambda₁ lambda₂)) (nestedPairedPoissonMeasure lambda₁ lambda₂) := by -- Follow the three public transports above: curry the outer Sigma, curry each inner -- Sigma, and turn each `Fin 2 → Nat` into a pair. let flatIndex := Sigma fun _ : iota => Sigma fun _ : kappa => Fin 2 let flatLambda : flatIndex → NNReal := fun p => Fin.cases (lambda₁ p.1 p.2.1) (fun _ => lambda₂ p.1 p.2.1) p.2.2 let e₁ := piCurry (fun (_ : iota) (_ : Sigma fun _ : kappa => Fin 2) => Nat) let e₂ := MeasurableEquiv.piCongrRight (fun _ : iota => piCurry (fun (_ : kappa) (_ : Fin 2) => Nat)) let e₃ := MeasurableEquiv.piCongrRight (fun _ : iota => MeasurableEquiv.piCongrRight (fun _ : kappa => MeasurableEquiv.piFinTwo (fun _ : Fin 2 => Nat))) let mu₀ : Measure (flatIndex → Nat) := poissonPi flatLambda let mu₁ : Measure (iota → (Sigma fun _ : kappa => Fin 2) → Nat) := Measure.pi fun i => Measure.pi fun q => poissonMeasure (flatLambda ⟨i, q⟩) let mu₂ : Measure (iota → kappa → Fin 2 → Nat) := Measure.pi fun i => Measure.pi fun j => Measure.pi fun b => poissonMeasure (flatLambda ⟨i, ⟨j, b⟩⟩) let mu₃ : Measure (iota → kappa → Nat × Nat) := nestedPairedPoissonMeasure lambda₁ lambda₂ have hmp₁ : MeasurePreserving e₁ mu₀ mu₁ := by simpa [e₁, mu₀, mu₁, poissonPi, flatIndex] using (measurePreserving_piCurry_probability (fun (i : iota) (q : Sigma fun _ : kappa => Fin 2) => poissonMeasure (flatLambda ⟨i, q⟩))) have hmp₂ : MeasurePreserving e₂ mu₁ mu₂ := by apply measurePreserving_piCongrRight_probability intro i simpa [mu₁, mu₂, e₂] using (measurePreserving_piCurry_probability (fun (j : kappa) (b : Fin 2) => poissonMeasure (flatLambda ⟨i, ⟨j, b⟩⟩))) have hmp₃ : MeasurePreserving e₃ mu₂ mu₃ := by apply measurePreserving_piCongrRight_probability intro i apply measurePreserving_piCongrRight_probability intro j convert (measurePreserving_piFinTwo (fun b : Fin 2 => poissonMeasure (Fin.cases (lambda₁ i j) (fun _ => lambda₂ i j) b))) using 1 · simp congr 2 have hmp := hmp₃.comp (hmp₂.comp hmp₁) change MeasurePreserving (e₃ ∘ e₂ ∘ e₁) mu₀ mu₃ exact hmp

theorem nestedPairedPoissonUnflattening_update_fst {iota kappa : Type*} [Fintype iota] [DecidableEq iota] [Fintype kappa] [DecidableEq kappa] (z : NestedPairedPoissonIndex iota kappa → Nat) (i : iota) (j : kappa) : nestedPairedPoissonUnflattening iota kappa (update z ⟨i, ⟨j, 0⟩⟩ (z ⟨i, ⟨j, 0⟩⟩ + 1)) = update (nestedPairedPoissonUnflattening iota kappa z) i (update (nestedPairedPoissonUnflattening iota kappa z i) j ((nestedPairedPoissonUnflattening iota kappa z i j).1 + 1, (nestedPairedPoissonUnflattening iota kappa z i j).2)) := by funext i' j' rw [nestedPairedPoissonUnflattening_apply] by_cases hi : i' = i <;> by_cases hj : j' = j · subst i' subst j' simp · subst i' simp [hj] · simp [hi] · simp [hi]

theorem nestedPairedPoissonUnflattening_update_snd {iota kappa : Type*} [Fintype iota] [DecidableEq iota] [Fintype kappa] [DecidableEq kappa] (z : NestedPairedPoissonIndex iota kappa → Nat) (i : iota) (j : kappa) : nestedPairedPoissonUnflattening iota kappa (update z ⟨i, ⟨j, 1⟩⟩ (z ⟨i, ⟨j, 1⟩⟩ + 1)) = update (nestedPairedPoissonUnflattening iota kappa z) i (update (nestedPairedPoissonUnflattening iota kappa z i) j ((nestedPairedPoissonUnflattening iota kappa z i j).1, (nestedPairedPoissonUnflattening iota kappa z i j).2 + 1)) := by funext i' j' rw [nestedPairedPoissonUnflattening_apply] by_cases hi : i' = i <;> by_cases hj : j' = j · subst i' subst j' simp · subst i' simp [hj] · simp [hi] · simp [hi]

lemma poissonWeight_hasSum_one (lambda : NNReal) : HasSum (poissonWeight lambda) 1 := by change HasSum (fun n ↦ exp (-(lambda : Real)) * (lambda : Real) ^ n / factorial n) 1 simpa using ProbabilityTheory.hasSum_one_poissonMeasure lambda

lemma poissonWeight_succ_shift (lambda : NNReal) (n : Nat) : ((n + 1 : Nat) : Real) * poissonWeight lambda (n + 1) = (lambda : Real) * poissonWeight lambda n := by -- Unfold the weight, rewrite `Nat.factorial_succ`, and cancel the positive successor cast; -- no division by `lambda` is needed, so the same calculation covers `lambda = 0`. simp only [poissonWeight, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, pow_succ] field_simp

lemma poissonWeight_shift (lambda : NNReal) {n : Nat} (hn : 0 < n) : (n : Real) * poissonWeight lambda n = (lambda : Real) * poissonWeight lambda (n - 1) := by -- Write `n` as `(n - 1) + 1` using `hn`, then apply the successor shift identity. have h : n - 1 + 1 = n := Nat.sub_add_cancel hn simpa only [h] using poissonWeight_succ_shift lambda (n - 1)

theorem ENNReal_tsum_lt_eq_tsum_fin (a : Nat → Nat → ENNReal) : (∑' m : Nat, ∑' n : Nat, if n < m then a n m else 0) = ∑' m : Nat, ∑' n : Fin m, a n m := by -- Convert the finite `Fin m` tsum with `Finset.tsum_subtype`, then use indicator/subtype -- reindexing. ENNReal Tonelli permits every exchange without a summability premise. congr 1 funext m calc (∑' n : Nat, if n < m then a n m else 0) = ∑' n : Nat, indicator {n | n < m} (fun n => a n m) n := by congr 1 funext n simp only [Set.indicator_apply] rfl _ = ∑' n : {n : Nat // n < m}, a n m := (tsum_subtype {n : Nat | n < m} (fun n => a n m)).symm _ = ∑' n : Fin m, a n m := by symm simpa using (Fin.equivSubtype.tsum_eq (fun n : {n : Nat // n < m} => a n m))

theorem ENNReal_tsum_upperTriangle_gap (a : Nat → Nat → ENNReal) : (∑' n : Nat, ∑' k : Nat, a n (n + k + 1)) = ∑' m : Nat, ∑' n : Fin m, a n m := by -- Reindex the countable type of pairs `(n,k)` by the strict triangle -- `Σ m, Fin m`, via `(n,k) ↦ ⟨n+k+1, n⟩`, and use `Equiv.tsum_eq`. let e : Nat × Nat ≃ Σ m : Nat, Fin m := { toFun := fun p => ⟨p.1 + p.2 + 1, ⟨p.1, by omega⟩⟩ invFun := fun q => (q.2.1, q.1 - q.2.1 - 1) left_inv := by intro p apply Prod.ext · rfl · simp only omega right_inv := by intro q have h : q.2.1 + (q.1 - q.2.1 - 1) + 1 = q.1 := by omega apply Sigma.eq h dsimp apply Fin.ext have cast_val {r s : Nat} (hrs : r = s) (i : Fin r) : (hrs ▸ i).val = i.val := by subst s rfl exact cast_val h _ } calc (∑' n : Nat, ∑' k : Nat, a n (n + k + 1)) = ∑' p : Nat × Nat, a p.1 (p.1 + p.2 + 1) := ENNReal.tsum_prod.symm _ = ∑' q : Σ m : Nat, Fin m, a q.2 q.1 := by rw [← e.tsum_eq (fun q : Σ m : Nat, Fin m => a q.2 q.1)] rfl _ = ∑' m : Nat, ∑' n : Fin m, a n m := ENNReal.tsum_sigma (fun (m : Nat) (n : Fin m) => a n m)

theorem integral_nestedPairedCoordinateProduct_eq_prod {iota kappa : Type*} [Fintype iota] [Fintype kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) (g : NestedPairedPoissonIndex iota kappa → Nat → Real) : (∫ x, nestedPairedCoordinateProduct g x ∂(nestedPairedPoissonMeasure lambda₁ lambda₂)) = ∏ p, ∫ n, g p n ∂(poissonMeasure (nestedPairedPoissonRates lambda₁ lambda₂ p)) := by let hmp := measurePreserving_nestedPairedPoissonFlattening lambda₁ lambda₂ calc _ = ∫ z, ∏ p, g p (z p) ∂(poissonPi (nestedPairedPoissonRates lambda₁ lambda₂)) := by simpa [nestedPairedCoordinateProduct] using hmp.integral_comp' (fun z => ∏ p, g p (z p)) _ = _ := by exact MeasureTheory.integral_fintype_prod_eq_prod g

theorem integral_sq_nestedPairedCoordinateProduct_eq_prod {iota kappa : Type*} [Fintype iota] [Fintype kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) (g : NestedPairedPoissonIndex iota kappa → Nat → Real) : (∫ x, (nestedPairedCoordinateProduct g x) ^ 2 ∂(nestedPairedPoissonMeasure lambda₁ lambda₂)) = ∏ p, ∫ n, (g p n) ^ 2 ∂(poissonMeasure (nestedPairedPoissonRates lambda₁ lambda₂ p)) := by let hmp := measurePreserving_nestedPairedPoissonFlattening lambda₁ lambda₂ calc _ = ∫ z, (∏ p, g p (z p)) ^ 2 ∂(poissonPi (nestedPairedPoissonRates lambda₁ lambda₂)) := by simpa [nestedPairedCoordinateProduct] using hmp.integral_comp' (fun z => (∏ p, g p (z p)) ^ 2) _ = ∫ z, ∏ p, (g p (z p)) ^ 2 ∂(poissonPi (nestedPairedPoissonRates lambda₁ lambda₂)) := by congr with z simp [Finset.prod_pow] _ = _ := by exact MeasureTheory.integral_fintype_prod_eq_prod (fun p n => (g p n) ^ 2)

theorem memLp_two_nestedPairedCoordinateProduct {iota kappa : Type*} [Fintype iota] [Fintype kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) (g : NestedPairedPoissonIndex iota kappa → Nat → Real) (hg : ∀ p, Integrable (fun n => (g p n) ^ 2) (poissonMeasure (nestedPairedPoissonRates lambda₁ lambda₂ p))) : MemLp (nestedPairedCoordinateProduct g) 2 (nestedPairedPoissonMeasure lambda₁ lambda₂) := by have hflat : Integrable (fun z => (∏ p, g p (z p)) ^ 2) (poissonPi (nestedPairedPoissonRates lambda₁ lambda₂)) := by have hprod := Integrable.fintype_prod (𝕜 := Real) hg simpa [poissonPi, Finset.prod_pow] using hprod have hnested := (measurePreserving_nestedPairedPoissonFlattening lambda₁ lambda₂) |>.integrable_comp_of_integrable hflat refine (memLp_two_iff_integrable_sq (measurable_of_countable _).aestronglyMeasurable).2 ?_ simpa [nestedPairedCoordinateProduct, Function.comp_def] using hnested

theorem integral_nestedPaired_cellwise_product_eq_prod {iota kappa : Type*} [Fintype iota] [Fintype kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) (g₁ g₂ : iota → kappa → Nat → Real) : (∫ x, ∏ i, ∏ j, g₁ i j (x i j).1 * g₂ i j (x i j).2 ∂(nestedPairedPoissonMeasure lambda₁ lambda₂)) = ∏ i, ∏ j, ((∫ n, g₁ i j n ∂(poissonMeasure (lambda₁ i j))) * (∫ n, g₂ i j n ∂(poissonMeasure (lambda₂ i j)))) := by let g : NestedPairedPoissonIndex iota kappa → Nat → Real := fun p => Fin.cases (g₁ p.1 p.2.1) (fun _ => g₂ p.1 p.2.1) p.2.2 have h := integral_nestedPairedCoordinateProduct_eq_prod lambda₁ lambda₂ g simp only [nestedPairedCoordinateProduct, g, Fintype.prod_sigma, Fin.prod_univ_two, nestedPairedPoissonFlattening_apply_zero, nestedPairedPoissonFlattening_apply_one, nestedPairedPoissonRates] at h have hone : (1 : Fin 2) = succ 0 := rfl rw [hone] at h simpa only [Fin.cases_zero, Fin.cases_succ] using h

theorem integrable_natCast_pow_poissonMeasure (lambda : NNReal) (degree : Nat) : Integrable (fun n : Nat => (n : Real) ^ degree) (poissonMeasure lambda) := by apply integrable_pow_of_integrable_exp_mul (t := 1) (by norm_num) · rw [integrable_poissonMeasure_iff] have h := (Real.summable_pow_div_factorial ((lambda : Real) * exp 1)).mul_left (exp (-(lambda : Real))) simpa [Real.norm_eq_abs, Real.abs_exp, Real.exp_nat_mul, mul_pow, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using h · refine Integrable.mono (integrable_const (μ := poissonMeasure lambda) (c := (1 : Real))) ?_ (ae_of_all _ fun n => ?_) · fun_prop · simp only [Real.norm_eq_abs, Real.abs_exp, norm_one] rw [Real.exp_le_one_iff] norm_num

theorem integrable_nestedPairedTotalCount_pow {iota kappa : Type*} [Fintype iota] [Fintype kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) (degree : Nat) : Integrable (fun x : iota → kappa → Nat × Nat => (nestedPairedTotalCount x : Real) ^ degree) (nestedPairedPoissonMeasure lambda₁ lambda₂) := by let rates := nestedPairedPoissonRates lambda₁ lambda₂ let S : (NestedPairedPoissonIndex iota kappa → Nat) → Real := fun z => ∑ p, (z p : Real) have hpos : Integrable (fun z => exp (1 * S z)) (poissonPi rates) := by have hcoord : ∀ p, Integrable (fun n : Nat => exp (n : Real)) (poissonMeasure (rates p)) := by intro p rw [integrable_poissonMeasure_iff] have h := (Real.summable_pow_div_factorial ((rates p : Real) * exp 1)).mul_left (exp (-(rates p : Real))) simpa [Real.norm_eq_abs, Real.abs_exp, Real.exp_nat_mul, mul_pow, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using h change Integrable _ (Measure.pi fun p => poissonMeasure (rates p)) simpa [S, one_mul, Real.exp_sum] using (Integrable.fintype_prod (𝕜 := Real) hcoord) have hneg : Integrable (fun z => exp (-1 * S z)) (poissonPi rates) := by change Integrable _ (Measure.pi fun p => poissonMeasure (rates p)) refine Integrable.mono (integrable_const (μ := Measure.pi fun p => poissonMeasure (rates p)) (c := (1 : Real))) (measurable_of_countable _).aestronglyMeasurable (ae_of_all _ fun z => ?_) simp only [Real.norm_eq_abs, Real.abs_exp, norm_one] rw [Real.exp_le_one_iff] have hs : 0 ≤ ∑ p, (z p : Real) := by positivity dsimp [S] linarith have hflat : Integrable (fun z => (S z) ^ degree) (poissonPi rates) := integrable_pow_of_integrable_exp_mul (t := 1) (by norm_num) hpos hneg degree have hcomp := (measurePreserving_nestedPairedPoissonFlattening lambda₁ lambda₂) |>.integrable_comp_of_integrable hflat convert hcomp using 1 funext x congr 1 simp only [nestedPairedTotalCount, S, Nat.cast_sum, Nat.cast_add] rw [Fintype.sum_sigma] simp only [Fintype.sum_sigma] simp [Fin.sum_univ_two]

theorem memLp_nestedPairedPoisson_of_polynomial_bound {iota kappa : Type*} [Fintype iota] [Fintype kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) (F : (iota → kappa → Nat × Nat) → Real) (hF : Measurable F) (C : Real) (degree : Nat) (hbound : ∀ x, |F x| ≤ C * (1 + (nestedPairedTotalCount x : Real)) ^ degree) : MemLp F 2 (nestedPairedPoissonMeasure lambda₁ lambda₂) := by let T : (iota → kappa → Nat × Nat) → Real := fun x => (nestedPairedTotalCount x : Real) have hmoment : Integrable (fun x => (T x) ^ (2 * degree)) (nestedPairedPoissonMeasure lambda₁ lambda₂) := by simpa [T] using integrable_nestedPairedTotalCount_pow lambda₁ lambda₂ (2 * degree) have hone : Integrable (fun _ : iota → kappa → Nat × Nat => (1 : Real)) (nestedPairedPoissonMeasure lambda₁ lambda₂) := by simpa using integrable_nestedPairedTotalCount_pow lambda₁ lambda₂ 0 have hshift : Integrable (fun x => (1 + T x) ^ (2 * degree)) (nestedPairedPoissonMeasure lambda₁ lambda₂) := by refine Integrable.mono ((hone.add hmoment).const_mul ((2 : Real) ^ (2 * degree - 1))) (measurable_of_countable _).aestronglyMeasurable (ae_of_all _ fun x => ?_) rw [Real.norm_eq_abs, abs_of_nonneg (pow_nonneg (by positivity) _)] rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (by positivity) (add_nonneg (by positivity) (pow_nonneg (by positivity) _)))] simpa only [Pi.add_apply, one_pow] using (add_pow_le (a := (1 : Real)) (b := T x) (by positivity) (by positivity) (2 * degree)) refine (memLp_two_iff_integrable_sq hF.aestronglyMeasurable).2 ?_ refine Integrable.mono (hshift.const_mul (C ^ 2)) (measurable_of_countable _).aestronglyMeasurable (ae_of_all _ fun x => ?_) rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (sq_nonneg _) (pow_nonneg (by positivity) _))] calc F x ^ 2 = |F x| ^ 2 := (sq_abs (F x)).symm _ ≤ (C * (1 + T x) ^ degree) ^ 2 := by gcongr; exact hbound x _ = C ^ 2 * (1 + T x) ^ (2 * degree) := by simp [mul_pow, ← pow_mul, Nat.mul_comm]

theorem memLp_nestedPairAddOneFst_of_polynomial_bound {iota kappa : Type*} [Fintype iota] [DecidableEq iota] [Fintype kappa] [DecidableEq kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) (F : (iota → kappa → Nat × Nat) → Real) (C : Real) (degree : Nat) (hC : 0 ≤ C) (hbound : ∀ x, |F x| ≤ C * (1 + (nestedPairedTotalCount x : Real)) ^ degree) (i : iota) (j : kappa) : MemLp (nestedPairAddOneFst i j F) 2 (nestedPairedPoissonMeasure lambda₁ lambda₂) := by let upd : (iota → kappa → Nat × Nat) → (iota → kappa → Nat × Nat) := fun x => update x i (update (x i) j ((x i j).1 + 1, (x i j).2)) apply memLp_nestedPairedPoisson_of_polynomial_bound lambda₁ lambda₂ (nestedPairAddOneFst i j F) (measurable_of_countable _) (2 * C * 2 ^ degree) degree intro x change |F (upd x) - F x| ≤ (2 * C * 2 ^ degree) * (1 + (nestedPairedTotalCount x : Real)) ^ degree have hcount : nestedPairedTotalCount (upd x) = nestedPairedTotalCount x + 1 := by exact nestedPairedTotalCount_update_fst x i j have hbase_update : 1 + (nestedPairedTotalCount (upd x) : Real) ≤ 2 * (1 + (nestedPairedTotalCount x : Real)) := by rw [hcount, Nat.cast_add, Nat.cast_one] have ht : 0 ≤ (nestedPairedTotalCount x : Real) := by positivity linarith have hbase_old : 1 + (nestedPairedTotalCount x : Real) ≤ 2 * (1 + (nestedPairedTotalCount x : Real)) := by have ht : 0 ≤ (nestedPairedTotalCount x : Real) := by positivity linarith calc |F (upd x) - F x| ≤ |F (upd x)| + |F x| := abs_sub _ _ _ ≤ C * (1 + (nestedPairedTotalCount (upd x) : Real)) ^ degree + C * (1 + (nestedPairedTotalCount x : Real)) ^ degree := add_le_add (hbound (upd x)) (hbound x) _ ≤ C * (2 * (1 + (nestedPairedTotalCount x : Real))) ^ degree + C * (2 * (1 + (nestedPairedTotalCount x : Real))) ^ degree := by gcongr _ = (2 * C * 2 ^ degree) * (1 + (nestedPairedTotalCount x : Real)) ^ degree := by simp [mul_pow] ring

theorem memLp_nestedPairAddOneSnd_of_polynomial_bound {iota kappa : Type*} [Fintype iota] [DecidableEq iota] [Fintype kappa] [DecidableEq kappa] (lambda₁ lambda₂ : iota → kappa → NNReal) (F : (iota → kappa → Nat × Nat) → Real) (C : Real) (degree : Nat) (hC : 0 ≤ C) (hbound : ∀ x, |F x| ≤ C * (1 + (nestedPairedTotalCount x : Real)) ^ degree) (i : iota) (j : kappa) : MemLp (nestedPairAddOneSnd i j F) 2 (nestedPairedPoissonMeasure lambda₁ lambda₂) := by let upd : (iota → kappa → Nat × Nat) → (iota → kappa → Nat × Nat) := fun x => update x i (update (x i) j ((x i j).1, (x i j).2 + 1)) apply memLp_nestedPairedPoisson_of_polynomial_bound lambda₁ lambda₂ (nestedPairAddOneSnd i j F) (measurable_of_countable _) (2 * C * 2 ^ degree) degree intro x change |F (upd x) - F x| ≤ (2 * C * 2 ^ degree) * (1 + (nestedPairedTotalCount x : Real)) ^ degree have hcount : nestedPairedTotalCount (upd x) = nestedPairedTotalCount x + 1 := by exact nestedPairedTotalCount_update_snd x i j have hbase_update : 1 + (nestedPairedTotalCount (upd x) : Real) ≤ 2 * (1 + (nestedPairedTotalCount x : Real)) := by rw [hcount, Nat.cast_add, Nat.cast_one] have ht : 0 ≤ (nestedPairedTotalCount x : Real) := by positivity linarith have hbase_old : 1 + (nestedPairedTotalCount x : Real) ≤ 2 * (1 + (nestedPairedTotalCount x : Real)) := by have ht : 0 ≤ (nestedPairedTotalCount x : Real) := by positivity linarith calc |F (upd x) - F x| ≤ |F (upd x)| + |F x| := abs_sub _ _ _ ≤ C * (1 + (nestedPairedTotalCount (upd x) : Real)) ^ degree + C * (1 + (nestedPairedTotalCount x : Real)) ^ degree := add_le_add (hbound (upd x)) (hbound x) _ ≤ C * (2 * (1 + (nestedPairedTotalCount x : Real))) ^ degree + C * (2 * (1 + (nestedPairedTotalCount x : Real))) ^ degree := by gcongr _ = (2 * C * 2 ^ degree) * (1 + (nestedPairedTotalCount x : Real)) ^ degree := by simp [mul_pow] ring

theorem poisson_addOne_poincare_finiteSupport (lambda : NNReal) (f : Nat → Real) (hf : (support f).Finite) : variance f (poissonMeasure lambda) ≤ (lambda : Real) * ∫ n, (addOne f n) ^ 2 ∂(poissonMeasure lambda) := by -- Use the pairwise product-law identity, split the double sum into the two strict -- triangles, telescope each `f m - f n`, and reindex the resulting nonnegative sums. -- The Poisson shift identity collapses the coefficient of each squared increment to -- at most `lambda * p_k`. Keep the zero-rate case inside the same mass calculation. have hflp : MemLp f 2 (poissonMeasure lambda) := memLp_poissonMeasure_of_finiteSupport lambda f hf have hfi : Integrable f (poissonMeasure lambda) := hflp.integrable one_le_two have hfsq : Integrable (fun n ↦ f n ^ 2) (poissonMeasure lambda) := hflp.integrable_sq have hfst : Integrable (fun z : Nat × Nat ↦ f z.1 ^ 2) ((poissonMeasure lambda).prod (poissonMeasure lambda)) := hfsq.comp_fst (poissonMeasure lambda) have hsnd : Integrable (fun z : Nat × Nat ↦ f z.2 ^ 2) ((poissonMeasure lambda).prod (poissonMeasure lambda)) := hfsq.comp_snd (poissonMeasure lambda) have hcross : Integrable (fun z : Nat × Nat ↦ f z.1 * f z.2) ((poissonMeasure lambda).prod (poissonMeasure lambda)) := hfi.mul_prod hfi have hpair : Integrable (fun z : Nat × Nat ↦ (f z.1 - f z.2) ^ 2) ((poissonMeasure lambda).prod (poissonMeasure lambda)) := by have h := (hfst.sub (hcross.const_mul 2)).add hsnd refine h.congr ?_ filter_upwards with z change f z.1 ^ 2 - 2 * (f z.1 * f z.2) + f z.2 ^ 2 = (f z.1 - f z.2) ^ 2 ring rw [variance_eq_half_integral_prod_sq_sub (poissonMeasure lambda) f hflp] rw [integral_prod _ hpair] have hinner (n : Nat) : (∫ m, (f n - f m) ^ 2 ∂(poissonMeasure lambda)) = ∑' m : Nat, poissonWeight lambda m * (f n - f m) ^ 2 := by rw [integral_poissonMeasure] simp only [poissonWeight, smul_eq_mul] have hp : Summable (poissonWeight lambda) := (poissonWeight_hasSum_one lambda).summable have hpsq : Summable (fun m : Nat ↦ poissonWeight lambda m * f m ^ 2) := by have h := integrable_poissonMeasure_iff.mp hfsq refine h.congr ?_ intro n rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg (f n))] rfl have hinnerSummable (n : Nat) : Summable (fun m : Nat ↦ poissonWeight lambda m * (f n - f m) ^ 2) := by have hmajor : Summable (fun m : Nat ↦ 2 * (poissonWeight lambda m * f n ^ 2 + poissonWeight lambda m * f m ^ 2)) := ((hp.mul_right (f n ^ 2)).add hpsq).mul_left 2 refine hmajor.of_nonneg_of_le (fun m ↦ ?_) (fun m ↦ ?_) · exact mul_nonneg (poissonWeight_nonneg lambda m) (sq_nonneg _) · have hs : (f n - f m) ^ 2 ≤ 2 * (f n ^ 2 + f m ^ 2) := by nlinarith [sq_nonneg (f n + f m)] have hm := mul_le_mul_of_nonneg_left hs (poissonWeight_nonneg lambda m) nlinarith rw [integral_poissonMeasure] simp only [poissonWeight, smul_eq_mul] have hdouble : (∑' n : Nat, (exp (-(lambda : Real)) * (lambda : Real) ^ n / factorial n) * ∫ m, (f n - f m) ^ 2 ∂(poissonMeasure lambda)) = ∑' n : Nat, ∑' m : Nat, poissonWeight lambda n * poissonWeight lambda m * (f n - f m) ^ 2 := by apply tsum_congr intro n rw [hinner] change poissonWeight lambda n * (∑' m : Nat, poissonWeight lambda m * (f n - f m) ^ 2) = _ rw [← (hinnerSummable n).tsum_mul_left] apply tsum_congr intro m ring rw [hdouble] have hpairBound := poisson_pairwise_tsum_le lambda f hf have henergy : (∫ n, (addOne f n) ^ 2 ∂(poissonMeasure lambda)) = ∑' n : Nat, poissonWeight lambda n * (addOne f n) ^ 2 := by rw [integral_poissonMeasure] simp only [poissonWeight, smul_eq_mul] rw [henergy] nlinarith

theorem poisson_addOne_poincare_tsum (lambda : NNReal) (f : Nat → Real) (hf : MemLp f 2 (poissonMeasure lambda)) (hdf : MemLp (addOne f) 2 (poissonMeasure lambda)) : variance f (poissonMeasure lambda) ≤ (lambda : Real) * ∑' n : Nat, poissonWeight lambda n * (addOne f n) ^ 2 := by -- Rewrite the integrable squared increment with `integral_poissonMeasure` and simplify -- real scalar multiplication. have h := poisson_addOne_poincare lambda f hf hdf rw [integral_poissonMeasure] at h simpa only [poissonWeight, smul_eq_mul] using h

theorem variance_poissonMeasure_zero (f : Nat → Real) (hf : MemLp f 2 (poissonMeasure 0)) : variance f (poissonMeasure 0) = 0 := by -- The singleton-mass formula identifies `poissonMeasure 0` with `Measure.dirac 0`; -- alternatively specialize the main inequality and combine with variance nonnegativity. rw [variance_eq_sub hf] rw [integral_poissonMeasure, integral_poissonMeasure] simp only [NNReal.coe_zero, neg_zero, Real.exp_zero, one_mul, smul_eq_mul] have hs (g : Nat → Real) : (∑' n : Nat, (0 : Real) ^ n / factorial n * g n) = g 0 := by rw [tsum_eq_single 0] · simp · intro n hn rw [zero_pow hn] simp rw [hs, hs] simp