From 99b555cd1df6b2cc341a03caab6851d9085d1f77 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 25 Jun 2024 14:10:44 +0200 Subject: [PATCH] push new files --- Carleson/RealInterpolation.lean | 56 +++++++++++++ Carleson/WeakType.lean | 143 ++++++++++++++++++++++++++++++++ 2 files changed, 199 insertions(+) create mode 100644 Carleson/RealInterpolation.lean create mode 100644 Carleson/WeakType.lean diff --git a/Carleson/RealInterpolation.lean b/Carleson/RealInterpolation.lean new file mode 100644 index 00000000..988b49fc --- /dev/null +++ b/Carleson/RealInterpolation.lean @@ -0,0 +1,56 @@ +import Carleson.WeakType + +noncomputable section + +open NNReal ENNReal NormedSpace MeasureTheory Set + +variable {α α' E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m : MeasurableSpace α'} + {p p' q : ℝ≥0∞} {c : ℝ≥0} + {μ : Measure α} {ν : Measure α'} [NontriviallyNormedField ℝ] + [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] + [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] [FiniteDimensional ℝ E₁] + [NormedAddCommGroup E₂] [NormedSpace ℝ E₂] [FiniteDimensional ℝ E₂] + [NormedAddCommGroup E₃] [NormedSpace ℝ E₃] [FiniteDimensional ℝ E₃] + [MeasurableSpace E] [BorelSpace E] + [MeasurableSpace E₁] [BorelSpace E₁] + [MeasurableSpace E₂] [BorelSpace E₂] + [MeasurableSpace E₃] [BorelSpace E₃] + (L : E₁ →L[ℝ] E₂ →L[ℝ] E₃) + {f g : α → E} {t : ℝ} {s x y : ℝ≥0∞} + {T : (α → E₁) → (α' → E₂)} + + +namespace MeasureTheory + +/-- The `t`-truncation of a function `f`. -/ +def trunc (f : α → E) (t : ℝ) (x : α) : E := if ‖f x‖ ≤ t then f x else 0 + +lemma aestronglyMeasurable_trunc (hf : AEStronglyMeasurable f μ) : + AEStronglyMeasurable (trunc f t) μ := sorry + +/-- The `t`-truncation of `f : α →ₘ[μ] E`. -/ +def AEEqFun.trunc (f : α →ₘ[μ] E) (t : ℝ) : α →ₘ[μ] E := + AEEqFun.mk (MeasureTheory.trunc f t) (aestronglyMeasurable_trunc f.aestronglyMeasurable) + +-- /-- A set of measurable functions is closed under truncation. -/ +-- class IsClosedUnderTruncation (U : Set (α →ₘ[μ] E)) : Prop where +-- trunc_mem {f : α →ₘ[μ] E} (hf : f ∈ U) (t : ℝ) : f.trunc t ∈ U + +def Subadditive (T : (α → E₁) → α' → E₂) : Prop := + ∃ A > 0, ∀ (f g : α → E₁) (x : α'), ‖T (f + g) x‖ ≤ A * (‖T f x‖ + ‖T g x‖) + +def Sublinear (T : (α → E₁) → α' → E₂) : Prop := + Subadditive T ∧ ∀ (f : α → E₁) (c : ℝ), T (c • f) = c • T f + +/-- Marcinkiewicz real interpolation theorem. -/ +-- feel free to assume that T also respect a.e.-equality. +theorem exists_lnorm_le_of_subadditive_of_lbounded {p₀ p₁ q₀ q₁ p q : ℝ≥0∞} + (hp₀ : p₀ ∈ Icc 1 q₀) (hp₁ : p₁ ∈ Icc 1 q₁) (hq : q₀ ≠ q₁) + {C₀ C₁ t : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) + (hp : p⁻¹ = (1 - t) / p₀ + t / p₁) (hq : q⁻¹ = (1 - t) / q₀ + t / q₁) + (hT : Sublinear T) (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (h₁T : HasWeakType T p₁ q₁ μ ν C₁) : + ∃ C > 0, HasStrongType T p p μ ν C := sorry + +/- State and prove Remark 1.2.7 -/ + +end MeasureTheory diff --git a/Carleson/WeakType.lean b/Carleson/WeakType.lean new file mode 100644 index 00000000..129dbd8e --- /dev/null +++ b/Carleson/WeakType.lean @@ -0,0 +1,143 @@ +import Mathlib.MeasureTheory.Integral.MeanInequalities +import Mathlib.MeasureTheory.Integral.Layercake +import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar +import Mathlib.Analysis.NormedSpace.Dual +import Mathlib.Analysis.NormedSpace.LinearIsometry + +noncomputable section + +open NNReal ENNReal NormedSpace MeasureTheory Set Filter Topology Function + +variable {α α' 𝕜 E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m : MeasurableSpace α'} + {p p' q : ℝ≥0∞} {c : ℝ≥0} + {μ : Measure α} {ν : Measure α'} [NontriviallyNormedField 𝕜] + [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] + [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [FiniteDimensional 𝕜 E₁] + [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] [FiniteDimensional 𝕜 E₂] + [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] [FiniteDimensional 𝕜 E₃] + [MeasurableSpace E] [BorelSpace E] + [MeasurableSpace E₁] [BorelSpace E₁] + [MeasurableSpace E₂] [BorelSpace E₂] + [MeasurableSpace E₃] [BorelSpace E₃] + (L : E₁ →L[𝕜] E₂ →L[𝕜] E₃) + {f g : α → E} (hf : AEMeasurable f) {t s x y : ℝ≥0∞} + {T : (α → E₁) → (α' → E₂)} + +#check meas_ge_le_mul_pow_snorm -- Chebyshev's inequality + +namespace MeasureTheory +/- If we need more properties of `E`, we can add `[RCLike E]` *instead of* the above type-classes-/ +#check _root_.RCLike + +/-! # The distribution function `d_f` -/ + +/-- The distribution function of a function `f`. +Note that unlike the notes, we also define this for `t = ∞`. +Note: we also want to use this for functions with codomain `ℝ≥0∞`, but for those we just write +`μ { x | t < f x }` -/ +def distribution [NNNorm E] (f : α → E) (t : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ := + μ { x | t < ‖f x‖₊ } + +@[gcongr] lemma distribution_mono_left (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) : + distribution f t μ ≤ distribution g t μ := sorry + +@[gcongr] lemma distribution_mono_right (h : t ≤ s) : + distribution f s μ ≤ distribution f t μ := sorry + +@[gcongr] lemma distribution_mono (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) (h : t ≤ s) : + distribution f s μ ≤ distribution g t μ := sorry + +lemma distribution_smul_left {c : 𝕜} (hc : c ≠ 0) : + distribution (c • f) t μ = distribution f (t / ‖c‖₊) μ := sorry + +lemma distribution_add_le : + distribution (f + g) (t + s) μ ≤ distribution f t μ + distribution g s μ := sorry + +lemma _root_.ContinuousLinearMap.distribution_le {f : α → E₁} {g : α → E₂} : + distribution (fun x ↦ L (f x) (g x)) (‖L‖₊ * t * s) μ ≤ + distribution f t μ + distribution g s μ := sorry + + +/- A version of the layer-cake theorem already exists, but the need the versions below. -/ +#check MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul + +/-- The layer-cake theorem, or Cavalieri's principle for functions into `ℝ≥0∞` -/ +lemma lintegral_norm_pow_eq_measure_lt {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) + {p : ℝ} (hp : 1 ≤ p) : + ∫⁻ x, (f x) ^ p ∂μ = + ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (p * t ^ (p - 1)) * μ { x | ENNReal.ofReal t < f x } := by + sorry + +/-- The layer-cake theorem, or Cavalieri's principle for functions into a normed group. -/ +lemma lintegral_norm_pow_eq_distribution {p : ℝ} (hp : 1 ≤ p) : + ∫⁻ x, ‖f x‖₊ ^ p ∂μ = + ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (p * t ^ (p - 1)) * distribution f (.ofReal t) μ := sorry + +/-- The layer-cake theorem, or Cavalieri's principle, written using `snorm`. -/ +lemma snorm_pow_eq_distribution {p : ℝ≥0} (hp : 1 ≤ p) : + snorm f p μ ^ (p : ℝ) = + ∫⁻ t in Ioi (0 : ℝ), p * ENNReal.ofReal (t ^ ((p : ℝ) - 1)) * distribution f (.ofReal t) μ := by + sorry + +lemma lintegral_pow_mul_distribution {p : ℝ} (hp : 1 ≤ p) : + ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (t ^ p) * distribution f (.ofReal t) μ = + ENNReal.ofReal p⁻¹ * ∫⁻ x, ‖f x‖₊ ^ (p + 1) ∂μ := sorry + + +/-- The weak L^p norm of a function, for `p < ∞` -/ +def wnorm' [NNNorm E] (f : α → E) (p : ℝ) (μ : Measure α) : ℝ≥0∞ := + ⨆ t : ℝ≥0, t * distribution f t μ ^ (p : ℝ)⁻¹ + +lemma wnorm'_le_snorm' {f : α → E} (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 1 ≤ p) : + wnorm' f p μ ≤ snorm' f p μ := sorry + +/-- The weak L^p norm of a function. -/ +def wnorm [NNNorm E] (f : α → E) (p : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ := + if p = ∞ then snormEssSup f μ else wnorm' f (ENNReal.toReal p) μ + +lemma wnorm_le_snorm {f : α → E} (hf : AEStronglyMeasurable f μ) {p : ℝ≥0∞} (hp : 1 ≤ p) : + wnorm f p μ ≤ snorm f p μ := sorry + +/-- A function is in weak-L^p if it is (strongly a.e.)-measurable and has finite weak L^p norm. -/ +def MemWℒp [NNNorm E] (f : α → E) (p : ℝ≥0∞) (μ : Measure α) : Prop := + AEStronglyMeasurable f μ ∧ wnorm f p μ < ∞ + +lemma Memℒp.memWℒp {f : α → E} {p : ℝ≥0∞} (hp : 1 ≤ p) (hf : Memℒp f p μ) : + MemWℒp f p μ := sorry + +/- Todo: define `MeasureTheory.WLp` as a subgroup, similar to `MeasureTheory.Lp` -/ + +/-- An operator has weak type `(p, q)` if it is bounded as a map from L^p to weak-L^q. +`HasWeakType T p p' μ ν c` means that `T` has weak type (p, q) w.r.t. measures `μ`, `ν` +and constant `c`. -/ +def HasWeakType (T : (α → E₁) → (α' → E₂)) (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') + (c : ℝ≥0) : Prop := + ∀ f : α → E₁, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ wnorm (T f) p' ν ≤ c * snorm f p μ + +/-- An operator has strong type (p, q) if it is bounded as an operator on `L^p → L^q`. +`HasStrongType T p p' μ ν c` means that `T` has strong type (p, q) w.r.t. measures `μ`, `ν` +and constant `c`. -/ +def HasStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] + {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → E) → (α' → E')) + (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0) : Prop := + ∀ f : α → E, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ snorm (T f) p' ν ≤ c * snorm f p μ + +/-- A weaker version of `HasStrongType`. This is the same as `HasStrongType` if `T` is continuous +w.r.t. the L^2 norm, but weaker in general. -/ +def HasBoundedStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] + {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → E) → (α' → E')) + (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0) : Prop := + ∀ f : α → E, Memℒp f p μ → snorm f ∞ μ < ∞ → μ (support f) < ∞ → + AEStronglyMeasurable (T f) ν ∧ snorm (T f) p' ν ≤ c * snorm f p μ + + +lemma HasStrongType.hasWeakType (hp : 1 ≤ p) + (h : HasStrongType T p p' μ ν c) : HasWeakType T p p' μ ν c := by + sorry + +lemma HasStrongType.hasBoundedStrongType (h : HasStrongType T p p' μ ν c) : + HasBoundedStrongType T p p' μ ν c := + fun f hf _ _ ↦ h f hf + + +end MeasureTheory