Mathlib.Probability.Poisson­Add­One­Poincare

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

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, 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 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

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₁ := MeasurableEquiv.piCurry (fun (_ : iota) (_ : Sigma fun _ : kappa ↦ Fin 2) ↦ Nat) let e₂ := MeasurableEquiv.piCongrRight (fun _ : iota ↦ MeasurableEquiv.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