PL1/EnfloBush.lean
All source files · Download exact source
SHA-256: 0b5b30eae3cad64dc9cddfcbcb822cac1c0697dc4940bad196588f88e4333070
1import PL1.FiniteRademacherClipping2import PL1.EnfloStarbirdDyadic3import PL1.DyadicCellMeasure45/-! # A positive dyadic bush from an actual bounded-below L1 embedding67The finite sign averages and the integrals in this file use actual functions8and actual L1 vectors. No Enflo extraction or moment estimate is assumed.9-/1011noncomputable section12open MeasureTheory13open scoped BigOperators1415namespace PL1.EnfloBush16open Bonami FiniteRademacherClipping1718theorem average_sq_le (n : ℕ) (f : Cube n → ℝ) :19 (average n f) ^ 2 ≤ average n (fun x => f x ^ 2) := by20 induction n with21 | zero => rfl22 | succ n ih =>23 have h₀ := ih (fun x => f (false, x))24 have h₁ := ih (fun x => f (true, x))25 change ((average n (fun x => f (false, x)) + average n (fun x => f (true, x))) / 2) ^ 2 ≤ _26 change _ ≤ (average n (fun x => f (false, x) ^ 2) + average n (fun x => f (true, x) ^ 2)) / 227 nlinarith [sq_nonneg (average n (fun x => f (false, x)) - average n (fun x => f (true, x)))]2829theorem rademacher_abs_average_sq_le (n : ℕ) (a : ℕ → ℝ) :30 (average n (fun x => |rademacherSum n a x|)) ^ 2 ≤ energy n a := by31 have h := average_sq_le n (fun x => |rademacherSum n a x|)32 simpa only [sq_abs, second_moment] using h3334def maxAbs : ℕ → (ℕ → ℝ) → ℝ35 | 0, _ => 036 | n + 1, a => max (maxAbs n a) |a n|3738theorem maxAbs_nonneg (n : ℕ) (a : ℕ → ℝ) : 0 ≤ maxAbs n a := by39 cases n with40 | zero => rfl41 | succ n => exact (abs_nonneg _).trans (le_max_right _ _)4243theorem abs_le_maxAbs {n j : ℕ} (a : ℕ → ℝ) (hj : j < n) : |a j| ≤ maxAbs n a := by44 induction n with45 | zero => omega46 | succ n ih =>47 by_cases h : j < n48 · exact (ih h).trans (le_max_left _ _)49 · have he : j = n := by omega50 subst j51 exact le_max_right _ _5253theorem energy_le_maxAbs_mul_sum (n : ℕ) (a : ℕ → ℝ) :54 energy n a ≤ maxAbs n a * ∑ j ∈ Finset.range n, |a j| := by55 rw [Finset.mul_sum]56 apply Finset.sum_le_sum57 intro j hj58 calc59 (a j) ^ 2 = |a j| * |a j| := by rw [← sq, sq_abs]60 _ ≤ _ := mul_le_mul_of_nonneg_right (abs_le_maxAbs a (Finset.mem_range.mp hj)) (abs_nonneg _)6162theorem quadratic_young {A U V : ℝ} (hU : 0 ≤ U) (hV : 0 ≤ V)63 (hA : A ^ 2 ≤ U * V) (k : ℝ) : 2 * k * A ≤ k ^ 2 * U + V := by64 by_cases hU0 : U = 065 · have hA0 : A = 0 := by rw [hU0, zero_mul] at hA; nlinarith [sq_nonneg A]66 simp only [hA0, hU0, mul_zero, zero_add]67 exact hV68 · have hUp : 0 < U := lt_of_le_of_ne hU (Ne.symm hU0)69 apply (mul_le_mul_iff_right₀ hUp).mp70 nlinarith [sq_nonneg (k * U - A)]7172theorem rademacher_abs_average_young (n : ℕ) (a : ℕ → ℝ) (k : ℝ) :73 2 * k * average n (fun x => |rademacherSum n a x|) ≤74 k ^ 2 * maxAbs n a + ∑ j ∈ Finset.range n, |a j| :=75 quadratic_young (maxAbs_nonneg n a) (Finset.sum_nonneg (fun _ _ => abs_nonneg _))76 ((rademacher_abs_average_sq_le n a).trans (energy_le_maxAbs_mul_sum n a)) k7778theorem square_le_mul_of_quadratic {c U V : ℝ} (hc : 0 ≤ c) (hU : 0 ≤ U) (hV : 0 ≤ V)79 (h : ∀ k : ℝ, 0 ≤ k → 2 * k * c ≤ k ^ 2 * U + V) : c ^ 2 ≤ U * V := by80 by_cases hc0 : c = 081 · simpa only [hc0, zero_pow (by norm_num : 2 ≠ 0)] using mul_nonneg hU hV82 have hcp : 0 < c := lt_of_le_of_ne hc (Ne.symm hc0)83 by_cases hU0 : U = 084 · have hh := h ((V + 1) / c) (div_nonneg (by linarith) hc)85 rw [hU0, mul_zero, zero_add] at hh86 have he : ((V + 1) / c) * c = V + 1 := div_mul_cancel₀ _ hc087 nlinarith88 · have hUp : 0 < U := lt_of_le_of_ne hU (Ne.symm hU0)89 have hh := mul_le_mul_of_nonneg_left (h (c / U) (div_nonneg hc hU)) hU90 have he : U * (c / U) = c := mul_div_cancel₀ c hU091 have he2 := congrArg (fun z : ℝ => z ^ 2) he92 nlinarith9394def signAt : (n : ℕ) → Cube n → ℕ → ℝ95 | 0, _, _ => 196 | n + 1, (b, x), j => if j = n then (if b then -1 else 1) else signAt n x j9798theorem abs_signAt (n : ℕ) (b : Cube n) (j : ℕ) : |signAt n b j| = 1 := by99 induction n with100 | zero => norm_num [signAt]101 | succ n ih =>102 obtain ⟨b, x⟩ := b103 by_cases hj : j = n104 · subst j105 cases b <;> norm_num [signAt]106 · simpa only [signAt, ite_eq_right hj] using ih x107108section Integral109variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}110111theorem integrable_average (n : ℕ) (f : Cube n → Ω → ℝ)112 (hf : ∀ b, Integrable (f b) μ) : Integrable (fun x => average n (fun b => f b x)) μ := by113 induction n with114 | zero => exact hf ()115 | succ n ih =>116 exact ((ih (fun b => f (false, b)) (fun b => hf (false, b))).add117 (ih (fun b => f (true, b)) (fun b => hf (true, b)))).div_const 2118119theorem integral_average (n : ℕ) (f : Cube n → Ω → ℝ)120 (hf : ∀ b, Integrable (f b) μ) :121 (∫ x, average n (fun b => f b x) ∂μ) = average n (fun b => ∫ x, f b x ∂μ) := by122 induction n with123 | zero => rfl124 | succ n ih =>125 change (∫ x, (average n (fun b => f (false, b) x) + average n (fun b => f (true, b) x)) / 2 ∂μ) = _126 rw [integral_div, integral_add127 (integrable_average n _ (fun b => hf (false, b)))128 (integrable_average n _ (fun b => hf (true, b))), ih _ (fun b => hf (false, b)),129 ih _ (fun b => hf (true, b))]130 rfl131132def signedSum : (n : ℕ) → (ℕ → Lp ℝ 1 μ) → Cube n → Lp ℝ 1 μ133 | 0, _, _ => 0134 | n + 1, f, (b, x) => (if b then -f n else f n) + signedSum n f x135136theorem signedSum_coe (n : ℕ) (f : ℕ → Lp ℝ 1 μ) (b : Cube n) :137 signedSum n f b =ᵐ[μ] (fun x => rademacherSum n (fun j => f j x) b) := by138 induction n with139 | zero => exact Lp.coeFn_zero _ _ _140 | succ n ih =>141 obtain ⟨b, y⟩ := b142 cases b143 · filter_upwards [Lp.coeFn_add (f n) (signedSum n f y), ih y] with x hx hy144 simpa only [signedSum, rademacherSum, Bool.false_eq_true, ite_false, Pi.add_apply, hy] using hx145 · filter_upwards [Lp.coeFn_add (-f n) (signedSum n f y), Lp.coeFn_neg (f n), ih y] with x hx hn hy146 simpa only [signedSum, rademacherSum, ite_true, Pi.add_apply, Pi.neg_apply, hn, hy] using hx147148theorem signedSum_eq_sum (n : ℕ) (f : ℕ → Lp ℝ 1 μ) (b : Cube n) :149 signedSum n f b = ∑ j ∈ Finset.range n, signAt n b j • f j := by150 induction n with151 | zero => simp [signedSum]152 | succ n ih =>153 obtain ⟨b, y⟩ := b154 rw [Finset.sum_range_succ]155 have hs : (∑ j ∈ Finset.range n, signAt (n + 1) (b, y) j • f j) =156 ∑ j ∈ Finset.range n, signAt n y j • f j := by157 apply Finset.sum_congr rfl158 intro j hj159 simp only [signAt, ite_eq_right (Nat.ne_of_lt (Finset.mem_range.mp hj))]160 rw [hs, ← ih y]161 cases b <;> simp [signedSum, signAt, add_comm]162163theorem signedSum_map {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]164 (T : E →L[ℝ] Lp ℝ 1 μ) (n : ℕ) (f : ℕ → E) (b : Cube n) :165 signedSum n (fun j => T (f j)) b = T (∑ j ∈ Finset.range n, signAt n b j • f j) := by166 rw [signedSum_eq_sum, map_sum]167 simp only [map_smul]168169theorem integrable_rademacher (n : ℕ) (f : ℕ → Lp ℝ 1 μ) (b : Cube n) :170 Integrable (fun x => rademacherSum n (fun j => f j x) b) μ :=171 (L1.integrable_coeFn (signedSum n f b)).congr (signedSum_coe n f b)172173theorem norm_signedSum (n : ℕ) (f : ℕ → Lp ℝ 1 μ) (b : Cube n) :174 ‖signedSum n f b‖ = ∫ x, |rademacherSum n (fun j => f j x) b| ∂μ := by175 rw [L1.norm_eq_integral_norm]176 apply integral_congr_ae177 filter_upwards [signedSum_coe n f b] with x hx178 rw [hx, Real.norm_eq_abs]179180theorem integrable_maxAbs (n : ℕ) (f : ℕ → Lp ℝ 1 μ) :181 Integrable (fun x => maxAbs n (fun j => f j x)) μ := by182 induction n with183 | zero => exact integrable_zero _ _ _184 | succ n ih => exact ih.sup (L1.integrable_coeFn (f n)).abs185186theorem signed_norm_average_young (n : ℕ) (f : ℕ → Lp ℝ 1 μ) (k : ℝ) :187 2 * k * average n (fun b => ‖signedSum n f b‖) ≤188 k ^ 2 * (∫ x, maxAbs n (fun j => f j x) ∂μ) + ∑ j ∈ Finset.range n, ‖f j‖ := by189 have hi : Integrable (fun x => average n (fun b => |rademacherSum n (fun j => f j x) b|)) μ :=190 integrable_average n _ (fun b => (integrable_rademacher n f b).abs)191 have h := integral_mono (hi.const_mul (2 * k))192 (((integrable_maxAbs n f).const_mul (k ^ 2)).add193 (integrable_finsetSum _ (fun j _ => (L1.integrable_coeFn (f j)).abs)))194 (fun x => rademacher_abs_average_young n (fun j => f j x) k)195 simp only [Pi.add_apply] at h196 rw [integral_const_mul, integral_add ((integrable_maxAbs n f).const_mul (k ^ 2))197 (integrable_finsetSum _ (fun j _ => (L1.integrable_coeFn (f j)).abs)), integral_const_mul,198 integral_finsetSum _ (fun j _ => (L1.integrable_coeFn (f j)).abs), integral_average n _199 (fun b => (integrable_rademacher n f b).abs)] at h200 simp_rw [← norm_signedSum n f] at h201 have hn (j : ℕ) : (∫ x, |f j x| ∂μ) = ‖f j‖ := by202 simpa only [Real.norm_eq_abs] using (L1.norm_eq_integral_norm (f j)).symm203 simpa only [hn] using h204205theorem lower_signed_norm_sq_le (n : ℕ) (f : ℕ → Lp ℝ 1 μ) {c : ℝ} (hc : 0 ≤ c)206 (hlower : ∀ b : Cube n, c ≤ ‖signedSum n f b‖) :207 c ^ 2 ≤ (∫ x, maxAbs n (fun j => f j x) ∂μ) * ∑ j ∈ Finset.range n, ‖f j‖ := by208 apply square_le_mul_of_quadratic hc (integral_nonneg (fun x => maxAbs_nonneg n _))209 (Finset.sum_nonneg (fun _ _ => norm_nonneg _))210 intro k hk211 have ha : c ≤ average n (fun b => ‖signedSum n f b‖) := by212 simpa only [average_const] using average_mono n hlower213 exact (mul_le_mul_of_nonneg_left ha (by positivity : 0 ≤ 2 * k)).trans214 (signed_norm_average_young n f k)215216end Integral217218section Dyadic219open DyadicTrace220attribute [local instance] intervalMeasure_probability221222theorem norm_dyadic_signed_step (n m : ℕ) (b : Cube m) :223 ‖step (𝕜 := ℝ) n (signAt m b)‖ = 1 := by224 rw [L1.norm_eq_integral_norm]225 calc226 _ = ∫ _ : ℝ, (1 : ℝ) ∂intervalMeasure := by227 apply integral_congr_ae228 filter_upwards [coeFn_step (𝕜 := ℝ) n (signAt m b)] with x hx229 rw [hx, Real.norm_eq_abs, abs_signAt]230 _ = 1 := by simp231232theorem sum_norm_dyadicVector (n : ℕ) :233 (∑ j ∈ Finset.range (2 ^ n), ‖dyadicVector (𝕜 := ℝ) n j‖) = 1 := by234 have he (j : ℕ) (hj : j ∈ Finset.range (2 ^ n)) :235 ‖dyadicVector (𝕜 := ℝ) n j‖ = ((2 : ℝ) ^ n)⁻¹ := by236 rw [PartitionAverages.norm_vector]237 exact intervalMeasure_cell_toReal n j (Finset.mem_range.mp hj)238 rw [Finset.sum_congr rfl he]239 simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, Nat.cast_pow, Nat.cast_ofNat]240 exact mul_inv_cancel₀ (pow_ne_zero n (by norm_num : (2 : ℝ) ≠ 0))241242variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}243244/-- Uniform lower bound for the pointwise maximum of actual dyadic indicator images.245The source is the genuine probability interval and the codomain can be any L1 space. -/246theorem dyadic_max_integral_mul_norm (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ)247 {c : ℝ} (hc : 0 ≤ c) (hT : ∀ f : IntervalL1 ℝ, c * ‖f‖ ≤ ‖T f‖) (n : ℕ) :248 c ^ 2 ≤ (∫ x, maxAbs (2 ^ n) (fun j => T (dyadicVector (𝕜 := ℝ) n j) x) ∂μ) * ‖T‖ := by249 have hl (b : Cube (2 ^ n)) : c ≤ ‖signedSum (2 ^ n) (fun j => T (dyadicVector n j)) b‖ := by250 rw [signedSum_map]251 change c ≤ ‖T (step n (signAt (2 ^ n) b))‖252 have h := hT (step n (signAt (2 ^ n) b))253 simpa only [norm_dyadic_signed_step, mul_one] using h254 have h := lower_signed_norm_sq_le (2 ^ n) (fun j => T (dyadicVector n j)) hc hl255 apply h.trans256 apply mul_le_mul_of_nonneg_left _ (integral_nonneg (fun x => maxAbs_nonneg _ _))257 calc258 _ ≤ ∑ j ∈ Finset.range (2 ^ n), ‖T‖ * ‖dyadicVector (𝕜 := ℝ) n j‖ :=259 Finset.sum_le_sum (fun j _ => T.le_opNorm _)260 _ = ‖T‖ := by rw [← Finset.mul_sum, sum_norm_dyadicVector, mul_one]261262end Dyadic263264#print axioms dyadic_max_integral_mul_norm265end PL1.EnfloBush266