PL1/EnfloMaxMass.lean
All source files · Download exact source
SHA-256: 6b47acb203c0eb944019da79fdcb1bc3f0563a7fa00ac2770441d3911404a6db
1import PL1.EnfloBush23/-! # Actual finite maxima and their dyadic operator seminorms -/45noncomputable section6open MeasureTheory Filter7open scoped BigOperators Topology89namespace PL1.EnfloBush1011theorem maxAbs_le {n : ℕ} {a : ℕ → ℝ} {M : ℝ} (hM : 0 ≤ M)12 (h : ∀ j < n, |a j| ≤ M) : maxAbs n a ≤ M := by13 induction n with14 | zero => exact hM15 | succ n ih => exact max_le (ih (fun j hj => h j (Nat.lt_succ_of_lt hj))) (h n (Nat.lt_succ_self n))1617theorem maxAbs_le_sum (n : ℕ) (a : ℕ → ℝ) :18 maxAbs n a ≤ ∑ j ∈ Finset.range n, |a j| :=19 maxAbs_le (Finset.sum_nonneg (fun _ _ => abs_nonneg _))20 (fun _j hj => Finset.single_le_sum (f := fun i => |a i|) (fun _ _ => abs_nonneg _) (Finset.mem_range.mpr hj))2122theorem maxAbs_add_le (n : ℕ) (a b : ℕ → ℝ) :23 maxAbs n (fun j => a j + b j) ≤ maxAbs n a + maxAbs n b := by24 apply maxAbs_le (add_nonneg (maxAbs_nonneg n a) (maxAbs_nonneg n b))25 intro j hj26 exact (abs_add_le _ _).trans (add_le_add (abs_le_maxAbs a hj) (abs_le_maxAbs b hj))2728theorem maxAbs_congr {n : ℕ} {a b : ℕ → ℝ} (h : ∀ j < n, a j = b j) :29 maxAbs n a = maxAbs n b := by30 apply le_antisymm31 · apply maxAbs_le (maxAbs_nonneg n b)32 intro j hj33 rw [h j hj]34 exact abs_le_maxAbs b hj35 · apply maxAbs_le (maxAbs_nonneg n a)36 intro j hj37 rw [← h j hj]38 exact abs_le_maxAbs a hj3940section General41variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}4243def maxMass (n : ℕ) (f : ℕ → Lp ℝ 1 μ) : ℝ :=44 ∫ x, maxAbs n (fun j => f j x) ∂μ4546theorem maxMass_nonneg (n : ℕ) (f : ℕ → Lp ℝ 1 μ) : 0 ≤ maxMass n f :=47 integral_nonneg (fun _ => maxAbs_nonneg n _)4849theorem maxMass_le_sum_norm (n : ℕ) (f : ℕ → Lp ℝ 1 μ) :50 maxMass n f ≤ ∑ j ∈ Finset.range n, ‖f j‖ := by51 have h := integral_mono (integrable_maxAbs n f)52 (integrable_finsetSum _ (fun j _ => (L1.integrable_coeFn (f j)).abs))53 (fun x => maxAbs_le_sum n (fun j => f j x))54 rw [integral_finsetSum _ (fun j _ => (L1.integrable_coeFn (f j)).abs)] at h55 have he (j : ℕ) : (∫ x, |f j x| ∂μ) = ‖f j‖ := by56 simpa only [Real.norm_eq_abs] using (L1.norm_eq_integral_norm (f j)).symm57 simpa only [maxMass, he] using h5859theorem maxMass_add_le (n : ℕ) (f g : ℕ → Lp ℝ 1 μ) :60 maxMass n (fun j => f j + g j) ≤ maxMass n f + maxMass n g := by61 rw [maxMass, maxMass, maxMass, ← integral_add (integrable_maxAbs n f) (integrable_maxAbs n g)]62 apply integral_mono_ae (integrable_maxAbs n _) ((integrable_maxAbs n f).add (integrable_maxAbs n g))63 filter_upwards [ae_all_iff.mpr (fun j => Lp.coeFn_add (f j) (g j))] with x hx64 simpa only [hx, Pi.add_apply] using maxAbs_add_le n (fun j => f j x) (fun j => g j x)6566theorem maxMass_le_add_sum_norm_sub (n : ℕ) (f g : ℕ → Lp ℝ 1 μ) :67 maxMass n f ≤ maxMass n g + ∑ j ∈ Finset.range n, ‖f j - g j‖ := by68 have h := maxMass_add_le n g (fun j => f j - g j)69 simp only [add_sub_cancel] at h70 exact h.trans (add_le_add le_rfl (maxMass_le_sum_norm n (fun j => f j - g j)))7172end General7374section Dyadic75open DyadicTrace76variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}7778def dyadicSumMass (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) : ℝ :=79 ∑ j ∈ Finset.range (2 ^ n), ‖T (dyadicVector (𝕜 := ℝ) n j)‖8081def dyadicMaxMass (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) : ℝ :=82 maxMass (2 ^ n) (fun j => T (dyadicVector (𝕜 := ℝ) n j))8384theorem dyadicSumMass_nonneg (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) :85 0 ≤ dyadicSumMass T n := Finset.sum_nonneg (fun _ _ => norm_nonneg _)8687theorem dyadicSumMass_le (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) :88 dyadicSumMass T n ≤ ‖T‖ := by89 calc90 _ ≤ ∑ j ∈ Finset.range (2 ^ n), ‖T‖ * ‖dyadicVector (𝕜 := ℝ) n j‖ :=91 Finset.sum_le_sum (fun j _ => T.le_opNorm _)92 _ = ‖T‖ := by rw [← Finset.mul_sum, sum_norm_dyadicVector, mul_one]9394theorem dyadicMaxMass_nonneg (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) :95 0 ≤ dyadicMaxMass T n := maxMass_nonneg _ _9697theorem dyadicMaxMass_le_sum (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) :98 dyadicMaxMass T n ≤ dyadicSumMass T n := maxMass_le_sum_norm _ _99100theorem dyadicMaxMass_le (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) :101 dyadicMaxMass T n ≤ ‖T‖ := (dyadicMaxMass_le_sum T n).trans (dyadicSumMass_le T n)102103theorem dyadicMaxMass_le_add_norm_sub (T S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) :104 dyadicMaxMass T n ≤ dyadicMaxMass S n + ‖T - S‖ := by105 have h := maxMass_le_add_sum_norm_sub (2 ^ n) (fun j => T (dyadicVector n j))106 (fun j => S (dyadicVector n j))107 exact h.trans (add_le_add le_rfl (dyadicSumMass_le (T - S) n))108109def DyadicVanishing (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) : Prop :=110 Tendsto (dyadicMaxMass T) atTop (𝓝 0)111112theorem not_boundedBelow_of_dyadicVanishing {T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ}113 (h : DyadicVanishing T) {c : ℝ} (hc : 0 < c)114 (hlower : ∀ f : IntervalL1 ℝ, c * ‖f‖ ≤ ‖T f‖) : False := by115 have he : Tendsto (fun n => dyadicMaxMass T n * ‖T‖) atTop (𝓝 0) := by116 simpa only [zero_mul] using h.mul_const ‖T‖117 have hle : c ^ 2 ≤ 0 := ge_of_tendsto he (Filter.Eventually.of_forall118 (fun n => dyadic_max_integral_mul_norm T hc.le hlower n))119 nlinarith120121end Dyadic122123#print axioms not_boundedBelow_of_dyadicVanishing124end PL1.EnfloBush125