PL1/EnfloMajorant.lean
All source files · Download exact source
SHA-256: a3be65b1cdd2d8b815301bb4c2681d4ea0ecd68e36535db027233389c91ea180
1import PL1.EnfloMaxMass2import Mathlib.MeasureTheory.Integral.Lebesgue.Add34/-! # A common integrable majorant for the dyadic images of any L1 operator56The sums of the absolute indicator images increase by dyadic refinement.7Their uniformly bounded integrals give a genuine integrable majorant by8monotone convergence, without assuming weak compactness of the operator.9-/1011noncomputable section12open MeasureTheory Filter13open scoped BigOperators ENNReal1415namespace PL1.EnfloBush1617theorem sum_range_double (f : ℕ → ℝ) (n : ℕ) :18 (∑ j ∈ Finset.range (2 * n), f j) =19 ∑ j ∈ Finset.range n, (f (2 * j) + f (2 * j + 1)) := by20 induction n with21 | zero => simp22 | succ n ih =>23 rw [Nat.mul_succ, Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ, ih]24 ring2526section General27variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}2829/-- Increasing nonnegative integrable functions with bounded integrals have30an actual real-valued integrable majorant, simultaneously almost everywhere. -/31theorem exists_integrable_majorant_of_monotone (f : ℕ → Ω → ℝ)32 (hf : ∀ n, Integrable (f n) μ) (hpos : ∀ n x, 0 ≤ f n x)33 (hmono : ∀ᵐ x ∂μ, Monotone (fun n => f n x)) {C : ℝ}34 (hb : ∀ n, ∫ x, f n x ∂μ ≤ C) :35 ∃ g : Ω → ℝ, Integrable g μ ∧ (∀ x, 0 ≤ g x) ∧ ∀ᵐ x ∂μ, ∀ n, f n x ≤ g x := by36 let F : Ω → ℝ≥0∞ := fun x => ⨆ n, ENNReal.ofReal (f n x)37 have hm (n : ℕ) : AEMeasurable (fun x => ENNReal.ofReal (f n x)) μ :=38 (hf n).aemeasurable.ennreal_ofReal39 have hF : AEMeasurable F μ := AEMeasurable.iSup hm40 have hFm : ∀ᵐ x ∂μ, Monotone (fun n => ENNReal.ofReal (f n x)) := by41 filter_upwards [hmono] with x hx42 exact fun n m hnm => ENNReal.ofReal_le_ofReal (hx hnm)43 have hI : (∫⁻ x, F x ∂μ) ≤ ENNReal.ofReal C := by44 rw [show (∫⁻ x, F x ∂μ) = ⨆ n, ∫⁻ x, ENNReal.ofReal (f n x) ∂μ from lintegral_iSup' hm hFm]45 apply iSup_le46 intro n47 rw [← ofReal_integral_eq_lintegral_ofReal (hf n) (Filter.Eventually.of_forall (hpos n))]48 exact ENNReal.ofReal_le_ofReal (hb n)49 have hIt : (∫⁻ x, F x ∂μ) ≠ ∞ := ne_top_of_le_ne_top ENNReal.ofReal_ne_top hI50 refine ⟨fun x => (F x).toReal, integrable_toReal_of_lintegral_ne_top hF hIt,51 fun x => ENNReal.toReal_nonneg, ?_⟩52 filter_upwards [ae_lt_top' hF hIt] with x hx53 intro n54 have h := ENNReal.toReal_mono hx.ne (le_iSup (fun n => ENNReal.ofReal (f n x)) n)55 simpa only [ENNReal.toReal_ofReal (hpos n x)] using h5657end General5859section Dyadic60open DyadicTrace61variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}6263def dyadicAbsSum (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) (x : Ω) : ℝ :=64 ∑ j ∈ Finset.range (2 ^ n), |T (dyadicVector (𝕜 := ℝ) n j) x|6566theorem dyadicAbsSum_nonneg (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) (x : Ω) :67 0 ≤ dyadicAbsSum T n x := Finset.sum_nonneg (fun _ _ => abs_nonneg _)6869theorem integrable_dyadicAbsSum (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) :70 Integrable (dyadicAbsSum T n) μ :=71 integrable_finsetSum _ (fun j _ => (L1.integrable_coeFn (T (dyadicVector n j))).abs)7273theorem integral_dyadicAbsSum (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) :74 (∫ x, dyadicAbsSum T n x ∂μ) = dyadicSumMass T n := by75 change (∫ x, ∑ j ∈ Finset.range (2 ^ n), |T (dyadicVector (𝕜 := ℝ) n j) x| ∂μ) = _76 rw [integral_finsetSum _ (fun j _ => (L1.integrable_coeFn (T (dyadicVector n j))).abs)]77 apply Finset.sum_congr rfl78 intro j _79 simpa only [Real.norm_eq_abs] using (L1.norm_eq_integral_norm (T (dyadicVector n j))).symm8081theorem dyadicAbsSum_le_succ_ae (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) (n : ℕ) :82 dyadicAbsSum T n ≤ᵐ[μ] dyadicAbsSum T (n + 1) := by83 filter_upwards [ae_all_iff.mpr (fun j => Lp.coeFn_add84 (T (dyadicVector (n + 1) (2 * j))) (T (dyadicVector (n + 1) (2 * j + 1))))] with x hx85 change (∑ j ∈ Finset.range (2 ^ n), |T (dyadicVector n j) x|) ≤86 ∑ j ∈ Finset.range (2 ^ (n + 1)), |T (dyadicVector (n + 1) j) x|87 rw [show 2 ^ (n + 1) = 2 * 2 ^ n by rw [pow_succ, Nat.mul_comm], sum_range_double]88 apply Finset.sum_le_sum89 intro j _90 rw [dyadicVector_refine, map_add, hx j, Pi.add_apply]91 exact abs_add_le _ _9293theorem dyadicAbsSum_monotone_ae (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) :94 ∀ᵐ x ∂μ, Monotone (fun n => dyadicAbsSum T n x) := by95 filter_upwards [ae_all_iff.mpr (dyadicAbsSum_le_succ_ae T)] with x hx96 exact monotone_nat_of_le_succ hx9798theorem dyadicSumMass_monotone (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) :99 Monotone (dyadicSumMass T) := by100 apply monotone_nat_of_le_succ101 intro n102 rw [← integral_dyadicAbsSum, ← integral_dyadicAbsSum]103 exact integral_mono_ae (integrable_dyadicAbsSum T n) (integrable_dyadicAbsSum T (n + 1))104 (dyadicAbsSum_le_succ_ae T n)105106/-- Every L1 operator has a common integrable bound for all its dyadic107absolute image sums, despite not necessarily being weakly compact. -/108theorem exists_dyadic_majorant (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) :109 ∃ g : Ω → ℝ, Integrable g μ ∧ (∀ x, 0 ≤ g x) ∧110 ∀ᵐ x ∂μ, ∀ n, dyadicAbsSum T n x ≤ g x :=111 exists_integrable_majorant_of_monotone (dyadicAbsSum T) (integrable_dyadicAbsSum T)112 (dyadicAbsSum_nonneg T) (dyadicAbsSum_monotone_ae T)113 (fun n => (integral_dyadicAbsSum T n).le.trans (dyadicSumMass_le T n))114115end Dyadic116117#print axioms exists_dyadic_majorant118end PL1.EnfloBush119