PL1/FiniteRademacherClipping.lean
All source files · Download exact source
SHA-256: 1fc2851438559a73076a82bb637936f4ef9559a39c082078fcfbbbcbf96bf768
1import PL1.BonamiTensorization23/-! Concrete finite Rademacher moments and clipping. -/45noncomputable section6open scoped BigOperators78namespace PL1.FiniteRademacherClipping9open PL1.Bonami1011/-- The newest Boolean coordinate supplies the sign of coefficient a(n). -/12def rademacherSum : (n : ℕ) → (ℕ → ℝ) → Cube n → ℝ13 | 0, _, _ => 014 | n + 1, a, (b, x) => (if b then -a n else a n) + rademacherSum n a x1516def energy (n : ℕ) (a : ℕ → ℝ) : ℝ := ∑ j ∈ Finset.range n, (a j) ^ 21718theorem energy_nonneg (n : ℕ) (a : ℕ → ℝ) : 0 ≤ energy n a :=19 Finset.sum_nonneg (fun _ _ => sq_nonneg _)2021theorem energy_succ (n : ℕ) (a : ℕ → ℝ) :22 energy (n + 1) a = energy n a + (a n) ^ 2 := Finset.sum_range_succ _ _2324theorem second_moment (n : ℕ) (a : ℕ → ℝ) :25 average n (fun x => rademacherSum n a x ^ 2) = energy n a := by26 induction n with27 | zero => simp [rademacherSum, average, energy]28 | succ n ih =>29 change (average n (fun x => (a n + rademacherSum n a x) ^ 2) +30 average n (fun x => (-a n + rademacherSum n a x) ^ 2)) / 2 = _31 rw [← average_add]32 have hp : (fun x : Cube n => (a n + rademacherSum n a x) ^ 2 +33 (-a n + rademacherSum n a x) ^ 2) =34 (fun x => 2 * ((a n) ^ 2 + rademacherSum n a x ^ 2)) := by35 funext x36 ring37 rw [hp, average_mul, average_add, average_const, ih, energy_succ]38 ring3940theorem mixed_second_moment (n : ℕ) (a b : ℕ → ℝ) :41 average n (fun x => rademacherSum n a x * rademacherSum n b x) =42 ∑ j ∈ Finset.range n, a j * b j := by43 induction n with44 | zero => simp [rademacherSum, average]45 | succ n ih =>46 change (average n (fun x => (a n + rademacherSum n a x) * (b n + rademacherSum n b x)) +47 average n (fun x => (-a n + rademacherSum n a x) * (-b n + rademacherSum n b x))) / 2 = _48 rw [← average_add]49 have hp : (fun x : Cube n =>50 (a n + rademacherSum n a x) * (b n + rademacherSum n b x) +51 (-a n + rademacherSum n a x) * (-b n + rademacherSum n b x)) =52 (fun x => 2 * (a n * b n + rademacherSum n a x * rademacherSum n b x)) := by53 funext x54 ring55 rw [hp, average_mul, average_add, average_const, ih, Finset.sum_range_succ]56 ring5758theorem fourth_moment (n : ℕ) (a : ℕ → ℝ) :59 average n (fun x => rademacherSum n a x ^ 4) =60 3 * (energy n a) ^ 2 - 2 * ∑ j ∈ Finset.range n, (a j) ^ 4 := by61 induction n with62 | zero => simp [rademacherSum, average, energy]63 | succ n ih =>64 change (average n (fun x => (a n + rademacherSum n a x) ^ 4) +65 average n (fun x => (-a n + rademacherSum n a x) ^ 4)) / 2 = _66 rw [← average_add]67 have hp : (fun x : Cube n => (a n + rademacherSum n a x) ^ 4 +68 (-a n + rademacherSum n a x) ^ 4) =69 (fun x => 2 * ((a n) ^ 4 + 6 * (a n) ^ 2 * rademacherSum n a x ^ 2 +70 rademacherSum n a x ^ 4)) := by71 funext x72 ring73 rw [hp, average_mul, average_add, average_add, average_const,74 average_mul, second_moment, ih, energy_succ, Finset.sum_range_succ]75 ring7677theorem fourth_moment_le (n : ℕ) (a : ℕ → ℝ) :78 average n (fun x => rademacherSum n a x ^ 4) ≤ 3 * (energy n a) ^ 2 := by79 rw [fourth_moment]80 have h : 0 ≤ ∑ j ∈ Finset.range n, (a j) ^ 4 := Finset.sum_nonneg (fun _ _ => by positivity)81 linarith8283def clipEight (z : ℝ) : ℝ := if 8 < z then 8 else if z < -8 then -8 else z8485theorem abs_clipEight_le (z : ℝ) : |clipEight z| ≤ 8 := by86 unfold clipEight87 split_ifs with hp hn88 · norm_num89 · norm_num90 · exact abs_le.mpr ⟨le_of_not_gt hn, le_of_not_gt hp⟩9192theorem clipEight_sq_le (z : ℝ) : clipEight z ^ 2 ≤ z ^ 2 := by93 unfold clipEight94 split_ifs with hp hn <;> nlinarith9596theorem residual_sq_le_fourth (z : ℝ) : (z - clipEight z) ^ 2 ≤ z ^ 4 / 64 := by97 unfold clipEight98 split_ifs with hp hn99 · have hs : 64 ≤ z ^ 2 := by nlinarith100 have h4 := mul_nonneg (sub_nonneg.mpr hs) (sq_nonneg z)101 nlinarith102 · have hs : 64 ≤ z ^ 2 := by nlinarith103 have h4 := mul_nonneg (sub_nonneg.mpr hs) (sq_nonneg z)104 nlinarith105 · simp only [sub_self, zero_pow (by norm_num : 2 ≠ 0)]106 positivity107108theorem clipped_second_moment_le (n : ℕ) (a : ℕ → ℝ) :109 average n (fun x => clipEight (rademacherSum n a x) ^ 2) ≤ energy n a := by110 rw [← second_moment]111 exact average_mono n (fun x => clipEight_sq_le (rademacherSum n a x))112113theorem residual_second_moment_le (n : ℕ) (a : ℕ → ℝ) (ha : energy n a ≤ 1) :114 average n (fun x => (rademacherSum n a x - clipEight (rademacherSum n a x)) ^ 2) ≤115 (1 / 16 : ℝ) := by116 have h := average_mono n (fun x => residual_sq_le_fourth (rademacherSum n a x))117 have he : average n (fun x => rademacherSum n a x ^ 4 / 64) =118 (1 / 64 : ℝ) * average n (fun x => rademacherSum n a x ^ 4) := by119 convert average_mul n (1 / 64 : ℝ) (fun x => rademacherSum n a x ^ 4) using 1120 congr 1121 funext x122 ring123 rw [he] at h124 have h4 := fourth_moment_le n a125 have hs := pow_le_pow_left₀ (energy_nonneg n a) ha 2126 nlinarith127128#print axioms second_moment129#print axioms mixed_second_moment130#print axioms fourth_moment_le131#print axioms residual_second_moment_le132133end PL1.FiniteRademacherClipping134135