PL1/FiniteGrothendieckNormalization.lean

All source files · Download exact source

SHA-256: c1f0d7bea31419e91179b1680bbbdac219ee9f801aedd6761ba5a2d6eca7efc5

1import PL1.FiniteSummingFromMatrix2import PL1.FiniteRademacherClipping3import PL1.BonamiHaarBridge45noncomputable section6set_option backward.isDefEq.respectTransparency false7open scoped BigOperators8namespace PL1.FiniteGrothendieck9open PL1.Bonami PL1.FiniteRademacherClipping1011theorem card_cube (n : ℕ) : Fintype.card (Cube n) = 2 ^ n := by12  induction n with13  | zero => rfl14  | succ n ih =>15    change Fintype.card (Bool × Cube n) = _16    rw [Fintype.card_prod, Fintype.card_bool, ih, pow_succ]17    ring1819theorem average_eq_sum (n : ℕ) (f : Cube n → ℝ) :20    average n f = (∑ x, f x) / (2 : ℝ) ^ n := by21  induction n with22  | zero => simp [average, Cube]23  | succ n ih =>24    change (average n (fun x => f (false, x)) + average n (fun x => f (true, x))) / 2 = _25    rw [ih, ih]26    change _ = (∑ x : Bool × Cube n, f x) / _27    simp only [Fintype.sum_prod_type, Fintype.sum_bool, pow_succ]28    ring2930def finExtend {n : ℕ} (a : Fin n → ℝ) (j : ℕ) : ℝ :=31  if h : j < n then a ⟨j, h⟩ else 03233theorem energy_extend {n : ℕ} (a : Fin n → ℝ) :34    energy n (finExtend a) = ∑ j, (a j) ^ 2 := by35  unfold energy36  rw [Finset.sum_range]37  simp [finExtend]3839theorem mixed_extend {n : ℕ} (a b : Fin n → ℝ) :40    average n (fun x => rademacherSum n (finExtend a) x * rademacherSum n (finExtend b) x) =41      ∑ j, a j * b j := by42  rw [mixed_second_moment, Finset.sum_range]43  simp [finExtend]4445def coordinates (n : ℕ) (f : Cube n → ℝ) : Fin (Fintype.card (Cube n)) → ℝ :=46  fun i => f ((Fintype.equivFin (Cube n)).symm i) / Real.sqrt ((2 : ℝ) ^ n)4748theorem coordinates_product (n : ℕ) (f g : Cube n → ℝ) :49    (∑ i, coordinates n f i * coordinates n g i) = average n (fun x => f x * g x) := by50  simp only [coordinates, div_mul_div_comm]51  rw [← pow_two, Real.sq_sqrt (by positivity : 0 ≤ (2 : ℝ) ^ n)]52  rw [← Finset.sum_div, (Fintype.equivFin (Cube n)).symm.sum_comp (fun x => f x * g x)]53  exact (average_eq_sum n _).symm5455theorem coordinates_square (n : ℕ) (f : Cube n → ℝ) :56    (∑ i, coordinates n f i ^ 2) = average n (fun x => f x ^ 2) := by57  simpa only [pow_two] using coordinates_product n f f5859theorem average_sum {ι : Type*} (n : ℕ) (s : Finset ι) (f : ι → Cube n → ℝ) :60    average n (fun x => ∑ i ∈ s, f i x) = ∑ i ∈ s, average n (f i) := by61  classical62  induction s using Finset.induction_on with63  | empty => simp64  | @insert i s hi ih => simp [hi, ih]6566theorem abs_average_le (n : ℕ) (f : Cube n → ℝ) (B : ℝ)67    (h : ∀ x, |f x| ≤ B) : |average n f| ≤ B := by68  apply abs_le.mpr69  constructor70  · have hh := average_mono n (fun x => (abs_le.mp (h x)).1)71    simpa using hh72  · have hh := average_mono n (fun x => (abs_le.mp (h x)).2)73    simpa using hh7475end PL1.FiniteGrothendieck767778