PL1/BonamiTwoPoint.lean
All source files · Download exact source
SHA-256: 52ee7d3106d97e0e643ad33922399c3108376cb4ff29f5a5d372f8a28d57929a
1import Mathlib.Analysis.Convex.SpecificFunctions.Basic2import Mathlib.Analysis.SpecialFunctions.Pow.Deriv3import Mathlib.Analysis.Calculus.Deriv.MeanValue4import Mathlib.Tactic.Linarith5import Mathlib.Tactic.Ring67/-! # The real two-point Bonami inequality89An elementary calculus proof of the scalar inequality used to tensorize10hypercontractivity. The second derivative estimate is reduced to AM–GM.11-/1213noncomputable section14open Set1516namespace PL1.BonamiTwoPoint1718private theorem negative_power_pair (x q : ℝ) (hx : -1 < x) (hx' : x < 1)19 (hq : q ≤ 0) : 2 ≤ (1 + x) ^ q + (1 - x) ^ q := by20 have hplus : 0 < 1 + x := by linarith21 have hminus : 0 < 1 - x := by linarith22 have hprod : 1 ≤ ((1 + x) * (1 - x)) ^ q :=23 Real.one_le_rpow_of_pos_of_le_one_of_nonpos (mul_pos hplus hminus)24 (by nlinarith [sq_nonneg x]) hq25 rw [Real.mul_rpow hplus.le hminus.le] at hprod26 have hp := Real.rpow_pos_of_pos hplus q27 have hm := Real.rpow_pos_of_pos hminus q28 nlinarith [sq_nonneg ((1 + x) ^ q - (1 - x) ^ q)]2930private def remainder (p x : ℝ) : ℝ :=31 ((1 + x) ^ p + (1 - x) ^ p) / 2 - 1 - p * (p - 1) / 2 * x ^ 23233private def remainderDeriv (p x : ℝ) : ℝ :=34 p / 2 * ((1 + x) ^ (p - 1) - (1 - x) ^ (p - 1)) - p * (p - 1) * x3536private theorem hasDerivAt_remainder (p x : ℝ) (hp : 1 ≤ p) :37 HasDerivAt (remainder p) (remainderDeriv p x) x := by38 have hplus := ((hasDerivAt_id x).const_add 1).rpow_const (Or.inr hp)39 have hminus := ((hasDerivAt_id x).const_sub 1).rpow_const (Or.inr hp)40 convert (((hplus.add hminus).div_const 2).sub_const 1).sub41 (((hasDerivAt_id x).pow 2).const_mul (p * (p - 1) / 2)) using 1 <;>42 first | rfl | (dsimp [remainder, remainderDeriv]; ring)4344private theorem hasDerivAt_remainderDeriv (p x : ℝ) (hx : -1 < x) (hx' : x < 1) :45 HasDerivAt (remainderDeriv p)46 (p * (p - 1) / 2 * ((1 + x) ^ (p - 2) + (1 - x) ^ (p - 2) - 2)) x := by47 have hplus := ((hasDerivAt_id x).const_add 1).rpow_const48 (p := p - 1) (Or.inl (by linarith : 1 + x ≠ 0))49 have hminus := ((hasDerivAt_id x).const_sub 1).rpow_const50 (p := p - 1) (Or.inl (by linarith : 1 - x ≠ 0))51 convert ((hplus.sub hminus).const_mul (p / 2)).sub52 ((hasDerivAt_id x).const_mul (p * (p - 1))) using 1 <;>53 first | rfl | (dsimp [remainderDeriv]; ring_nf)5455private theorem remainderDeriv_nonneg (p : ℝ) (hp : 1 ≤ p) (hp' : p ≤ 2)56 (x : ℝ) (hx : 0 ≤ x) (hx' : x < 1) : 0 ≤ remainderDeriv p x := by57 have hd : ∀ y ∈ Ioo (-1 : ℝ) 1,58 HasDerivAt (remainderDeriv p)59 (p * (p - 1) / 2 * ((1 + y) ^ (p - 2) + (1 - y) ^ (p - 2) - 2)) y :=60 fun y hy => hasDerivAt_remainderDeriv p y hy.1 hy.261 have hm : MonotoneOn (remainderDeriv p) (Ioo (-1 : ℝ) 1) := by62 apply monotoneOn_of_hasDerivWithinAt_nonneg (convex_Ioo _ _)63 (fun y hy => (hd y hy).continuousAt.continuousWithinAt)64 · intro y hy65 exact (hd y (by simpa only [interior_Ioo] using hy)).hasDerivWithinAt66 · intro y hy67 have hy' : y ∈ Ioo (-1 : ℝ) 1 := by simpa only [interior_Ioo] using hy68 exact mul_nonneg (by positivity) (sub_nonneg.mpr69 (negative_power_pair y (p - 2) hy'.1 hy'.2 (by linarith)))70 have h := hm (show (0 : ℝ) ∈ Ioo (-1 : ℝ) 1 by constructor <;> norm_num)71 (show x ∈ Ioo (-1 : ℝ) 1 by constructor <;> linarith) hx72 simpa [remainderDeriv] using h7374/-- Quadratic lower bound for the normalized two-point p-moment. -/75theorem normalized_moment_lower (p : ℝ) (hp : 1 ≤ p) (hp' : p ≤ 2)76 (x : ℝ) (hx : 0 ≤ x) (hx' : x ≤ 1) :77 1 + p * (p - 1) / 2 * x ^ 2 ≤ ((1 + x) ^ p + (1 - x) ^ p) / 2 := by78 have hm : MonotoneOn (remainder p) (Icc (0 : ℝ) 1) := by79 apply monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc _ _)80 (fun y _ => (hasDerivAt_remainder p y hp).continuousAt.continuousWithinAt)81 · intro y _82 exact (hasDerivAt_remainder p y hp).hasDerivWithinAt83 · intro y hy84 have hy' : y ∈ Ioo (0 : ℝ) 1 := by simpa only [interior_Icc] using hy85 exact remainderDeriv_nonneg p hp hp' y hy'.1.le hy'.286 have h := hm (show (0 : ℝ) ∈ Icc (0 : ℝ) 1 by constructor <;> norm_num)87 ⟨hx, hx'⟩ hx88 have h0 : remainder p 0 = 0 := by simp [remainder]89 rw [h0] at h90 dsimp [remainder] at h91 linarith9293/-- The sharp normalized real two-point Bonami inequality. -/94theorem normalized (p : ℝ) (hp : 1 ≤ p) (hp' : p ≤ 2)95 (x : ℝ) (hx : 0 ≤ x) (hx' : x ≤ 1) :96 1 + (p - 1) * x ^ 2 ≤ (((1 + x) ^ p + (1 - x) ^ p) / 2) ^ (2 / p) := by97 have hp0 : 0 < p := lt_of_lt_of_le zero_lt_one hp98 have hz : 0 ≤ p * (p - 1) / 2 * x ^ 2 := by positivity99 have hbernoulli := one_add_mul_self_le_rpow_one_add100 (s := p * (p - 1) / 2 * x ^ 2) (p := 2 / p) (by linarith)101 ((le_div_iff₀ hp0).mpr (by linarith))102 have heq : 1 + (2 / p) * (p * (p - 1) / 2 * x ^ 2) = 1 + (p - 1) * x ^ 2 := by103 field_simp104 rw [heq] at hbernoulli105 exact hbernoulli.trans (Real.rpow_le_rpow (by linarith)106 (normalized_moment_lower p hp hp' x hx hx') (by positivity))107108private theorem coefficient_ordered (p : ℝ) (hp : 1 ≤ p) (hp' : p ≤ 2)109 (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hba : b ≤ a) :110 a ^ 2 + (p - 1) * b ^ 2 ≤ ((|a + b| ^ p + |a - b| ^ p) / 2) ^ (2 / p) := by111 rcases eq_or_lt_of_le ha with rfl | ha112 · have hb0 : b = 0 := le_antisymm hba hb113 subst b114 simp [Real.zero_rpow (by linarith : p ≠ 0),115 Real.zero_rpow (by positivity : 2 / p ≠ 0)]116 have hx : 0 ≤ b / a := div_nonneg hb ha.le117 have hx' : b / a ≤ 1 := (div_le_one ha).mpr hba118 have h := mul_le_mul_of_nonneg_left (normalized p hp hp' (b / a) hx hx')119 (sq_nonneg a)120 have heqplus : a + b = a * (1 + b / a) := by field_simp121 have heqminus : a - b = a * (1 - b / a) := by field_simp122 have hmoment : (|a + b| ^ p + |a - b| ^ p) / 2 =123 a ^ p * (((1 + b / a) ^ p + (1 - b / a) ^ p) / 2) := by124 rw [abs_of_nonneg (add_nonneg ha.le hb), abs_of_nonneg (sub_nonneg.mpr hba),125 heqplus, heqminus, Real.mul_rpow ha.le (by linarith),126 Real.mul_rpow ha.le (by linarith)]127 ring128 rw [hmoment, Real.mul_rpow (Real.rpow_nonneg ha.le p) (by positivity),129 ← Real.rpow_mul ha.le, show p * (2 / p) = (2 : ℝ) by field_simp,130 Real.rpow_two]131 convert h using 1 <;> first | rfl | field_simp132133private theorem coefficient_nonneg (p : ℝ) (hp : 1 ≤ p) (hp' : p ≤ 2)134 (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) :135 a ^ 2 + (p - 1) * b ^ 2 ≤ ((|a + b| ^ p + |a - b| ^ p) / 2) ^ (2 / p) := by136 rcases le_total b a with hba | hab137 · exact coefficient_ordered p hp hp' a b ha hb hba138 · have h := coefficient_ordered p hp hp' b a hb ha hab139 rw [add_comm b a, abs_sub_comm b a] at h140 have hs : a ^ 2 ≤ b ^ 2 := by nlinarith141 have hc := mul_nonneg (show 0 ≤ 2 - p by linarith) (sub_nonneg.mpr hs)142 nlinarith143144private theorem abs_moment (p a b : ℝ) :145 |(|a| + |b|)| ^ p + |(|a| - |b|)| ^ p = |a + b| ^ p + |a - b| ^ p := by146 rcases le_total 0 a with ha | ha <;> rcases le_total 0 b with hb | hb147 · simp only [abs_of_nonneg ha, abs_of_nonneg hb]148 · simp only [abs_of_nonneg ha, abs_of_nonpos hb, sub_neg_eq_add, ← sub_eq_add_neg]149 ring150 · simp only [abs_of_nonpos ha, abs_of_nonneg hb]151 rw [show -a + b = -(a - b) by ring, show -a - b = -(a + b) by ring,152 abs_neg, abs_neg]153 ring154 · simp only [abs_of_nonpos ha, abs_of_nonpos hb]155 rw [show -a + -b = -(a + b) by ring, show -a - -b = -(a - b) by ring,156 abs_neg, abs_neg]157158/-- Sharp coefficient form of the real two-point Bonami inequality. -/159theorem coefficient (p : ℝ) (hp : 1 ≤ p) (hp' : p ≤ 2) (a b : ℝ) :160 a ^ 2 + (p - 1) * b ^ 2 ≤ ((|a + b| ^ p + |a - b| ^ p) / 2) ^ (2 / p) := by161 have h := coefficient_nonneg p hp hp' |a| |b| (abs_nonneg a) (abs_nonneg b)162 rwa [abs_moment, sq_abs, sq_abs] at h163164/-- Noise coefficient form, allowing either sign of rho. -/165theorem noise_coefficient (p ρ : ℝ) (hp : 1 ≤ p) (hp' : p ≤ 2)166 (hρ : ρ ^ 2 ≤ p - 1) (a b : ℝ) :167 a ^ 2 + (ρ * b) ^ 2 ≤ ((|a + b| ^ p + |a - b| ^ p) / 2) ^ (2 / p) := by168 have h := coefficient p hp hp' a b169 have hc := mul_le_mul_of_nonneg_right hρ (sq_nonneg b)170 nlinarith171172/-- Moment form used directly by finite-product tensorization. -/173theorem noise_moment (p ρ : ℝ) (hp : 1 ≤ p) (hp' : p ≤ 2)174 (hρ : ρ ^ 2 ≤ p - 1) (a b : ℝ) :175 (a ^ 2 + (ρ * b) ^ 2) ^ (p / 2) ≤ (|a + b| ^ p + |a - b| ^ p) / 2 := by176 have hp0 : 0 < p := lt_of_lt_of_le zero_lt_one hp177 have h := Real.rpow_le_rpow (by positivity) (noise_coefficient p ρ hp hp' hρ a b)178 (show 0 ≤ p / 2 by positivity)179 rwa [← Real.rpow_mul (by positivity), show (2 / p) * (p / 2) = (1 : ℝ) by field_simp,180 Real.rpow_one] at h181182#print axioms coefficient183#print axioms noise_moment184185end PL1.BonamiTwoPoint186