PL1/BonamiTensorization.lean
All source files · Download exact source
SHA-256: d42fee4958cc2aa3220ac71e4c9ccecc2b79723405341ee1bfcbe11da6fd9713
1import Mathlib.Analysis.MeanInequalities2import PL1.BonamiTwoPoint3import Mathlib.Tactic.Positivity4import Mathlib.Tactic.NormNum5import Mathlib.Tactic.Ring67/-! # Dimension-independent tensorization of the two-point noise inequality89The finite cubes and their normalized averages are explicit. The scalar10two-point estimate is a visible premise of the tensorization theorem.11-/1213noncomputable section14open scoped BigOperators1516namespace PL1.Bonami1718def Cube : ℕ → Type19 | 0 => Unit20 | n + 1 => Bool × Cube n2122def average : (n : ℕ) → (Cube n → ℝ) → ℝ23 | 0, f => f ()24 | n + 1, f => (average n (fun x => f (false, x)) +25 average n (fun x => f (true, x))) / 22627theorem average_nonneg (n : ℕ) {f : Cube n → ℝ} (hf : ∀ x, 0 ≤ f x) :28 0 ≤ average n f := by29 induction n with30 | zero => exact hf ()31 | succ n ih =>32 exact div_nonneg (add_nonneg (ih (fun x => hf (false, x)))33 (ih (fun x => hf (true, x)))) (by norm_num)3435theorem average_mono (n : ℕ) {f g : Cube n → ℝ} (hfg : ∀ x, f x ≤ g x) :36 average n f ≤ average n g := by37 induction n with38 | zero => exact hfg ()39 | succ n ih =>40 exact div_le_div_of_nonneg_right (add_le_add (ih (fun x => hfg (false, x)))41 (ih (fun x => hfg (true, x)))) (by norm_num)4243theorem average_congr (n : ℕ) {f g : Cube n → ℝ} (hfg : ∀ x, f x = g x) :44 average n f = average n g := congrArg (average n) (funext hfg)4546@[simp] theorem average_add (n : ℕ) (f g : Cube n → ℝ) :47 average n (fun x => f x + g x) = average n f + average n g := by48 induction n with49 | zero => rfl50 | succ n ih => simp only [average, ih]; ring5152@[simp] theorem average_mul (n : ℕ) (c : ℝ) (f : Cube n → ℝ) :53 average n (fun x => c * f x) = c * average n f := by54 induction n with55 | zero => rfl56 | succ n ih => simp only [average, ih]; ring5758@[simp] theorem average_const (n : ℕ) (c : ℝ) : average n (fun _ => c) = c := by59 induction n with60 | zero => rfl61 | succ n ih => simp only [average, ih]; ring6263def pairNorm (r a b : ℝ) : ℝ := (a ^ r + b ^ r) ^ (1 / r)6465theorem pairNorm_nonneg {r a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) :66 0 ≤ pairNorm r a b := Real.rpow_nonneg (by positivity) _6768theorem pairNorm_mono {r a b c d : ℝ} (hr : 0 ≤ r)69 (ha : 0 ≤ a) (hb : 0 ≤ b) (hac : a ≤ c) (hbd : b ≤ d) :70 pairNorm r a b ≤ pairNorm r c d := by71 exact Real.rpow_le_rpow (by positivity)72 (add_le_add (Real.rpow_le_rpow ha hac hr) (Real.rpow_le_rpow hb hbd hr))73 (by positivity)7475theorem pairNorm_add_le {r a b c d : ℝ} (hr : 1 ≤ r)76 (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) :77 pairNorm r (a + c) (b + d) ≤ pairNorm r a b + pairNorm r c d := by78 have h := Real.Lp_add_le (Finset.univ : Finset Bool)79 (fun i => if i then b else a) (fun i => if i then d else c) hr80 simpa [pairNorm, Fintype.sum_bool, abs_of_nonneg ha, abs_of_nonneg hb,81 abs_of_nonneg hc, abs_of_nonneg hd, abs_of_nonneg (add_nonneg ha hc),82 abs_of_nonneg (add_nonneg hb hd), add_comm] using h8384theorem pairNorm_mul {r a b c : ℝ} (hr : r ≠ 0)85 (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) :86 pairNorm r (c * a) (c * b) = c * pairNorm r a b := by87 unfold pairNorm88 rw [Real.mul_rpow hc ha, Real.mul_rpow hc hb, ← mul_add,89 Real.mul_rpow (Real.rpow_nonneg hc _) (by positivity),90 ← Real.rpow_mul hc]91 simp [hr]9293/-- The mixed-norm inequality needed for the tensor step, derived from94ordinary Minkowski at the conjugate mixed exponent. -/95theorem pairNorm_average_le (n : ℕ) {r : ℝ} (hr : 1 ≤ r)96 (f g : Cube n → ℝ) (hf : ∀ x, 0 ≤ f x) (hg : ∀ x, 0 ≤ g x) :97 pairNorm r (average n f) (average n g) ≤98 average n (fun x => pairNorm r (f x) (g x)) := by99 induction n with100 | zero => exact le_rfl101 | succ n ih =>102 have hf0 := average_nonneg n (fun x => hf (false, x))103 have hf1 := average_nonneg n (fun x => hf (true, x))104 have hg0 := average_nonneg n (fun x => hg (false, x))105 have hg1 := average_nonneg n (fun x => hg (true, x))106 simp only [average]107 rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm _ (2 : ℝ)⁻¹,108 mul_comm _ (2 : ℝ)⁻¹,109 pairNorm_mul (ne_of_gt (lt_of_lt_of_le zero_lt_one hr))110 (add_nonneg hf0 hf1) (add_nonneg hg0 hg1) (by norm_num)]111 calc112 _ ≤ (2 : ℝ)⁻¹ * (pairNorm r (average n (fun x => f (false, x)))113 (average n (fun x => g (false, x))) +114 pairNorm r (average n (fun x => f (true, x)))115 (average n (fun x => g (true, x)))) :=116 mul_le_mul_of_nonneg_left (pairNorm_add_le hr hf0 hg0 hf1 hg1) (by norm_num)117 _ ≤ _ := by118 rw [div_eq_mul_inv, mul_comm]119 exact mul_le_mul_of_nonneg_right120 (add_le_add (ih _ _ (fun x => hf (false, x)) (fun x => hg (false, x)))121 (ih _ _ (fun x => hf (true, x)) (fun x => hg (true, x)))) (show 0 ≤ (2 : ℝ)⁻¹ by norm_num)122123def moment (n : ℕ) (p : ℝ) (f : Cube n → ℝ) : ℝ :=124 average n (fun x => |f x| ^ p)125126theorem moment_nonneg (n : ℕ) (p : ℝ) (f : Cube n → ℝ) : 0 ≤ moment n p f :=127 average_nonneg n (fun x => Real.rpow_nonneg (abs_nonneg _) _)128129theorem moment_mul (n : ℕ) (p c : ℝ) (f : Cube n → ℝ) :130 moment n p (fun x => c * f x) = |c| ^ p * moment n p f := by131 simp only [moment, abs_mul, Real.mul_rpow (abs_nonneg c) (abs_nonneg _), average_mul]132133theorem mixed_moment_le (n : ℕ) {p : ℝ} (hp : 0 < p) (hp2 : p ≤ 2)134 (f g : Cube n → ℝ) :135 moment n p f ^ (2 / p) + moment n p g ^ (2 / p) ≤136 average n (fun x => (f x ^ 2 + g x ^ 2) ^ (p / 2)) ^ (2 / p) := by137 have hr : 1 ≤ 2 / p := (le_div_iff₀ hp).mpr (by linarith)138 have hi : 1 / (2 / p) = p / 2 := by field_simp139 have hpow (a : ℝ) : (|a| ^ p) ^ (2 / p) = a ^ 2 := by140 rw [← Real.rpow_mul (abs_nonneg _)]141 have he : p * (2 / p) = 2 := by field_simp142 rw [he, Real.rpow_two, sq_abs]143 have h := pairNorm_average_le n hr (fun x => |f x| ^ p) (fun x => |g x| ^ p)144 (fun x => Real.rpow_nonneg (abs_nonneg _) _) (fun x => Real.rpow_nonneg (abs_nonneg _) _)145 simp only [pairNorm, hi, hpow] at h146 have hb : 0 ≤ moment n p f ^ (2 / p) + moment n p g ^ (2 / p) :=147 add_nonneg (Real.rpow_nonneg (moment_nonneg _ _ _) _) (Real.rpow_nonneg (moment_nonneg _ _ _) _)148 have h' := Real.rpow_le_rpow (Real.rpow_nonneg hb (p / 2)) h149 (show 0 ≤ (2 : ℝ) / p by positivity)150 rw [← Real.rpow_mul hb] at h'151 have he : p / 2 * (2 / p) = 1 := by field_simp152 simpa only [he, Real.rpow_one, moment] using h'153154def meanSlice {n : ℕ} (f : Cube (n + 1) → ℝ) (x : Cube n) : ℝ :=155 (f (false, x) + f (true, x)) / 2156157def diffSlice {n : ℕ} (f : Cube (n + 1) → ℝ) (x : Cube n) : ℝ :=158 (f (false, x) - f (true, x)) / 2159160/-- The tensor product of the two-point noise maps. False represents +1. -/161def noise (ρ : ℝ) : (n : ℕ) → (Cube n → ℝ) → Cube n → ℝ162 | 0, f => f163 | n + 1, f => fun x => noise ρ n (meanSlice f) x.2 +164 (if x.1 then -ρ else ρ) * noise ρ n (diffSlice f) x.2165166theorem average_noise_sq (ρ : ℝ) (n : ℕ) (f : Cube (n + 1) → ℝ) :167 average (n + 1) (fun x => noise ρ (n + 1) f x ^ 2) =168 average n (fun x => noise ρ n (meanSlice f) x ^ 2) +169 ρ ^ 2 * average n (fun x => noise ρ n (diffSlice f) x ^ 2) := by170 simp only [average, noise, Bool.false_eq_true, ↓reduceIte]171 rw [← average_add, ← average_mul, ← average_add]172 calc173 _ = average n (fun x => 2 * (noise ρ n (meanSlice f) x ^ 2 +174 ρ ^ 2 * noise ρ n (diffSlice f) x ^ 2)) / 2 := by175 congr 1176 apply average_congr177 intro x178 ring179 _ = _ := by rw [average_mul]; ring180181/-- An explicit scalar hypothesis; this is discharged by the scalar Bonami182inequality in the application, rather than hidden in a typeclass. -/183def TwoPointBound (p ρ : ℝ) : Prop :=184 ∀ a b : ℝ, (a ^ 2 + (ρ * b) ^ 2) ^ (p / 2) ≤185 (|a + b| ^ p + |a - b| ^ p) / 2186187/-- Every finite tensor power has the same norm bound one. -/188theorem noise_moment_bound {p ρ : ℝ} (hp : 0 < p) (hp2 : p ≤ 2)189 (hpoint : TwoPointBound p ρ) (n : ℕ) (f : Cube n → ℝ) :190 average n (fun x => noise ρ n f x ^ 2) ≤ moment n p f ^ (2 / p) := by191 induction n with192 | zero =>193 simp only [average, noise, moment]194 rw [← Real.rpow_mul (abs_nonneg _)]195 have he : p * (2 / p) = 2 := by field_simp196 rw [he, Real.rpow_two, sq_abs]197 | succ n ih =>198 rw [average_noise_sq]199 calc200 _ ≤ moment n p (meanSlice f) ^ (2 / p) +201 ρ ^ 2 * moment n p (diffSlice f) ^ (2 / p) :=202 add_le_add (ih _) (mul_le_mul_of_nonneg_left (ih _) (sq_nonneg _))203 _ = moment n p (meanSlice f) ^ (2 / p) +204 moment n p (fun x => ρ * diffSlice f x) ^ (2 / p) := by205 rw [moment_mul, Real.mul_rpow (Real.rpow_nonneg (abs_nonneg _) _)206 (moment_nonneg _ _ _), ← Real.rpow_mul (abs_nonneg _)]207 have he : p * (2 / p) = 2 := by field_simp208 rw [he, Real.rpow_two, sq_abs]209 _ ≤ average n (fun x => (meanSlice f x ^ 2 + (ρ * diffSlice f x) ^ 2) ^210 (p / 2)) ^ (2 / p) := mixed_moment_le n hp hp2 _ _211 _ ≤ moment (n + 1) p f ^ (2 / p) := by212 apply Real.rpow_le_rpow (average_nonneg n (fun x => by positivity)) _ (by positivity)213 calc214 _ ≤ average n (fun x => (|meanSlice f x + diffSlice f x| ^ p +215 |meanSlice f x - diffSlice f x| ^ p) / 2) :=216 average_mono n (fun x => hpoint _ _)217 _ = moment (n + 1) p f := by218 have hplus (x : Cube n) : meanSlice f x + diffSlice f x = f (false, x) := by219 simp only [meanSlice, diffSlice]; ring220 have hminus (x : Cube n) : meanSlice f x - diffSlice f x = f (true, x) := by221 simp only [meanSlice, diffSlice]; ring222 simp only [hplus, hminus, moment, average, div_eq_mul_inv]223 rw [show (fun x : Cube n => (|f (false, x)| ^ p + |f (true, x)| ^ p) * 2⁻¹) =224 (fun x => 2⁻¹ * (|f (false, x)| ^ p + |f (true, x)| ^ p)) by225 funext x; ring, average_mul, average_add]226 ring227228/-- The sharp finite-dimensional Bonami estimate with its scalar premise229fully discharged. -/230theorem noise_moment_bound_sharp {p ρ : ℝ} (hp : 1 ≤ p) (hp2 : p ≤ 2)231 (hρ : ρ ^ 2 ≤ p - 1) (n : ℕ) (f : Cube n → ℝ) :232 average n (fun x => noise ρ n f x ^ 2) ≤ moment n p f ^ (2 / p) :=233 noise_moment_bound (lt_of_lt_of_le zero_lt_one hp) hp2234 (BonamiTwoPoint.noise_moment p ρ hp hp2 hρ) n f235236@[simp] theorem noise_zero (ρ : ℝ) (n : ℕ) : noise ρ n (fun _ => 0) = fun _ => 0 := by237 induction n with238 | zero => rfl239 | succ n ih =>240 have hm : meanSlice (fun _ : Cube (n + 1) => (0 : ℝ)) = fun _ => 0 := by241 funext x; simp [meanSlice]242 have hd : diffSlice (fun _ : Cube (n + 1) => (0 : ℝ)) = fun _ => 0 := by243 funext x; simp [diffSlice]244 funext x245 simp [noise, hm, hd, ih]246247theorem noise_add (ρ : ℝ) (n : ℕ) (f g : Cube n → ℝ) :248 noise ρ n (fun x => f x + g x) = fun x => noise ρ n f x + noise ρ n g x := by249 induction n with250 | zero => rfl251 | succ n ih =>252 have hm : meanSlice (fun x => f x + g x) = fun x => meanSlice f x + meanSlice g x := by253 funext x; simp only [meanSlice]; ring254 have hd : diffSlice (fun x => f x + g x) = fun x => diffSlice f x + diffSlice g x := by255 funext x; simp only [diffSlice]; ring256 funext x257 simp only [noise, hm, hd, ih]258 ring259260theorem noise_mul (ρ : ℝ) (n : ℕ) (c : ℝ) (f : Cube n → ℝ) :261 noise ρ n (fun x => c * f x) = fun x => c * noise ρ n f x := by262 induction n with263 | zero => rfl264 | succ n ih =>265 have hm : meanSlice (fun x => c * f x) = fun x => c * meanSlice f x := by266 funext x; simp only [meanSlice]; ring267 have hd : diffSlice (fun x => c * f x) = fun x => c * diffSlice f x := by268 funext x; simp only [diffSlice]; ring269 funext x270 simp only [noise, hm, hd, ih]271 ring272273theorem noise_sum (ρ : ℝ) (n : ℕ) {ι : Type*} (s : Finset ι) (f : ι → Cube n → ℝ) :274 noise ρ n (fun x => ∑ i ∈ s, f i x) = fun x => ∑ i ∈ s, noise ρ n (f i) x := by275 classical276 induction s using Finset.induction_on with277 | empty => simpa using noise_zero ρ n278 | @insert i s hi ih => simp only [Finset.sum_insert hi, noise_add, ih]279280end PL1.Bonami281282283