PL1/EnfloHypercontractive.lean
All source files · Download exact source
SHA-256: c3049051645c852485481f0991bb9468d1b1d2c5fb738d759bf4b2ddb4bdd148
1import PL1.EnfloMaxMass2import PL1.LpInterpolation3import PL1.NoiseHypercontractivity45/-! # Finite maximum bounds from the actual noise Lp-to-L2 contraction -/67noncomputable section8open MeasureTheory9open scoped BigOperators ENNReal NNReal1011namespace PL1.EnfloBush12open Walsh Noise NoiseHypercontractivity1314theorem maxAbs_sq_le_energy (n : ℕ) (a : ℕ → ℝ) :15 maxAbs n a ^ 2 ≤ FiniteRademacherClipping.energy n a := by16 induction n with17 | zero => simp [maxAbs, FiniteRademacherClipping.energy]18 | succ n ih =>19 rw [maxAbs, FiniteRademacherClipping.energy_succ]20 by_cases h : maxAbs n a ≤ |a n|21 · rw [max_eq_right h, sq_abs]22 nlinarith [FiniteRademacherClipping.energy_nonneg n a]23 · rw [max_eq_left (le_of_not_ge h)]24 nlinarith [sq_nonneg (a n)]2526theorem memLp_maxAbs (n : ℕ) (f : ℕ → Lp ℝ 2 haar) :27 MemLp (fun x => maxAbs n (fun j => f j x)) 2 haar := by28 induction n with29 | zero => exact MemLp.zero30 | succ n ih => exact ih.sup (Lp.memLp (f n)).abs3132def maxL2 (n : ℕ) (f : ℕ → Lp ℝ 2 haar) : Lp ℝ 2 haar :=33 (memLp_maxAbs n f).toLp (fun x => maxAbs n (fun j => f j x))3435theorem maxL2_coe (n : ℕ) (f : ℕ → Lp ℝ 2 haar) :36 maxL2 n f =ᵐ[haar] (fun x => maxAbs n (fun j => f j x)) :=37 (memLp_maxAbs n f).coeFn_toLp3839theorem norm_l2_sq_eq_integral (f : Lp ℝ 2 haar) :40 ‖f‖ ^ 2 = ∫ x, f x ^ 2 ∂haar := by41 simpa only [ENNReal.toReal_ofNat, div_self (by norm_num : (2 : ℝ) ≠ 0),42 Real.rpow_one, Real.rpow_two, Real.norm_eq_abs, sq_abs] using43 norm_sq_eq_integral_rpow ℝ 2 (by norm_num) f (Filter.EventuallyEq.rfl : f =ᵐ[haar] f)4445theorem integrable_l2_sq (f : Lp ℝ 2 haar) : Integrable (fun x => f x ^ 2) haar := by46 simpa only [Real.norm_eq_abs, sq_abs] using47 (Lp.memLp f).integrable_norm_pow (by norm_num : (2 : ℕ) ≠ 0)4849theorem maxMass_l2_eq (n : ℕ) (f : ℕ → Lp ℝ 2 haar) :50 maxMass n (fun j => l2ToL1 (f j)) = ‖l2ToL1 (maxL2 n f)‖ := by51 rw [maxMass, L1.norm_eq_integral_norm]52 apply integral_congr_ae53 filter_upwards [ae_all_iff.mpr (fun j => ProbabilityLp.coeFn_inclusion haar 1 2 (by norm_num) (f j)),54 ProbabilityLp.coeFn_inclusion haar 1 2 (by norm_num) (maxL2 n f), maxL2_coe n f] with x hf hm he55 rw [hm, he, Real.norm_eq_abs, abs_of_nonneg (maxAbs_nonneg n _)]56 exact maxAbs_congr (fun j _ => hf j)5758theorem maxMass_l2_sq_le (n : ℕ) (f : ℕ → Lp ℝ 2 haar) :59 maxMass n (fun j => l2ToL1 (f j)) ^ 2 ≤ ∑ j ∈ Finset.range n, ‖f j‖ ^ 2 := by60 have hnorm : ‖l2ToL1 (maxL2 n f)‖ ≤ ‖maxL2 n f‖ :=61 ProbabilityLp.norm_inclusionFun_le haar 1 2 (by norm_num) _62 rw [maxMass_l2_eq]63 apply (pow_le_pow_left₀ (norm_nonneg _) hnorm 2).trans64 rw [norm_l2_sq_eq_integral]65 have he : (fun x => maxL2 n f x ^ 2) =ᵐ[haar]66 (fun x => maxAbs n (fun j => f j x) ^ 2) := by67 filter_upwards [maxL2_coe n f] with x hx68 rw [hx]69 have hi : Integrable (fun x => maxAbs n (fun j => f j x) ^ 2) haar :=70 (integrable_l2_sq (maxL2 n f)).congr he71 rw [integral_congr_ae he]72 have h := integral_mono hi (integrable_finsetSum _ (fun j _ => integrable_l2_sq (f j)))73 (fun x => maxAbs_sq_le_energy n (fun j => f j x))74 rw [integral_finsetSum _ (fun j _ => integrable_l2_sq (f j))] at h75 simpa only [← norm_l2_sq_eq_integral] using h7677theorem rpow_sq_eq (x a : ℝ) (hx : 0 ≤ x) : (x ^ a) ^ 2 = x ^ (2 * a) := by78 rw [← Real.rpow_two, ← Real.rpow_mul hx]79 congr 180 ring8182theorem rpow_le_bound_mul {x A r : ℝ} (hx : 0 ≤ x) (hxA : x ≤ A) (hr : 0 ≤ r) :83 x ^ (r + 1) ≤ A ^ r * x := by84 rw [Real.rpow_add_of_nonneg hx hr zero_le_one, Real.rpow_one]85 exact mul_le_mul_of_nonneg_right (Real.rpow_le_rpow hx hxA hr) hx8687theorem positiveTimeNoiseL2_bounded_sq_le (u : ℝ≥0) (f : Lp ℝ 1 haar)88 (M : ℝ) (hM : 0 ≤ M) (hfM : ∀ᵐ x ∂haar, ‖f x‖ ≤ M)89 (hf : MemLp (fun x => f x) (exponent u) haar) :90 ‖positiveTimeNoiseL2 ℝ u (hf.toLp (fun x => f x))‖ ^ 2 ≤91 M ^ (2 * (1 - 1 / (exponent u).toReal)) * ‖f‖ ^ (2 / (exponent u).toReal) := by92 have h₁ : ‖positiveTimeNoiseL2 ℝ u (hf.toLp (fun x => f x))‖ ≤ ‖hf.toLp (fun x => f x)‖ := by93 calc94 _ ≤ ‖positiveTimeNoiseL2 ℝ u‖ * ‖hf.toLp (fun x => f x)‖ :=95 (positiveTimeNoiseL2 ℝ u).le_opNorm _96 _ ≤ 1 * ‖hf.toLp (fun x => f x)‖ := mul_le_mul_of_nonneg_right97 (norm_positiveTimeNoiseL2_le_one ℝ u) (norm_nonneg _)98 _ = _ := one_mul _99 have h₂ := LpInterpolation.norm_toLp_le_of_ae_norm_bound f (exponent u)100 (exponent_ge_one u) (exponent_ne_top u) M hM hfM hf101 have h := pow_le_pow_left₀ (norm_nonneg _) (h₁.trans h₂) 2102 rw [mul_pow, rpow_sq_eq M _ hM, rpow_sq_eq ‖f‖ _ (norm_nonneg _)] at h103 simpa only [mul_one_div] using h104105/-- Uniform finite-family estimate for actual constant-rate noise. No106dimension appears in the constant; the small L1 mass carries a positive107power at every positive noise time. -/108theorem bounded_family_noise_max_sq_le (u : ℝ≥0) (n : ℕ) (f : ℕ → Lp ℝ 1 haar)109 (M : ℝ) (hM : 0 ≤ M) (hfM : ∀ j, ∀ᵐ x ∂haar, ‖f j x‖ ≤ M)110 (A C : ℝ) (hA : 0 ≤ A) (_hC : 0 ≤ C)111 (hfA : ∀ j < n, ‖f j‖ ≤ A) (hfC : (∑ j ∈ Finset.range n, ‖f j‖) ≤ C) :112 maxMass n (fun j => noiseL1 ℝ constantRates u (f j)) ^ 2 ≤113 M ^ (2 * (1 - 1 / (exponent u).toReal)) * A ^ (2 / (exponent u).toReal - 1) * C := by114 let p := exponent u115 have hp (j : ℕ) : MemLp (fun x => f j x) p haar :=116 LpInterpolation.memLp_of_ae_norm_bound (f j) p (exponent_ge_one u) (exponent_ne_top u) M (hfM j)117 let F : ℕ → Lp ℝ 2 haar := fun j => positiveTimeNoiseL2 ℝ u ((hp j).toLp (fun x => f j x))118 have hF (j : ℕ) : l2ToL1 (F j) = noiseL1 ℝ constantRates u (f j) := by119 dsimp only [F]120 rw [positiveTimeNoiseL2_overlap]121 congr 1122 apply Lp.ext123 exact (ProbabilityLp.coeFn_inclusion haar 1 p (exponent_ge_one u) _).trans (hp j).coeFn_toLp124 have h := maxMass_l2_sq_le n F125 simp_rw [hF] at h126 apply h.trans127 have hp0 : 0 < p.toReal := by rw [exponent_toReal]; positivity128 have hr : 0 ≤ 2 / p.toReal - 1 := by129 have hp2 := exponent_toReal_le_two u130 have he : 1 ≤ 2 / p.toReal := (le_div_iff₀ hp0).mpr (by simpa only [one_mul] using hp2)131 linarith132 calc133 _ ≤ ∑ j ∈ Finset.range n, M ^ (2 * (1 - 1 / p.toReal)) * ‖f j‖ ^ (2 / p.toReal) :=134 Finset.sum_le_sum (fun j _ => positiveTimeNoiseL2_bounded_sq_le u (f j) M hM (hfM j) (hp j))135 _ ≤ ∑ j ∈ Finset.range n, M ^ (2 * (1 - 1 / p.toReal)) *136 (A ^ (2 / p.toReal - 1) * ‖f j‖) := by137 apply Finset.sum_le_sum138 intro j hj139 apply mul_le_mul_of_nonneg_left _ (Real.rpow_nonneg hM _)140 have hh := rpow_le_bound_mul (norm_nonneg (f j)) (hfA j (Finset.mem_range.mp hj)) hr141 simpa only [sub_add_cancel] using hh142 _ = (M ^ (2 * (1 - 1 / p.toReal)) * A ^ (2 / p.toReal - 1)) *143 ∑ j ∈ Finset.range n, ‖f j‖ := by simp only [← mul_assoc, Finset.mul_sum]144 _ ≤ _ := mul_le_mul_of_nonneg_left hfC (mul_nonneg (Real.rpow_nonneg hM _) (Real.rpow_nonneg hA _))145146#print axioms bounded_family_noise_max_sq_le147end PL1.EnfloBush148