Mathlib.Probability.Ident­Distrib.Eighth­Moment

theorem patternImage_card_bounds (a : Fin 8 → α) (ha : NoSingleton a) : 1 ≤ (patternImage a).card ∧ (patternImage a).card ≤ 4 := by -- Sum fiber cardinalities to 8 using `Finset.card_eq_sum_card_image`; all fibers contribute ≥2. have hsum : ∑ r ∈ patternImage a, multiplicity a r = 8 := by simpa [patternImage, multiplicity] using (Finset.card_eq_sum_card_image a univ).symm have hle : (patternImage a).card * 2 ≤ 8 := by calc (patternImage a).card * 2 = ∑ r ∈ patternImage a, 2 := by simp _ ≤ ∑ r ∈ patternImage a, multiplicity a r := Finset.sum_le_sum ha _ = 8 := hsum constructor · exact Finset.card_pos.mpr ⟨a 0, Finset.mem_image.mpr ⟨0, Finset.mem_univ _, rfl⟩⟩ · omega

theorem card_patterns_with_image_le (S T : Finset α) : ((piFinset (fun _ : Fin 8 => S)).filter (fun a => patternImage a = T)).card ≤ T.card ^ 8 := by -- Containment in `piFinset (fun _ : Fin 8 => T)` suffices; its card is T.card^8. classical calc _ ≤ (piFinset (fun _ : Fin 8 => T)).card := by apply Finset.card_le_card intro a ha apply Fintype.mem_piFinset.mpr intro j rw [← (Finset.mem_filter.mp ha).2] exact Finset.mem_image.mpr ⟨j, Finset.mem_univ _, rfl⟩ _ = T.card ^ 8 := Fintype.card_piFinset_const T 8

theorem weighted_survivingPatterns_le_choose_sum (S : Finset α) (v : ℝ) (hv : 0 ≤ v) : (∑ a ∈ survivingPatterns S, v ^ (patternImage a).card) ≤ ∑ k ∈ Icc 1 4, (S.card.choose k : ℝ) * (k : ℝ) ^ 8 * v ^ k := by -- Group by image T ∈ S.powerset, then by T.card. Use the preceding two lemmas and -- `Finset.card_powersetCard`. The nonnegative weight permits enlarging each image fiber. classical let P := S.powerset.filter (fun T => T.card ∈ Icc 1 4) have hmaps : ∀ a ∈ survivingPatterns S, patternImage a ∈ P := by intro a ha obtain ⟨hs, hn⟩ := Finset.mem_filter.mp ha apply Finset.mem_filter.mpr constructor · apply Finset.mem_powerset.mpr intro r hr obtain ⟨j, _, rfl⟩ := Finset.mem_image.mp hr exact Fintype.mem_piFinset.mp hs j · exact Finset.mem_Icc.mpr (patternImage_card_bounds a hn) calc _ = ∑ T ∈ P, ∑ a ∈ (survivingPatterns S).filter (fun a => patternImage a = T), v ^ (patternImage a).card := (Finset.sum_fiberwise_of_maps_to hmaps _).symm _ ≤ ∑ T ∈ P, (T.card : ℝ) ^ 8 * v ^ T.card := by apply Finset.sum_le_sum intro T hT have hc : ((survivingPatterns S).filter (fun a => patternImage a = T)).card ≤ T.card ^ 8 := by apply le_trans (Finset.card_le_card _) (card_patterns_with_image_le S T) intro a ha obtain ⟨hs, he⟩ := Finset.mem_filter.mp ha exact Finset.mem_filter.mpr ⟨(Finset.mem_filter.mp hs).1, he⟩ calc _ = (((survivingPatterns S).filter (fun a => patternImage a = T)).card : ℝ) * v ^ T.card := by rw [← nsmul_eq_mul] rw [← Finset.sum_const] apply Finset.sum_congr rfl intro a ha rw [(Finset.mem_filter.mp ha).2] _ ≤ (T.card : ℝ) ^ 8 * v ^ T.card := mul_le_mul_of_nonneg_right (by exact_mod_cast hc) (pow_nonneg hv _) _ = ∑ k ∈ Icc 1 4, ∑ T ∈ P.filter (fun T => T.card = k), (T.card : ℝ) ^ 8 * v ^ T.card := by symm apply Finset.sum_fiberwise_of_maps_to intro T hT exact (Finset.mem_filter.mp hT).2 _ = _ := by apply Finset.sum_congr rfl intro k hk have hfilter : P.filter (fun T => T.card = k) = S.powersetCard k := by ext T simp only [P, mem_filter, Finset.mem_powersetCard, Finset.mem_powerset] constructor · rintro ⟨⟨hT, _⟩, he⟩ exact ⟨hT, he⟩ · rintro ⟨hT, he⟩ exact ⟨⟨hT, he ▸ hk⟩, he⟩ calc _ = ∑ T ∈ P.filter (fun T => T.card = k), (k : ℝ) ^ 8 * v ^ k := by apply Finset.sum_congr rfl intro T hT rw [(Finset.mem_filter.mp hT).2] _ = _ := by rw [Finset.sum_const, nsmul_eq_mul, hfilter, Finset.card_powersetCard] exact mul_assoc _ _ _ |>.symm

theorem choose_sum_le_polynomial (m : ℕ) (v : ℝ) (hv : 0 ≤ v) : (∑ k ∈ Icc 1 4, (m.choose k : ℝ) * (k : ℝ) ^ 8 * v ^ k) ≤ (m : ℝ) * v + 128 * ((m : ℝ) * v) ^ 2 + 1094 * ((m : ℝ) * v) ^ 3 + 2731 * ((m : ℝ) * v) ^ 4 := by -- Use `Nat.choose_le_pow_div (α := ℝ)` for k=1,2,3,4 and nonnegativity of v^k. -- The coefficients round up 1^8/1!, 2^8/2!, 3^8/3!, and 4^8/4! respectively. have h2 := mul_le_mul_of_nonneg_right (Nat.choose_le_pow_div (α := ℝ) 2 m) (pow_nonneg hv 2) have h3 := mul_le_mul_of_nonneg_right (Nat.choose_le_pow_div (α := ℝ) 3 m) (pow_nonneg hv 3) have h4 := mul_le_mul_of_nonneg_right (Nat.choose_le_pow_div (α := ℝ) 4 m) (pow_nonneg hv 4) norm_num [factorial] at h2 h3 h4 have hIcc : Icc 1 4 = {1, 2, 3, 4} := by decide norm_num [hIcc, mul_pow, Nat.choose_one_right] nlinarith [mul_nonneg (pow_nonneg (Nat.cast_nonneg m : (0 : ℝ) ≤ m) 3) (pow_nonneg hv 3), mul_nonneg (pow_nonneg (Nat.cast_nonneg m : (0 : ℝ) ≤ m) 4) (pow_nonneg hv 4)]

theorem sq_le_self_add_fourth (t : ℝ) (ht : 0 ≤ t) : t ^ 2 ≤ t + t ^ 4 := by by_cases h : t ≤ 1 · have h2 : t ^ 2 ≤ t := by nlinarith nlinarith [sq_nonneg (t ^ 2)] · have h2 : 1 ≤ t ^ 2 := by nlinarith nlinarith [sq_nonneg (t ^ 2 - 1)]

theorem cube_le_self_add_fourth (t : ℝ) (ht : 0 ≤ t) : t ^ 3 ≤ t + t ^ 4 := by by_cases h : t ≤ 1 · have h2 : t ^ 2 ≤ 1 := by nlinarith have := mul_nonneg ht (sub_nonneg.mpr h2) nlinarith [sq_nonneg (t ^ 2)] · have h3 : 0 ≤ t ^ 3 := pow_nonneg ht _ have := mul_nonneg h3 (sub_nonneg.mpr (le_of_not_ge h)) nlinarith

theorem polynomial_le_factorial (t : ℝ) (ht : 0 ≤ t) : t + 128 * t ^ 2 + 1094 * t ^ 3 + 2731 * t ^ 4 ≤ (factorial 8 : ℝ) * (t ^ 4 + t) := by have h2 := sq_le_self_add_fourth t ht have h3 := cube_le_self_add_fourth t ht norm_num [factorial] at * nlinarith [sq_nonneg (t ^ 2)]

theorem integral_eighth_sum_eq_pattern_sum (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : Measurable g) (hb : ∀ y, |g y| ≤ 1) (S : Finset ι) : (∫ x : ι → Ω, (∑ r ∈ S, g (x r)) ^ 8 ∂Measure.pi (fun _ : ι => μ)) = ∑ a ∈ piFinset (fun _ : Fin 8 => S), ∫ x : ι → Ω, (∏ j : Fin 8, g (x (a j))) ∂Measure.pi (fun _ : ι => μ) := by -- Rewrite pointwise by `Finset.sum_pow'`, then use `integral_finsetSum` and -- `integrable_pattern` for each term. No independence argument is needed in this step. classical have hexpand (x : ι → Ω) := Finset.sum_pow' S (fun r => g (x r)) 8 simp_rw [hexpand] exact integral_finsetSum _ (fun a _ => integrable_pattern μ g hg hb a)

theorem integral_eighth_sum_le_survivors (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : Measurable g) (hb : ∀ y, |g y| ≤ 1) (hcenter : (∫ y, g y ∂μ) = 0) (S : Finset ι) : (∫ x : ι → Ω, (∑ r ∈ S, g (x r)) ^ 8 ∂Measure.pi (fun _ : ι => μ)) ≤ ∑ a ∈ survivingPatterns S, (∫ y, g y ^ 2 ∂μ) ^ (patternImage a).card := by -- Start with the expansion above. If ¬NoSingleton a, a used coordinate has -- positive multiplicity <2, hence multiplicity 1; cancel using -- `integral_pattern_eq_zero_of_singleton`. Keep only the filter, use le_abs_self, -- and apply `abs_integral_pattern_le` termwise. classical rw [integral_eighth_sum_eq_pattern_sum μ g hg hb S] have hrestrict : (∑ a ∈ survivingPatterns S, ∫ x : ι → Ω, (∏ j : Fin 8, g (x (a j))) ∂Measure.pi (fun _ : ι => μ)) = ∑ a ∈ piFinset (fun _ : Fin 8 => S), ∫ x : ι → Ω, (∏ j : Fin 8, g (x (a j))) ∂Measure.pi (fun _ : ι => μ) := by apply Finset.sum_subset (filter_subset NoSingleton _) intro a ha hnot have hn : ¬NoSingleton a := fun h => hnot (Finset.mem_filter.mpr ⟨ha, h⟩) simp only [NoSingleton] at hn push Not at hn obtain ⟨r, hr, hlt⟩ := hn have hpos : 0 < multiplicity a r := by obtain ⟨j, _, hj⟩ := Finset.mem_image.mp hr exact Finset.card_pos.mpr ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ j, hj⟩⟩ exact integral_pattern_eq_zero_of_singleton μ g hcenter a r (by omega) rw [← hrestrict] apply Finset.sum_le_sum intro a ha exact (le_abs_self _).trans (abs_integral_pattern_le μ g hg hb a (Finset.mem_filter.mp ha).2)

theorem centered_sum_eighth_moment_le (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : Measurable g) (hb : ∀ y, |g y| ≤ 1) (hcenter : (∫ y, g y ∂μ) = 0) (S : Finset ι) : (∫ x : ι → Ω, (∑ r ∈ S, g (x r)) ^ 8 ∂Measure.pi (fun _ : ι => μ)) ≤ (factorial 8 : ℝ) * (((S.card : ℝ) * (∫ y, g y ^ 2 ∂μ)) ^ 4 + (S.card : ℝ) * (∫ y, g y ^ 2 ∂μ)) := by classical exact (integral_eighth_sum_le_survivors μ g hg hb hcenter S).trans (weighted_survivingPatterns_le S _ (integral_nonneg (fun y => sq_nonneg (g y))))

theorem integral_pattern_factorization (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (a : Fin 8 → ι) : (∫ x : ι → Ω, (∏ j : Fin 8, g (x (a j))) ∂Measure.pi (fun _ : ι => μ)) = ∏ r : ι, ∫ y, g y ^ multiplicity a r ∂μ := by -- Pointwise regroup via `Finset.prod_fiberwise'`, rewriting each fiber product as a power. -- Then apply `integral_fintype_prod_eq_prod` to the coordinate-dependent powers. have hprod (x : ι → Ω) : (∏ j : Fin 8, g (x (a j))) = ∏ r : ι, g (x r) ^ multiplicity a r := by simpa [multiplicity] using (Finset.prod_fiberwise' univ a (fun r => g (x r))).symm simp_rw [hprod] exact integral_fintype_prod_eq_prod (fun r y => g y ^ multiplicity a r)

@[fun_prop] theorem integrable_pattern (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : Measurable g) (hb : ∀ y, |g y| ≤ 1) (a : Fin 8 → ι) : Integrable (fun x : ι → Ω => ∏ j : Fin 8, g (x (a j))) (Measure.pi (fun _ : ι => μ)) := by classical have hm : Measurable (fun x : ι → Ω => ∏ j : Fin 8, g (x (a j))) := by fun_prop refine (integrable_const (1 : ℝ)).mono' hm.aestronglyMeasurable ?_ exact ae_of_all _ fun x => by rw [Real.norm_eq_abs, Finset.abs_prod] exact Finset.prod_le_one (fun j _ => abs_nonneg _) (fun j _ => hb _)

theorem integral_pattern_eq_zero_of_singleton (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hcenter : (∫ y, g y ∂μ) = 0) (a : Fin 8 → ι) (r : ι) (hr : multiplicity a r = 1) : (∫ x : ι → Ω, (∏ j : Fin 8, g (x (a j))) ∂Measure.pi (fun _ : ι => μ)) = 0 := by -- Factorization has a zero factor at r, since its multiplicity is one. rw [integral_pattern_factorization] exact Finset.prod_eq_zero (Finset.mem_univ r) (by simpa [hr] using hcenter)

@[fun_prop] theorem integrable_pow_of_abs_le_one (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : Measurable g) (hb : ∀ y, |g y| ≤ 1) (n : ℕ) : Integrable (fun y => g y ^ n) μ := by -- Dominate |g|^n by the integrable constant 1. refine (integrable_const (1 : ℝ)).mono' (hg.pow_const n).aestronglyMeasurable ?_ exact ae_of_all μ fun y => by simpa only [Real.norm_eq_abs, abs_pow] using (pow_le_one₀ (abs_nonneg (g y)) (hb y) : |g y| ^ n ≤ 1)

theorem abs_integral_pow_le_secondMoment (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : Measurable g) (hb : ∀ y, |g y| ≤ 1) (n : ℕ) (hn : 2 ≤ n) : |∫ y, g y ^ n ∂μ| ≤ ∫ y, g y ^ 2 ∂μ := by -- |g|^n ≤ |g|^2 follows from |g|≤1. Integrate the pointwise inequality and use -- `abs_integral_le_integral_abs`, with the integrability lemma above. have hi := integrable_pow_of_abs_le_one μ g hg hb n have hi2 := integrable_pow_of_abs_le_one μ g hg hb 2 refine abs_integral_le_integral_abs.trans (integral_mono hi.abs hi2 ?_) intro y change |g y ^ n| ≤ g y ^ 2 rw [abs_pow, ← sq_abs] exact pow_le_pow_of_le_one (abs_nonneg (g y)) (hb y) hn

theorem mean_mem_unitInterval (μ : Measure Ω) [IsProbabilityMeasure μ] (f : Ω → ℝ) (hf : Measurable f) (h0 : ∀ y, 0 ≤ f y) (h1 : ∀ y, f y ≤ 1) : 0 ≤ (∫ y, f y ∂μ) ∧ (∫ y, f y ∂μ) ≤ 1 := by -- Integrability follows from `integrable_pow_of_abs_le_one` with n=1. have hb : ∀ y, |f y| ≤ 1 := fun y => by rw [abs_of_nonneg (h0 y)] exact h1 y have hi : Integrable f μ := by simpa only [pow_one] using integrable_pow_of_abs_le_one μ f hf hb 1 refine ⟨integral_nonneg h0, ?_⟩ simpa using integral_mono hi (integrable_const (1 : ℝ)) h1

theorem abs_centered_mark_le_one (μ : Measure Ω) [IsProbabilityMeasure μ] (f : Ω → ℝ) (hf : Measurable f) (h0 : ∀ y, 0 ≤ f y) (h1 : ∀ y, f y ≤ 1) (y : Ω) : |f y - ∫ z, f z ∂μ| ≤ 1 := by obtain ⟨hm0, hm1⟩ := mean_mem_unitInterval μ f hf h0 h1 rw [abs_le] constructor <;> linarith [h0 y, h1 y]

theorem integral_centered_mark_eq_zero (μ : Measure Ω) [IsProbabilityMeasure μ] (f : Ω → ℝ) (hf : Measurable f) (h0 : ∀ y, 0 ≤ f y) (h1 : ∀ y, f y ≤ 1) : (∫ y, (f y - ∫ z, f z ∂μ) ∂μ) = 0 := by have hb : ∀ y, |f y| ≤ 1 := fun y => by rw [abs_of_nonneg (h0 y)]; exact h1 y have hi : Integrable f μ := by simpa only [pow_one] using integrable_pow_of_abs_le_one μ f hf hb 1 rw [integral_sub hi (integrable_const _)] simp