Stat.UStatistic.Localized­Variance

theorem pairValue_memLp_two {n : ℕ} (p : Fin n × Fin n) : MemLp (pairValue H p) 2 (iidLaw P n) := by have : IsProbabilityMeasure (iidLaw P n) := by unfold iidLaw; infer_instance have hm : Measurable (pairValue H p) := by change Measurable (fun ω : Fin n → X => H (ω p.1) (ω p.2)) have hpair : Measurable (fun ω : Fin n → X => (ω p.1, ω p.2)) := by fun_prop exact h.measurable_kernel.comp hpair apply MemLp.of_bound hm.aestronglyMeasurable M filter_upwards [] with ω rw [Real.norm_eq_abs] exact (h.envelope (ω p.1) (ω p.2)).trans (mul_le_of_le_one_right h.envelope_nonneg (h.weight_le_one _ _))

theorem kernel_mean_sq_le_rowMassSq : (∫ x, ∫ y, H x y ∂P ∂P) ^ 2 ≤ M ^ 2 * rowMassSq P W := by have hH (x : X) : Integrable (H x) P := Integrable.of_bound (h.measurable_kernel.comp (measurable_const.prodMk measurable_id)).aestronglyMeasurable M (Filter.Eventually.of_forall (fun y => by rw [Real.norm_eq_abs] exact (h.envelope x y).trans (mul_le_of_le_one_right h.envelope_nonneg (h.weight_le_one x y)))) have hW (x : X) : Integrable (W x) P := Integrable.of_bound (h.measurable_weight.comp (measurable_const.prodMk measurable_id)).aestronglyMeasurable 1 (Filter.Eventually.of_forall (fun y => by rw [Real.norm_eq_abs, abs_of_nonneg (h.weight_nonneg x y)] exact h.weight_le_one x y)) have hrow (x : X) : |∫ y, H x y ∂P| ≤ M * ∫ y, W x y ∂P := by calc _ ≤ ∫ y, |H x y| ∂P := abs_integral_le_integral_abs _ ≤ ∫ y, M * W x y ∂P := integral_mono (hH x).abs ((hW x).const_mul M) (h.envelope x) _ = _ := by rw [integral_const_mul] have hHprod : Integrable (fun z : X × X => H z.1 z.2) (P.prod P) := Integrable.of_bound h.measurable_kernel.aestronglyMeasurable M (Filter.Eventually.of_forall (fun z => by rw [Real.norm_eq_abs] exact (h.envelope z.1 z.2).trans (mul_le_of_le_one_right h.envelope_nonneg (h.weight_le_one _ _)))) have hWprod : Integrable (fun z : X × X => W z.1 z.2) (P.prod P) := Integrable.of_bound h.measurable_weight.aestronglyMeasurable 1 (Filter.Eventually.of_forall (fun z => by rw [Real.norm_eq_abs, abs_of_nonneg (h.weight_nonneg _ _)] exact h.weight_le_one _ _)) have hHout : Integrable (fun x => ∫ y, H x y ∂P) P := hHprod.integral_prod_left have hWout : Integrable (fun x => ∫ y, W x y ∂P) P := hWprod.integral_prod_left have hWmeas : Measurable (fun x => ∫ y, W x y ∂P) := (h.measurable_weight.stronglyMeasurable.integral_prod_right' (ν := P)).measurable have hWbound (x : X) : |∫ y, W x y ∂P| ≤ 1 := by calc _ ≤ ∫ y, |W x y| ∂P := abs_integral_le_integral_abs _ = ∫ y, W x y ∂P := by congr 1; funext y; rw [abs_of_nonneg (h.weight_nonneg x y)] _ ≤ 1 := by simpa using integral_mono (hW x) (integrable_const (1 : ℝ)) (h.weight_le_one x) have hWsq : Integrable (fun x => (∫ y, W x y ∂P) ^ 2) P := Integrable.of_bound (hWmeas.pow_const 2).aestronglyMeasurable 1 (Filter.Eventually.of_forall (fun x => by rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith [mul_nonneg (sub_nonneg.mpr (hWbound x)) (add_nonneg (abs_nonneg (∫ y, W x y ∂P)) (by norm_num : (0 : ℝ) ≤ 1)), sq_abs (∫ y, W x y ∂P)])) have hglobal : |∫ x, ∫ y, H x y ∂P ∂P| ≤ M * ∫ x, ∫ y, W x y ∂P ∂P := by calc _ ≤ ∫ x, |∫ y, H x y ∂P| ∂P := abs_integral_le_integral_abs _ ≤ ∫ x, M * ∫ y, W x y ∂P ∂P := integral_mono hHout.abs (hWout.const_mul M) hrow _ = _ := by rw [integral_const_mul] have hjs : (∫ x, ∫ y, W x y ∂P ∂P) ^ 2 ≤ rowMassSq P W := by have hvar := variance_nonneg (fun x => ∫ y, W x y ∂P) P rw [variance_eq_sub ((memLp_two_iff_integrable_sq hWmeas.aestronglyMeasurable).2 hWsq)] at hvar simp only [Pi.pow_apply] at hvar unfold rowMassSq linarith have hsq : (∫ x, ∫ y, H x y ∂P ∂P) ^ 2 ≤ M ^ 2 * (∫ x, ∫ y, W x y ∂P ∂P) ^ 2 := by have hw : 0 ≤ ∫ x, ∫ y, W x y ∂P ∂P := integral_nonneg (fun x => integral_nonneg (h.weight_nonneg x)) have ha := (sq_le_sq₀ (abs_nonneg (∫ x, ∫ y, H x y ∂P ∂P)) (mul_nonneg h.envelope_nonneg hw)).2 hglobal nlinarith [ha, sq_abs (∫ x, ∫ y, H x y ∂P ∂P)] nlinarith [mul_le_mul_of_nonneg_left hjs (sq_nonneg M)]

theorem pairValue_second_moment_le_pairMass {n : ℕ} {p : Fin n × Fin n} (hp : p ∈ pairIndices n) : (∫ ω, (pairValue H p ω) ^ 2 ∂iidLaw P n) ≤ M ^ 2 * pairMass P W := by have hij : p.1 ≠ p.2 := ne_of_lt (Finset.mem_filter.mp hp).2 have hsq (x y : X) : H x y ^ 2 ≤ M ^ 2 * W x y := by have hw0 := h.weight_nonneg x y have hw1 := h.weight_le_one x y have he := h.envelope x y have hm := h.envelope_nonneg have ha : H x y ^ 2 ≤ (M * W x y) ^ 2 := by nlinarith [mul_nonneg (sub_nonneg.mpr he) (add_nonneg (abs_nonneg (H x y)) (mul_nonneg hm hw0)), sq_abs (H x y)] have hb : (W x y) ^ 2 ≤ W x y := by nlinarith [mul_nonneg hw0 (sub_nonneg.mpr hw1)] nlinarith [mul_le_mul_of_nonneg_left hb (sq_nonneg M)] have hmeas : Measurable (fun z : X × X => H z.1 z.2 ^ 2) := h.measurable_kernel.pow_const 2 have hbound (x y : X) : |H x y ^ 2| ≤ M ^ 2 := by rw [abs_of_nonneg (sq_nonneg _)] have := hsq x y exact this.trans (mul_le_of_le_one_right (sq_nonneg M) (h.weight_le_one x y)) have hH (x : X) : Integrable (fun y => H x y ^ 2) P := Integrable.of_bound (hmeas.comp (measurable_const.prodMk measurable_id)).aestronglyMeasurable (M ^ 2) (Filter.Eventually.of_forall (fun y => by simpa only [Real.norm_eq_abs] using hbound x y)) have hW (x : X) : Integrable (fun y => M ^ 2 * W x y) P := by have hwm : Measurable (fun y => M ^ 2 * W x y) := (h.measurable_weight.comp (measurable_const.prodMk measurable_id)).const_mul _ exact Integrable.of_bound hwm.aestronglyMeasurable (M ^ 2) (Filter.Eventually.of_forall (fun y => by rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (sq_nonneg _) (h.weight_nonneg _ _))] exact mul_le_of_le_one_right (sq_nonneg _) (h.weight_le_one _ _))) have hinner (x : X) : (∫ y, H x y ^ 2 ∂P) ≤ M ^ 2 * ∫ y, W x y ∂P := by calc _ ≤ ∫ y, M ^ 2 * W x y ∂P := integral_mono (hH x) (hW x) (hsq x) _ = _ := by rw [integral_const_mul] have houtH : Integrable (fun x => ∫ y, H x y ^ 2 ∂P) P := by have hp : Integrable (fun z : X × X => H z.1 z.2 ^ 2) (P.prod P) := Integrable.of_bound hmeas.aestronglyMeasurable (M ^ 2) (Filter.Eventually.of_forall (fun z => by simpa only [Real.norm_eq_abs] using hbound z.1 z.2)) exact hp.integral_prod_left have houtW : Integrable (fun x => M ^ 2 * ∫ y, W x y ∂P) P := by have hw : Integrable (fun z : X × X => W z.1 z.2) (P.prod P) := Integrable.of_bound h.measurable_weight.aestronglyMeasurable 1 (Filter.Eventually.of_forall (fun z => by rw [Real.norm_eq_abs, abs_of_nonneg (h.weight_nonneg _ _)] exact h.weight_le_one _ _)) exact hw.integral_prod_left.const_mul _ calc _ = ∫ x, ∫ y, H x y ^ 2 ∂P ∂P := by change (∫ ω, H (ω p.1) (ω p.2) ^ 2 ∂iidLaw P n) = _ exact integral_two_coordinates P hij (fun x y => H x y ^ 2) hmeas (M ^ 2) hbound _ ≤ ∫ x, M ^ 2 * ∫ y, W x y ∂P ∂P := integral_mono houtH houtW hinner _ = M ^ 2 * pairMass P W := by rw [integral_const_mul]; rfl

theorem pairValue_integral_eq_kernel_mean {n : ℕ} {p : Fin n × Fin n} (hp : p ∈ pairIndices n) : (∫ ω, pairValue H p ω ∂iidLaw P n) = ∫ x, ∫ y, H x y ∂P ∂P := by have hij : p.1 ≠ p.2 := ne_of_lt (Finset.mem_filter.mp hp).2 have hbound (x y : X) : |H x y| ≤ M := (h.envelope x y).trans (mul_le_of_le_one_right h.envelope_nonneg (h.weight_le_one x y)) change (∫ ω, H (ω p.1) (ω p.2) ∂iidLaw P n) = _ exact integral_two_coordinates P hij H h.measurable_kernel M hbound

theorem covariance_disjoint_pairs_eq_zero {n : ℕ} {p q : Fin n × Fin n} (hpq : ¬ SharesIndex p q) : covariance (pairValue H p) (pairValue H q) (iidLaw P n) = 0 := by -- The two coordinate pairs are independent by `iIndepFun_pi` and the four -- cross-inequalities from `¬ SharesIndex`; apply `IndepFun.covariance_eq_zero`. haveI : IsProbabilityMeasure (iidLaw P n) := by unfold iidLaw; infer_instance have hcross : p.1 ≠ q.1 ∧ p.1 ≠ q.2 ∧ p.2 ≠ q.1 ∧ p.2 ≠ q.2 := by simp only [SharesIndex, not_or] at hpq exact hpq have hcoord : iIndepFun (fun i : Fin n => fun ω : Fin n → X => ω i) (iidLaw P n) := by unfold iidLaw simpa using (iIndepFun_pi (μ := fun _ : Fin n => P) (X := fun _ : Fin n => id) (fun _ => aemeasurable_id)) have hind : pairValue H p ⟂ᵢ[iidLaw P n] pairValue H q := by have hpairs := hcoord.indepFun_prodMk_prodMk (fun i => measurable_pi_apply i) p.1 p.2 q.1 q.2 hcross.1 hcross.2.1 hcross.2.2.1 hcross.2.2.2 have hc := hpairs.comp h.measurable_kernel h.measurable_kernel change (fun ω => H (ω p.1) (ω p.2)) ⟂ᵢ[iidLaw P n] (fun ω => H (ω q.1) (ω q.2)) simpa only [Function.comp_def, Function.uncurry_apply_pair] using hc exact hind.covariance_eq_zero (pairValue_memLp_two P h p) (pairValue_memLp_two P h q)

theorem shared_triple_integral_abs_le_rowMassSq : |∫ x, ∫ y, ∫ z, H x y * H x z ∂P ∂P ∂P| ≤ M ^ 2 * rowMassSq P W := by have hH (x : X) : Integrable (H x) P := Integrable.of_bound (h.measurable_kernel.comp (measurable_const.prodMk measurable_id)).aestronglyMeasurable M (Filter.Eventually.of_forall (fun y => by rw [Real.norm_eq_abs] exact (h.envelope x y).trans (mul_le_of_le_one_right h.envelope_nonneg (h.weight_le_one x y)))) have hW (x : X) : Integrable (W x) P := Integrable.of_bound (h.measurable_weight.comp (measurable_const.prodMk measurable_id)).aestronglyMeasurable 1 (Filter.Eventually.of_forall (fun y => by rw [Real.norm_eq_abs, abs_of_nonneg (h.weight_nonneg x y)] exact h.weight_le_one x y)) have hrow (x : X) : |∫ y, H x y ∂P| ≤ M * ∫ y, W x y ∂P := by calc _ ≤ ∫ y, |H x y| ∂P := abs_integral_le_integral_abs _ ≤ ∫ y, M * W x y ∂P := integral_mono (hH x).abs ((hW x).const_mul M) (h.envelope x) _ = _ := by rw [integral_const_mul] have hWrow_nonneg (x : X) : 0 ≤ ∫ y, W x y ∂P := integral_nonneg (h.weight_nonneg x) have hWrow_le_one (x : X) : ∫ y, W x y ∂P ≤ 1 := by simpa using integral_mono (hW x) (integrable_const (1 : ℝ)) (h.weight_le_one x) have hWmeas : Measurable (fun x => ∫ y, W x y ∂P) := (h.measurable_weight.stronglyMeasurable.integral_prod_right' (ν := P)).measurable have hHmeas : Measurable (fun x => ∫ y, H x y ∂P) := (h.measurable_kernel.stronglyMeasurable.integral_prod_right' (ν := P)).measurable have hWsq : Integrable (fun x => (∫ y, W x y ∂P) ^ 2) P := Integrable.of_bound (hWmeas.pow_const 2).aestronglyMeasurable 1 (Filter.Eventually.of_forall (fun x => by rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith [hWrow_nonneg x, hWrow_le_one x])) have hHsq : Integrable (fun x => (∫ y, H x y ∂P) ^ 2) P := Integrable.of_bound (hHmeas.pow_const 2).aestronglyMeasurable (M ^ 2) (Filter.Eventually.of_forall (fun x => by rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] have hx : |∫ y, H x y ∂P| ≤ M := (hrow x).trans (mul_le_of_le_one_right h.envelope_nonneg (hWrow_le_one x)) nlinarith [(sq_le_sq₀ (abs_nonneg (∫ y, H x y ∂P)) h.envelope_nonneg).2 hx, sq_abs (∫ y, H x y ∂P)])) have hsq (x : X) : (∫ y, H x y ∂P) ^ 2 ≤ M ^ 2 * (∫ y, W x y ∂P) ^ 2 := by have hx := hrow x have hy := hWrow_nonneg x nlinarith [(sq_le_sq₀ (abs_nonneg (∫ y, H x y ∂P)) (mul_nonneg h.envelope_nonneg hy)).2 hx, sq_abs (∫ y, H x y ∂P)] have hid (x : X) : (∫ y, ∫ z, H x y * H x z ∂P ∂P) = (∫ y, H x y ∂P) ^ 2 := by simp_rw [integral_const_mul, integral_mul_const] ring calc _ = |∫ x, (∫ y, H x y ∂P) ^ 2 ∂P| := by simp_rw [hid] _ = ∫ x, (∫ y, H x y ∂P) ^ 2 ∂P := by rw [abs_of_nonneg (integral_nonneg (fun x => sq_nonneg _))] _ ≤ ∫ x, M ^ 2 * (∫ y, W x y ∂P) ^ 2 ∂P := integral_mono hHsq (hWsq.const_mul _) hsq _ = M ^ 2 * rowMassSq P W := by rw [integral_const_mul]; rfl

theorem shared_first_coordinate_product_integral_abs_le_rowMassSq {n : ℕ} {i j k : Fin n} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : |∫ ω, H (ω i) (ω j) * H (ω i) (ω k) ∂iidLaw P n| ≤ M ^ 2 * rowMassSq P W := by have hmeas : Measurable (fun t : (X × X) × X => H t.1.1 t.1.2 * H t.1.1 t.2) := by have hleft : Measurable (fun t : (X × X) × X => (t.1.1, t.1.2)) := by fun_prop have hright : Measurable (fun t : (X × X) × X => (t.1.1, t.2)) := by fun_prop exact (h.measurable_kernel.comp hleft).mul (h.measurable_kernel.comp hright) have hbound (x y z : X) : |H x y * H x z| ≤ M ^ 2 := by have hxy : |H x y| ≤ M := (h.envelope x y).trans (mul_le_of_le_one_right h.envelope_nonneg (h.weight_le_one x y)) have hxz : |H x z| ≤ M := (h.envelope x z).trans (mul_le_of_le_one_right h.envelope_nonneg (h.weight_le_one x z)) calc |H x y * H x z| = |H x y| * |H x z| := abs_mul _ _ _ ≤ M * M := mul_le_mul hxy hxz (abs_nonneg _) h.envelope_nonneg _ = M ^ 2 := by ring rw [integral_three_coordinates P hij hik hjk (fun x y z => H x y * H x z) hmeas (M ^ 2) hbound] exact shared_triple_integral_abs_le_rowMassSq P h

theorem shared_pairs_product_integral_abs_le_rowMassSq {n : ℕ} {p q : Fin n × Fin n} (hp : p ∈ pairIndices n) (hq : q ∈ pairIndices n) (hne : p ≠ q) (hpq : SharesIndex p q) : |∫ ω, pairValue H p ω * pairValue H q ω ∂iidLaw P n| ≤ M ^ 2 * rowMassSq P W := by have hpord : p.1 < p.2 := (Finset.mem_filter.mp hp).2 have hqord : q.1 < q.2 := (Finset.mem_filter.mp hq).2 rcases hpq with h11 | h12 | h21 | h22 · have hjk : p.2 ≠ q.2 := by intro e exact hne (Prod.ext h11 e) have hb := shared_first_coordinate_product_integral_abs_le_rowMassSq P h (ne_of_lt hpord) (by omega : p.1 ≠ q.2) hjk convert hb using 1 congr 1 apply integral_congr_ae filter_upwards [] with ω simp only [pairValue, h11] · have hjk : p.2 ≠ q.1 := by omega have hb := shared_first_coordinate_product_integral_abs_le_rowMassSq P h (ne_of_lt hpord) (by omega : p.1 ≠ q.1) hjk convert hb using 1 congr 1 apply integral_congr_ae filter_upwards [] with ω simp only [pairValue] rw [h.symmetric_kernel (ω q.1) (ω q.2), ← h12] · have hjk : p.1 ≠ q.2 := by omega have hb := shared_first_coordinate_product_integral_abs_le_rowMassSq P h (by omega : p.2 ≠ p.1) (by omega : p.2 ≠ q.2) hjk convert hb using 1 congr 1 apply integral_congr_ae filter_upwards [] with ω simp only [pairValue] rw [h.symmetric_kernel (ω p.1) (ω p.2), h21] · have hjk : p.1 ≠ q.1 := by intro e exact hne (Prod.ext e h22) have hb := shared_first_coordinate_product_integral_abs_le_rowMassSq P h (by omega : p.2 ≠ p.1) (by omega : p.2 ≠ q.1) hjk convert hb using 1 congr 1 apply integral_congr_ae filter_upwards [] with ω simp only [pairValue] rw [h.symmetric_kernel (ω p.1) (ω p.2), h.symmetric_kernel (ω q.1) (ω q.2), h22]

theorem covariance_identical_pair_le_pairMass {n : ℕ} {p : Fin n × Fin n} (hp : p ∈ pairIndices n) : covariance (pairValue H p) (pairValue H p) (iidLaw P n) ≤ M ^ 2 * pairMass P W := by -- Use `variance_le_expectation_sq` or `covariance_self`, then the localized -- second-moment estimate above. haveI : IsProbabilityMeasure (iidLaw P n) := by unfold iidLaw; infer_instance have hm := pairValue_memLp_two P h p calc covariance (pairValue H p) (pairValue H p) (iidLaw P n) = variance (pairValue H p) (iidLaw P n) := covariance_self hm.aemeasurable _ ≤ ∫ ω, (pairValue H p ω) ^ 2 ∂iidLaw P n := variance_le_expectation_sq hm.aestronglyMeasurable _ ≤ M ^ 2 * pairMass P W := pairValue_second_moment_le_pairMass P h hp

theorem integral_two_coordinates {n : ℕ} {i j : Fin n} (hij : i ≠ j) (f : X → X → ℝ) (hf : Measurable fun z : X × X => f z.1 z.2) (B : ℝ) (hB : ∀ x y, |f x y| ≤ B) : ∫ ω, f (ω i) (ω j) ∂iidLaw P n = ∫ x, ∫ y, f x y ∂P ∂P := by -- Use independence of the two coordinate projections under `Measure.pi` to identify -- their joint law with `P.prod P`; bounded measurability supplies integrability. have hcoord : iIndepFun (fun a : Fin n => fun ω : Fin n → X => ω a) (iidLaw P n) := by unfold iidLaw simpa using (iIndepFun_pi (μ := fun _ : Fin n => P) (X := fun _ : Fin n => id) (fun _ => aemeasurable_id)) have hpair : (iidLaw P n).map (fun ω => (ω i, ω j)) = P.prod P := by letI : IsProbabilityMeasure (iidLaw P n) := by unfold iidLaw; infer_instance have hind := hcoord.indepFun hij simpa only [(measurePreserving_eval (fun _ : Fin n => P) i).map_eq, (measurePreserving_eval (fun _ : Fin n => P) j).map_eq, iidLaw] using (hind.map_prod_eq_prod_map_map (measurable_pi_apply i).aemeasurable (measurable_pi_apply j).aemeasurable) have hfi : Integrable (fun z : X × X => f z.1 z.2) (P.prod P) := Integrable.of_bound hf.aestronglyMeasurable B (Filter.Eventually.of_forall (by intro z simpa only [Real.norm_eq_abs] using hB z.1 z.2)) calc _ = ∫ z : X × X, f z.1 z.2 ∂(iidLaw P n).map (fun ω => (ω i, ω j)) := by rw [integral_map (by fun_prop) hf.aestronglyMeasurable] _ = ∫ z : X × X, f z.1 z.2 ∂(P.prod P) := by rw [hpair] _ = _ := integral_prod _ hfi

theorem integral_three_coordinates {n : ℕ} {i j k : Fin n} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (f : X → X → X → ℝ) (hf : Measurable fun z : (X × X) × X => f z.1.1 z.1.2 z.2) (B : ℝ) (hB : ∀ x y z, |f x y z| ≤ B) : ∫ ω, f (ω i) (ω j) (ω k) ∂iidLaw P n = ∫ x, ∫ y, ∫ z, f x y z ∂P ∂P ∂P := by -- Push the product law along the three distinct coordinate projections, then -- apply Fubini twice. A reusable finite-coordinate map theorem may shorten this. letI : IsProbabilityMeasure (iidLaw P n) := by unfold iidLaw; infer_instance have hcoord : iIndepFun (fun a : Fin n => fun ω : Fin n → X => ω a) (iidLaw P n) := by unfold iidLaw simpa using (iIndepFun_pi (μ := fun _ : Fin n => P) (X := fun _ : Fin n => id) (fun _ => aemeasurable_id)) have hpair : (iidLaw P n).map (fun ω => (ω i, ω j)) = P.prod P := by have hind := hcoord.indepFun hij simpa only [(measurePreserving_eval (fun _ : Fin n => P) i).map_eq, (measurePreserving_eval (fun _ : Fin n => P) j).map_eq, iidLaw] using (hind.map_prod_eq_prod_map_map (measurable_pi_apply i).aemeasurable (measurable_pi_apply j).aemeasurable) have htriple : (iidLaw P n).map (fun ω => ((ω i, ω j), ω k)) = (P.prod P).prod P := by have hind := hcoord.indepFun_prodMk (fun a => measurable_pi_apply a) i j k hik hjk have h := hind.map_prod_eq_prod_map_map ((measurable_pi_apply i).prodMk (measurable_pi_apply j)).aemeasurable (measurable_pi_apply k).aemeasurable rw [hpair] at h simpa only [(measurePreserving_eval (fun _ : Fin n => P) k).map_eq, iidLaw] using h have hfi : Integrable (fun z : (X × X) × X => f z.1.1 z.1.2 z.2) ((P.prod P).prod P) := Integrable.of_bound hf.aestronglyMeasurable B (Filter.Eventually.of_forall (by intro z simpa only [Real.norm_eq_abs] using hB z.1.1 z.1.2 z.2)) calc _ = ∫ z : (X × X) × X, f z.1.1 z.1.2 z.2 ∂ (iidLaw P n).map (fun ω => ((ω i, ω j), ω k)) := by rw [integral_map (by fun_prop) hf.aestronglyMeasurable] _ = ∫ z : (X × X) × X, f z.1.1 z.1.2 z.2 ∂((P.prod P).prod P) := by rw [htriple] _ = ∫ z : X × X, ∫ w : X, f z.1 z.2 w ∂P ∂(P.prod P) := integral_prod _ hfi _ = _ := by exact integral_prod _ hfi.integral_prod_left

theorem card_identical_pair_configurations (n : ℕ) : ((pairIndices n).product (pairIndices n) |>.filter fun pq => pq.1 = pq.2).card = n.choose 2 := by change ((pairIndices n ×ˢ pairIndices n).filter (fun pq => pq.1 = pq.2)).card = _ rw [← Finset.diag_eq_filter, Finset.diag_card, card_pairIndices]

theorem card_pairs_sharing_fixed_pair {n : ℕ} (hn : 2 ≤ n) {p : Fin n × Fin n} (hp : p ∈ pairIndices n) : ((pairIndices n).filter fun q => p ≠ q ∧ SharesIndex p q).card = 2 * (n - 2) := by -- Partition the filtered pairs by which endpoint of p they contain. The -- parts are disjoint because q ≠ p; each is indexed by the n - 2 remaining -- vertices. An order-free Finset erase of the two endpoints is convenient. have hcount (a b : Fin n) (hab : a ≠ b) : ((pairIndices n).filter (fun q => q ≠ (if a < b then (a,b) else (b,a)) ∧ (q.1 = a ∨ q.2 = a))).card = n - 2 := by let t := ((Finset.univ : Finset (Fin n)).erase a).erase b let f : Fin n → Fin n × Fin n := fun x => if a < x then (a,x) else (x,a) have heq : (pairIndices n).filter (fun q => q ≠ (if a < b then (a,b) else (b,a)) ∧ (q.1 = a ∨ q.2 = a)) = t.image f := by ext q simp only [mem_filter, pairIndices, Finset.mem_univ, true_and, mem_image] constructor · rintro ⟨hord, hne, hshare⟩ rcases hshare with h | h · refine ⟨q.2, ?_, ?_⟩ · grind · dsimp [f]; split_ifs <;> grind · refine ⟨q.1, ?_, ?_⟩ · grind · dsimp [f]; split_ifs <;> grind · rintro ⟨x, hx, hqx⟩ rw [← hqx] have hxa : x ≠ a := (Finset.mem_erase.mp (Finset.mem_erase.mp hx).2).1 have hxb : x ≠ b := (Finset.mem_erase.mp hx).1 dsimp [f] split_ifs <;> grind have hinj : InjOn f ↑t := by intro x hx y hy h have hxa : x ≠ a := (Finset.mem_erase.mp (Finset.mem_erase.mp hx).2).1 have hya : y ≠ a := (Finset.mem_erase.mp (Finset.mem_erase.mp hy).2).1 dsimp [f] at h split_ifs at h <;> grind rw [heq, Finset.card_image_of_injOn hinj] have hb : b ∈ (Finset.univ : Finset (Fin n)).erase a := by simp [hab.symm] rw [Finset.card_erase_of_mem hb, Finset.card_erase_of_mem (Finset.mem_univ a)] simp only [Finset.card_univ, Fintype.card_fin] omega have hpord : p.1 < p.2 := by simpa [pairIndices] using hp let A := (pairIndices n).filter fun q => q ≠ p ∧ (q.1 = p.1 ∨ q.2 = p.1) let B := (pairIndices n).filter fun q => q ≠ p ∧ (q.1 = p.2 ∨ q.2 = p.2) have hcover : ((pairIndices n).filter fun q => p ≠ q ∧ SharesIndex p q) = A ∪ B := by ext q simp only [mem_filter, mem_union] dsimp [A, B] simp only [mem_filter] unfold SharesIndex grind have hdisj : Disjoint A B := by apply Finset.disjoint_left.mpr intro q hA hB have hqord : q.1 < q.2 := by have hq : q ∈ pairIndices n := (Finset.mem_filter.mp hA).1 simpa [pairIndices] using hq have ha := (Finset.mem_filter.mp hA).2 have hb := (Finset.mem_filter.mp hB).2 grind have hA : A.card = n - 2 := by simpa [A, hpord] using hcount p.1 p.2 (ne_of_lt hpord) have hB : B.card = n - 2 := by have hnot : ¬ p.2 < p.1 := not_lt_of_ge (le_of_lt hpord) simpa [B, hnot] using hcount p.2 p.1 (Ne.symm (ne_of_lt hpord)) rw [hcover, Finset.card_union_of_disjoint hdisj, hA, hB] omega

theorem card_pairs_disjoint_fixed_pair {n : ℕ} {p : Fin n × Fin n} (hp : p ∈ pairIndices n) : ((pairIndices n).filter fun q => ¬ SharesIndex p q).card = (n - 2).choose 2 := by let s := ((Finset.univ : Finset (Fin n)).erase p.1).erase p.2 have hset : (pairIndices n).filter (fun q => ¬ SharesIndex p q) = (s ×ˢ s).filter (fun q => q.1 < q.2) := by ext q simp [s, pairIndices, SharesIndex, Finset.mem_product, and_comm, and_assoc] grind have hpord : p.1 < p.2 := by simpa [pairIndices] using hp have hp2 : p.2 ∈ (Finset.univ : Finset (Fin n)).erase p.1 := by simp [ne_of_gt hpord] have hs : s.card = n - 2 := by dsimp [s] rw [Finset.card_erase_of_mem hp2, Finset.card_erase_of_mem (Finset.mem_univ p.1)] simp only [Finset.card_univ, Fintype.card_fin] omega rw [hset, Finset.card_product_filter_lt, hs]

theorem choose_two_mul_choose_sub_two (n : ℕ) : n.choose 2 * (n - 2).choose 2 = 6 * n.choose 4 := by have h := Nat.choose_mul (n := n) (k := 4) (s := 2) (by omega) have hchoose : choose 4 2 = 6 := by decide rw [hchoose] at h simpa [Nat.mul_comm] using h.symm

theorem card_shared_pair_configurations {n : ℕ} (hn : 2 ≤ n) : ((pairIndices n).product (pairIndices n) |>.filter fun (pq : (Fin n × Fin n) × (Fin n × Fin n)) => pq.1 ≠ pq.2 ∧ SharesIndex pq.1 pq.2).card = 2 * (n.choose 2) * (n - 2) := by -- Sum the fixed-pair fiber count `card_pairs_sharing_fixed_pair` over -- `pairIndices`; then use `card_pairIndices`. classical let s := pairIndices n have hfiber (p : Fin n × Fin n) (hp : p ∈ s) : (((s ×ˢ s).filter (fun pq => pq.1 ≠ pq.2 ∧ SharesIndex pq.1 pq.2)).filter (fun pq => pq.1 = p)).card = 2 * (n - 2) := by have heq : ((s ×ˢ s).filter (fun pq => pq.1 ≠ pq.2 ∧ SharesIndex pq.1 pq.2)).filter (fun pq => pq.1 = p) = {p} ×ˢ (s.filter fun q => p ≠ q ∧ SharesIndex p q) := by ext pq simp only [mem_filter, Finset.mem_product, Finset.mem_singleton] constructor · rintro ⟨⟨⟨hpq, hqq⟩, hne, hshare⟩, hfst⟩ subst p exact ⟨rfl, hqq, hne, hshare⟩ · rintro ⟨hfst, hqq, hne, hshare⟩ subst p exact ⟨⟨⟨hp, hqq⟩, hne, hshare⟩, rfl⟩ rw [heq, Finset.card_product] simpa [s] using card_pairs_sharing_fixed_pair hn hp have hsum := Finset.card_eq_sum_card_fiberwise (s := (s ×ˢ s).filter (fun pq => pq.1 ≠ pq.2 ∧ SharesIndex pq.1 pq.2)) (t := s) (f := fst) (by intro pq hpq exact (Finset.mem_product.mp (Finset.mem_filter.mp hpq).1).1) rw [Finset.sum_const_nat hfiber] at hsum simpa [s, card_pairIndices, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using hsum

theorem card_disjoint_pair_configurations (n : ℕ) : ((pairIndices n).product (pairIndices n) |>.filter fun (pq : (Fin n × Fin n) × (Fin n × Fin n)) => ¬ SharesIndex pq.1 pq.2).card = 6 * n.choose 4 := by -- Sum `card_pairs_disjoint_fixed_pair` over first pairs, rewrite with -- `card_pairIndices`, then use `choose_two_mul_choose_sub_two`. classical let s := pairIndices n have hfiber (p : Fin n × Fin n) (hp : p ∈ s) : (((s ×ˢ s).filter (fun pq => ¬ SharesIndex pq.1 pq.2)).filter (fun pq => pq.1 = p)).card = (n - 2).choose 2 := by have heq : ((s ×ˢ s).filter (fun pq => ¬ SharesIndex pq.1 pq.2)).filter (fun pq => pq.1 = p) = {p} ×ˢ (s.filter fun q => ¬ SharesIndex p q) := by ext pq simp only [mem_filter, Finset.mem_product, Finset.mem_singleton] constructor · rintro ⟨⟨⟨hpq, hqq⟩, hdis⟩, hfst⟩ subst p exact ⟨rfl, hqq, hdis⟩ · rintro ⟨hfst, hqq, hdis⟩ subst p exact ⟨⟨⟨hp, hqq⟩, hdis⟩, rfl⟩ rw [heq, Finset.card_product] simpa [s] using card_pairs_disjoint_fixed_pair hp have hsum := Finset.card_eq_sum_card_fiberwise (s := (s ×ˢ s).filter (fun pq => ¬ SharesIndex pq.1 pq.2)) (t := s) (f := fst) (by intro pq hpq exact (Finset.mem_product.mp (Finset.mem_filter.mp hpq).1).1) rw [Finset.sum_const_nat hfiber] at hsum have hcard : ((pairIndices n ×ˢ pairIndices n).filter (fun pq => ¬ SharesIndex pq.1 pq.2)).card = n.choose 2 * (n - 2).choose 2 := by simpa [s, card_pairIndices] using hsum exact hcard.trans (choose_two_mul_choose_sub_two n)

theorem uStatistic_memLp_two {n : ℕ} : MemLp (uStatistic n H) 2 (iidLaw P n) := by have hsum : MemLp (∑ p ∈ pairIndices n, pairValue H p) 2 (iidLaw P n) := memLp_finsetSum' (pairIndices n) (fun p _ => pairValue_memLp_two P h p) convert hsum.const_mul (((pairIndices n).card : ℝ)⁻¹) using 1 funext ω simp only [uStatistic, pairValue, Finset.sum_apply]

theorem integral_two_coordinates_integrable {n : ℕ} {i j : Fin n} (hij : i ≠ j) (H : X → X → ℝ) (hH : Measurable fun z : X × X => H z.1 z.2) : ∫ ω, H (ω i) (ω j) ∂iidLaw P n = ∫ z : X × X, H z.1 z.2 ∂(P.prod P) := by -- Follow `LocalizedVariance.integral_two_coordinates`: the joint coordinate -- map sends `iidLaw P n` to `P.prod P`. Use `integral_map`. letI : IsProbabilityMeasure (iidLaw P n) := by unfold iidLaw; infer_instance have hcoord : iIndepFun (fun a : Fin n => fun ω : Fin n → X => ω a) (iidLaw P n) := by unfold iidLaw simpa using (iIndepFun_pi (μ := fun _ : Fin n => P) (X := fun _ : Fin n => id) (fun _ => aemeasurable_id)) have hpair : (iidLaw P n).map (fun ω => (ω i, ω j)) = P.prod P := by have hind := hcoord.indepFun hij simpa only [(measurePreserving_eval (fun _ : Fin n => P) i).map_eq, (measurePreserving_eval (fun _ : Fin n => P) j).map_eq, iidLaw] using (hind.map_prod_eq_prod_map_map (measurable_pi_apply i).aemeasurable (measurable_pi_apply j).aemeasurable) calc _ = ∫ z : X × X, H z.1 z.2 ∂(iidLaw P n).map (fun ω => (ω i, ω j)) := by rw [integral_map (by fun_prop) hH.aestronglyMeasurable] _ = _ := by rw [hpair]

theorem pair_sum_variance_eq_covariance_sum {n : ℕ} : variance (fun ω => ∑ p ∈ pairIndices n, pairValue H p ω) (iidLaw P n) = ∑ p ∈ pairIndices n, ∑ q ∈ pairIndices n, covariance (pairValue H p) (pairValue H q) (iidLaw P n) := by have : IsProbabilityMeasure (iidLaw P n) := by unfold iidLaw; infer_instance exact variance_fun_sum' (fun p _ => pairValue_memLp_two P h p)