The Marcinkiewisz real interpolation theorem #
This file contains a proof of the Marcinkiewisz real interpolation theorem. The proof roughly follows Folland, Real Analysis. Modern Techniques and Their Applications, section 6.4, theorem 6.28, but a different truncation is used, and some estimates instead follow the technique as e.g. described in [Duoandikoetxea, Fourier Analysis, 2000].
This file has the definitions for the main proof, and the final proof of the theorem. A few other files contain the necessary pre-requisites:
- (in
InterpolateExponents.lean) Convenience results for working with (interpolated) exponents - (in
InterpolateExponents.lean) Results about the particular choice of exponent - (in
Misc.lean) Interface for using cutoff functions - (in
Misc.lean) Results about the particular choice of scale - (in
Misc.lean) Some tools for measure theory computations - (in
Misc.lean) Results about truncations of a function - (in
Misc.lean) Measurability properties of truncations - (in
Misc.lean) Truncations and Lp spaces - (in
Misc.lean) Some results about the integrals of truncations - (in
Minkowski.lean) Minkowski's integral inequality - (in
Minkowski.lean) Apply Minkowski's integral inequality to truncations - (in
Minkowski.lean) Weaktype estimates applied to truncations
TODO #
Generalise this to functions taking values in ℝ≥0∞, instead of ℝ. This entails generalising
most intermediate lemmas from normed spaces to the appropriate enorm classes.
def
MeasureTheory.Subadditive
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[ENorm ε]
(T : (α → ε₁) → α' → ε)
:
Equations
Instances For
def
MeasureTheory.Subadditive_trunc
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[ENorm ε]
(T : (α → ε₁) → α' → ε)
(A : ENNReal)
(f : α → ε₁)
(ν : Measure α')
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.AESubadditiveOn
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[ENorm ε]
(T : (α → ε₁) → α' → ε)
(P : (α → ε₁) → Prop)
(A : ENNReal)
(ν : Measure α')
:
The operator is subadditive on functions satisfying P with constant A
(this is almost vacuous if A = ⊤).
Equations
Instances For
theorem
MeasureTheory.AESubadditiveOn.antitone
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{ν : Measure α'}
{T : (α → ε₁) → α' → ε}
{P P' : (α → ε₁) → Prop}
(h : ∀ {u : α → ε₁}, P u → P' u)
{A : ENNReal}
(sa : AESubadditiveOn T P' A ν)
:
AESubadditiveOn T P A ν
theorem
MeasureTheory.AESubadditiveOn.zero
{α : Type u_1}
{α' : Type u_2}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
{ε₂ : Type u_9}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ENormedAddMonoid ε₂]
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
{P : (α → ε₁) → Prop}
(hP : ∀ {f g : α → ε₁}, P f → P g → P (f + g))
(A : ENNReal)
(h : ∀ (u : α → ε₁), P u → T u =ᶠ[ae ν] 0)
:
AESubadditiveOn T P A ν
theorem
MeasureTheory.AESubadditiveOn.forall_le
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{ν : Measure α'}
{ι : Type u_10}
{𝓑 : Set ι}
(h𝓑 : 𝓑.Countable)
{T : ι → (α → ε₁) → α' → ε}
{P : (α → ε₁) → Prop}
{A : ENNReal}
(h : ∀ i ∈ 𝓑, AESubadditiveOn (T i) P A ν)
{f g : α → ε₁}
(hf : P f)
(hg : P g)
:
theorem
MeasureTheory.AESubadditiveOn.biSup
{α : Type u_1}
{α' : Type u_2}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
{ν : Measure α'}
{ι : Type u_10}
{𝓑 : Set ι}
(h𝓑 : 𝓑.Countable)
{T : ι → (α → ε₁) → α' → ENNReal}
{P : (α → ε₁) → Prop}
(hT : ∀ (u : α → ε₁), P u → ∀ᵐ (x : α') ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ⊤)
(hP : ∀ {f g : α → ε₁}, P f → P g → P (f + g))
{A : ENNReal}
(h : ∀ i ∈ 𝓑, AESubadditiveOn (T i) P A ν)
:
AESubadditiveOn (fun (u : α → ε₁) (x : α') => ⨆ i ∈ 𝓑, T i u x) P A ν
theorem
MeasureTheory.AESubadditiveOn.indicator
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{ν : Measure α'}
{T : (α → ε₁) → α' → ε}
{P : (α → ε₁) → Prop}
{A : ENNReal}
(sa : AESubadditiveOn T P A ν)
(S : Set α')
:
AESubadditiveOn (fun (u : α → ε₁) (x : α') => S.indicator (fun (y : α') => T u y) x) P A ν
theorem
MeasureTheory.AESubadditiveOn.const
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{ν : Measure α'}
(T : (α → ε₁) → ε)
(P : (α → ε₁) → Prop)
(h_add : ∀ {f g : α → ε₁}, P f → P g → ‖T (f + g)‖ₑ ≤ ‖T f‖ₑ + ‖T g‖ₑ)
:
AESubadditiveOn (fun (u : α → ε₁) (x : α') => T u) P 1 ν
def
MeasureTheory.AESublinearOn
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
[TopologicalSpace ε]
[ENormedSpace ε]
{ε₁ : Type u_10}
[TopologicalSpace ε₁]
[ENormedSpace ε₁]
(T : (α → ε₁) → α' → ε)
(P : (α → ε₁) → Prop)
(A : ENNReal)
(ν : Measure α')
:
The operator is sublinear on functions satisfying P with constant A.
Equations
- MeasureTheory.AESublinearOn T P A ν = (MeasureTheory.AESubadditiveOn T P A ν ∧ ∀ (f : α → ε₁) (c : NNReal), P f → T (c • f) =ᵐ[ν] c • T f)
Instances For
theorem
MeasureTheory.AESublinearOn.antitone
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
[TopologicalSpace ε]
[ENormedSpace ε]
{ε₁ : Type u_10}
[TopologicalSpace ε₁]
[ENormedSpace ε₁]
{ν : Measure α'}
{T : (α → ε₁) → α' → ε}
{P P' : (α → ε₁) → Prop}
(h : ∀ {u : α → ε₁}, P u → P' u)
{A : ENNReal}
(sl : AESublinearOn T P' A ν)
:
AESublinearOn T P A ν
theorem
MeasureTheory.AESublinearOn.biSup
{α : Type u_1}
{α' : Type u_2}
{m' : MeasurableSpace α'}
{ε₁ : Type u_10}
[TopologicalSpace ε₁]
[ENormedSpace ε₁]
{ν : Measure α'}
{ι : Type u_12}
{𝓑 : Set ι}
(h𝓑 : 𝓑.Countable)
{T : ι → (α → ε₁) → α' → ENNReal}
{P : (α → ε₁) → Prop}
(hT : ∀ (u : α → ε₁), P u → ∀ᵐ (x : α') ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ⊤)
(h_add : ∀ {f g : α → ε₁}, P f → P g → P (f + g))
(h_smul : ∀ {f : α → ε₁} {c : NNReal}, P f → P (c • f))
{A : ENNReal}
(h : ∀ i ∈ 𝓑, AESublinearOn (T i) P A ν)
:
AESublinearOn (fun (u : α → ε₁) (x : α') => ⨆ i ∈ 𝓑, T i u x) P A ν
theorem
MeasureTheory.AESublinearOn.biSup2
{α : Type u_1}
{α' : Type u_2}
{m' : MeasurableSpace α'}
{ε₁ : Type u_10}
[TopologicalSpace ε₁]
[ENormedSpace ε₁]
{ν : Measure α'}
{ι : Type u_12}
{𝓑 : Set ι}
(h𝓑 : 𝓑.Countable)
{T : ι → (α → ε₁) → α' → ENNReal}
{P Q : (α → ε₁) → Prop}
(hPT : ∀ (u : α → ε₁), P u → ∀ᵐ (x : α') ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ⊤)
(hQT : ∀ (u : α → ε₁), Q u → ∀ᵐ (x : α') ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ⊤)
(P0 : P 0)
(Q0 : Q 0)
(haP : ∀ {f g : α → ε₁}, P f → P g → P (f + g))
(haQ : ∀ {f g : α → ε₁}, Q f → Q g → Q (f + g))
(hsP : ∀ {f : α → ε₁} {c : NNReal}, P f → P (c • f))
(hsQ : ∀ {f : α → ε₁} {c : NNReal}, Q f → Q (c • f))
{A : NNReal}
(hAP : ∀ i ∈ 𝓑, AESublinearOn (T i) (fun (g : α → ε₁) => g ∈ {f : α → ε₁ | P f} + {f : α → ε₁ | Q f}) (↑A) ν)
:
AESublinearOn (fun (u : α → ε₁) (x : α') => ⨆ i ∈ 𝓑, T i u x) (fun (f : α → ε₁) => P f ∨ Q f) (↑A) ν
theorem
MeasureTheory.AESublinearOn.indicator
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
[TopologicalSpace ε]
[ENormedSpace ε]
{ε₁ : Type u_10}
[TopologicalSpace ε₁]
[ENormedSpace ε₁]
{ν : Measure α'}
{T : (α → ε₁) → α' → ε}
{P : (α → ε₁) → Prop}
{A : ENNReal}
(S : Set α')
(sl : AESublinearOn T P A ν)
:
AESublinearOn (fun (u : α → ε₁) (x : α') => S.indicator (fun (y : α') => T u y) x) P A ν
theorem
MeasureTheory.AESublinearOn.const
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
[TopologicalSpace ε]
[ENormedSpace ε]
{ε₁ : Type u_10}
[TopologicalSpace ε₁]
[ENormedSpace ε₁]
{ν : Measure α'}
(T : (α → ε₁) → ε)
(P : (α → ε₁) → Prop)
(h_add : ∀ {f g : α → ε₁}, P f → P g → ‖T (f + g)‖ₑ ≤ ‖T f‖ₑ + ‖T g‖ₑ)
(h_smul : ∀ (f : α → ε₁) {c : NNReal}, P f → T (c • f) = c • T f)
:
AESublinearOn (fun (u : α → ε₁) (x : α') => T u) P 1 ν
theorem
MeasureTheory.AESublinearOn.toReal
{α : Type u_1}
{α' : Type u_2}
{m' : MeasurableSpace α'}
{ε₁ : Type u_10}
[TopologicalSpace ε₁]
[ENormedSpace ε₁]
{ν : Measure α'}
{T : (α → ε₁) → α' → ENNReal}
{P : (α → ε₁) → Prop}
{A : ENNReal}
(h : AESublinearOn T P A ν)
(hP : ∀ (u : α → ε₁), P u → ∀ᵐ (x : α') ∂ν, T u x ≠ ⊤)
:
AESublinearOn (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) P A ν
Proof of the real interpolation theorem #
In this section the estimates are combined to finally give a proof of the
real interpolation theorem.
def
MeasureTheory.PreservesAEStrongMeasurability
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{ε₁ : Type u_7}
{ε₂ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε₂]
(T : (α → ε₁) → α' → ε₂)
(p : ENNReal)
:
Proposition that expresses that the map T map between function spaces preserves
AE strong measurability on L^p.
Equations
- MeasureTheory.PreservesAEStrongMeasurability T p = ∀ ⦃f : α → ε₁⦄, MeasureTheory.MemLp f p μ → MeasureTheory.AEStronglyMeasurable (T f) ν
Instances For
theorem
MeasureTheory.estimate_distribution_Subadditive_trunc
{α : Type u_1}
{α' : Type u_2}
{m' : MeasurableSpace α'}
{ν : Measure α'}
{t : ENNReal}
{ε₁ : Type u_7}
{ε₂ : Type u_8}
[TopologicalSpace ε₁]
[ENormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ENormedAddMonoid ε₂]
{f : α → ε₁}
{T : (α → ε₁) → α' → ε₂}
{a : ENNReal}
(ha : 0 < a)
{A : ENNReal}
(h : Subadditive_trunc T A f ν)
:
distribution (T f) (2 * A * t) ν ≤ distribution (T (trunc f a)) t ν + distribution (T (truncCompl f a)) t ν
theorem
MeasureTheory.rewrite_norm_func
{α' : Type u_2}
{E : Type u_3}
{m' : MeasurableSpace α'}
{ν : Measure α'}
{q : ℝ}
{g : α' → E}
[TopologicalSpace E]
[ENormedAddCommMonoid E]
(hq : 0 < q)
{A : NNReal}
(hA : 0 < A)
(hg : AEStronglyMeasurable g ν)
:
theorem
MeasureTheory.estimate_norm_rpow_range_operator
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m' : MeasurableSpace α'}
{ν : Measure α'}
{T : (α → E₁) → α' → E₂}
{q : ℝ}
{f : α → E₁}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hq : 0 < q)
(tc : StrictRangeToneCouple)
{A : NNReal}
(hA : 0 < A)
(ht : Subadditive_trunc T (↑A) f ν)
(hTf : AEStronglyMeasurable (T f) ν)
:
theorem
MeasureTheory.ton_measurable_eLpNorm_trunc
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p₁ : ENNReal}
{μ : Measure α}
{f : α → E₁}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(tc : ToneCouple)
:
Measurable fun (x : ENNReal) => eLpNorm (trunc f (tc.ton x)) p₁ μ
theorem
MeasureTheory.estimate_norm_rpow_range_operator'
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : Measure α}
{ν : Measure α'}
{f : α → E₁}
{T : (α → E₁) → α' → E₂}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hp₀ : 0 < p₀)
(hq₀ : 0 < q₀)
(hq₁ : 0 < q₁)
(hp₁p : p < p₁)
(hp₀p : p₀ < p)
(tc : StrictRangeToneCouple)
(hq₀' : q₀ = ⊤ → ∀ s > 0, distribution (T (truncCompl f (tc.ton s))) s ν = 0)
(hq₁' : q₁ = ⊤ → ∀ s > 0, distribution (T (trunc f (tc.ton s))) s ν = 0)
(hf : MemLp f p μ)
(hT₁ : HasWeakType T p₁ q₁ μ ν ↑C₁)
(hT₀ : HasWeakType T p₀ q₀ μ ν ↑C₀)
:
∫⁻ (s : ENNReal), distribution (T (trunc f (tc.ton s))) s ν * s ^ (q.toReal - 1) + distribution (T (truncCompl f (tc.ton s))) s ν * s ^ (q.toReal - 1) ≤ (if q₁ < ⊤ then 1 else 0) * (↑C₁ ^ q₁.toReal * ∫⁻ (s : ENNReal), eLpNorm (trunc f (tc.ton s)) p₁ μ ^ q₁.toReal * s ^ (q.toReal - q₁.toReal - 1)) + (if q₀ < ⊤ then 1 else 0) * (↑C₀ ^ q₀.toReal * ∫⁻ (s : ENNReal), eLpNorm (truncCompl f (tc.ton s)) p₀ μ ^ q₀.toReal * s ^ (q.toReal - q₀.toReal - 1))
theorem
MeasureTheory.simplify_factor₀
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : Measure α}
{f : α → E₁}
{t D : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(hq₀' : q₀ ≠ ⊤)
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(ht : t ∈ Set.Ioo 0 1)
(hq₀q₁ : q₀ ≠ q₁)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
(hD : D = ChoiceScale.d)
:
theorem
MeasureTheory.simplify_factor₁
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : Measure α}
{f : α → E₁}
{t D : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(hq₁' : q₁ ≠ ⊤)
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(ht : t ∈ Set.Ioo 0 1)
(hq₀q₁ : q₀ ≠ q₁)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
(hD : D = ChoiceScale.d)
:
def
MeasureTheory.finite_spanning_sets_from_lintegrable
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{g : α → ENNReal}
(hg : AEMeasurable g μ)
(hg_int : ∫⁻ (x : α), g x ∂μ < ⊤)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.support_sigma_finite_of_lintegrable
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{g : α → ENNReal}
(hg : AEMeasurable g μ)
(hg_int : ∫⁻ (x : α), g x ∂μ < ⊤)
:
SigmaFinite (μ.restrict (Function.support g))
theorem
MeasureTheory.support_sigma_finite_from_MemLp
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{f : α → E₁}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(hf : MemLp f p μ)
(hp : p ≠ ⊤)
(hp' : p ≠ 0)
:
SigmaFinite (μ.restrict (Function.support f))
theorem
MeasureTheory.combine_estimates₀
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : Measure α}
{ν : Measure α'}
{f : α → E₁}
{t : ENNReal}
{T : (α → E₁) → α' → E₂}
{A : NNReal}
(hA : 0 < A)
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[MeasurableSpace E₁]
[BorelSpace E₁]
[TopologicalSpace.PseudoMetrizableSpace E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
{spf : ScaledPowerFunction}
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(ht : t ∈ Set.Ioo 0 1)
(hp₀p₁ : p₀ < p₁)
(hq₀q₁ : q₀ ≠ q₁)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
(hf : MemLp f p μ)
(hT : Subadditive_trunc T (↑A) f ν)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
(hspf : spf = ChoiceScale.spf_ch ⋯ hq₀q₁ ⋯ ⋯ ⋯ ⋯ ⋯ hC₀ hC₁ hF)
(h₁T : HasWeakType T p₁ q₁ μ ν ↑C₁)
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(h₂T : PreservesAEStrongMeasurability T p)
:
∫⁻ (x : α'), ‖T f x‖ₑ ^ q.toReal ∂ν ≤ ENNReal.ofReal ((2 * ↑A) ^ q.toReal * q.toReal) * ((if q₁ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ + (if q₀ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹) * ↑C₀ ^ ((1 - t).toReal * q.toReal) * ↑C₁ ^ (t.toReal * q.toReal) * eLpNorm f p μ ^ q.toReal
theorem
MeasureTheory.combine_estimates₁
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : Measure α}
{ν : Measure α'}
{f : α → E₁}
{t : ENNReal}
{T : (α → E₁) → α' → E₂}
{A : NNReal}
(hA : 0 < A)
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[MeasurableSpace E₁]
[BorelSpace E₁]
[TopologicalSpace.PseudoMetrizableSpace E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
{spf : ScaledPowerFunction}
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(ht : t ∈ Set.Ioo 0 1)
(hp₀p₁ : p₀ < p₁)
(hq₀q₁ : q₀ ≠ q₁)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
(hf : MemLp f p μ)
(hT : Subadditive_trunc T (↑A) f ν)
(h₁T : HasWeakType T p₁ q₁ μ ν ↑C₁)
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(h₂T : PreservesAEStrongMeasurability T p)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
(hspf : spf = ChoiceScale.spf_ch ⋯ hq₀q₁ ⋯ ⋯ ⋯ ⋯ ⋯ hC₀ hC₁ hF)
:
theorem
MeasureTheory.simplify_factor₃
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p p₀ q₀ p₁ : ENNReal}
{C₀ : NNReal}
{μ : Measure α}
{f : α → E₁}
{t : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(hp₀ : 0 < p₀)
(hp₀' : p₀ ≠ ⊤)
(ht : t ∈ Set.Ioo 0 1)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hp₀p₁ : p₀ = p₁)
:
theorem
MeasureTheory.simplify_factor_aux₄
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p q p₀ q₀ p₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : Measure α}
{f : α → E₁}
{t : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(hq₀' : q₀ ≠ ⊤)
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(ht : t ∈ Set.Ioo 0 1)
(hp₀p₁ : p₀ = p₁)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hF : eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
MeasureTheory.simplify_factor₄
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : Measure α}
{f : α → E₁}
{t D : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(hq₀' : q₀ ≠ ⊤)
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(ht : t ∈ Set.Ioo 0 1)
(hp₀p₁ : p₀ = p₁)
(hq₀q₁ : q₀ ≠ q₁)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
(hD : D = ChoiceScale.d)
:
theorem
MeasureTheory.simplify_factor₅
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : Measure α}
{f : α → E₁}
{t D : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(hq₁' : q₁ ≠ ⊤)
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(ht : t ∈ Set.Ioo 0 1)
(hp₀p₁ : p₀ = p₁)
(hq₀q₁ : q₀ ≠ q₁)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
(hD : D = ChoiceScale.d)
:
theorem
MeasureTheory.exists_hasStrongType_real_interpolation_aux₀
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{f : α → E₁}
{t : ENNReal}
{T : (α → E₁) → α' → E₂}
{p₀ p₁ q₀ q₁ p q : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(ht : t ∈ Set.Ioo 0 1)
{C₀ : NNReal}
(hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
(hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(h₂T : PreservesAEStrongMeasurability T p)
(hf : MemLp f p μ)
(hF : eLpNorm f p μ = 0)
:
The trivial case for the estimate in the real interpolation theorem
when the function Lp norm of f vanishes.
theorem
MeasureTheory.exists_hasStrongType_real_interpolation_aux
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{f : α → E₁}
{t : ENNReal}
{T : (α → E₁) → α' → E₂}
{p₀ p₁ q₀ q₁ p q : ENNReal}
{A : NNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[MeasurableSpace E₁]
[BorelSpace E₁]
[TopologicalSpace.PseudoMetrizableSpace E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hA : 0 < A)
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(hp₀p₁ : p₀ < p₁)
(hq₀q₁ : q₀ ≠ q₁)
{C₀ C₁ : NNReal}
(ht : t ∈ Set.Ioo 0 1)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
(hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
(hT : Subadditive_trunc T (↑A) f ν)
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(h₁T : HasWeakType T p₁ q₁ μ ν ↑C₁)
(h₂T : PreservesAEStrongMeasurability T p)
(hf : MemLp f p μ)
:
The estimate for the real interpolation theorem in case p₀ < p₁.
theorem
MeasureTheory.exists_hasStrongType_real_interpolation_aux₁
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{μ : Measure α}
{t : ENNReal}
{f : α → E₁}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(hp₀p₁ : p₀ = p₁)
(hq₀q₁ : q₀ < q₁)
{C₀ C₁ : NNReal}
(ht : t ∈ Set.Ioo 0 1)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
(hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
(hF : eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
(ENNReal.ofReal q.toReal * ((((↑C₀ * eLpNorm f p μ) ^ q₀.toReal * ∫⁻ (t : ℝ) in Set.Ioo 0 ChoiceScale.d.toReal, ENNReal.ofReal (t ^ (q.toReal - q₀.toReal - 1))) * if q₀ = ⊤ then 0 else 1) + ((↑C₁ * eLpNorm f p μ) ^ q₁.toReal * ∫⁻ (t : ℝ) in Set.Ici ChoiceScale.d.toReal, ENNReal.ofReal (t ^ (q.toReal - q₁.toReal - 1))) * if q₁ = ⊤ then 0 else 1)) ^ q.toReal⁻¹ = q ^ q.toReal⁻¹ * ((ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹ * if q₀ = ⊤ then 0 else 1) + ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ * if q₁ = ⊤ then 0 else 1) ^ q.toReal⁻¹ * ↑C₀ ^ (1 - t).toReal * ↑C₁ ^ t.toReal * eLpNorm f p μ
theorem
MeasureTheory.exists_hasStrongType_real_interpolation_aux₂
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{t : ENNReal}
{T : (α → E₁) → α' → E₂}
{f : α → E₁}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(hp₀p₁ : p₀ = p₁)
(hq₀q₁ : q₀ < q₁)
{C₀ C₁ : NNReal}
(ht : t ∈ Set.Ioo 0 1)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
(hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(h₁T : HasWeakType T p₁ q₁ μ ν ↑C₁)
(h₂T : PreservesAEStrongMeasurability T p)
(hf : MemLp f p μ)
:
The main estimate in the real interpolation theorem for p₀ = p₁, before taking roots,
for the case q₀ < q₁.
theorem
MeasureTheory.exists_hasStrongType_real_interpolation_aux₃
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{f : α → E₁}
{t : ENNReal}
{T : (α → E₁) → α' → E₂}
{p₀ p₁ q₀ q₁ p q : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(hp₀p₁ : p₀ = p₁)
(hq₀q₁ : q₀ ≠ q₁)
{C₀ C₁ : NNReal}
(ht : t ∈ Set.Ioo 0 1)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
(hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(h₁T : HasWeakType T p₁ q₁ μ ν ↑C₁)
(h₂T : PreservesAEStrongMeasurability T p)
(hf : MemLp f p μ)
:
The main estimate for the real interpolation theorem for p₀ = p₁, requiring q₀ ≠ q₁,
before taking roots.
theorem
MeasureTheory.exists_hasStrongType_real_interpolation_aux₄
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{f : α → E₁}
{t : ENNReal}
{T : (α → E₁) → α' → E₂}
{p₀ p₁ q₀ q₁ p q : ENNReal}
{A : NNReal}
(hA : 0 < A)
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[MeasurableSpace E₁]
[BorelSpace E₁]
[TopologicalSpace.PseudoMetrizableSpace E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(hq₀q₁ : q₀ ≠ q₁)
{C₀ C₁ : NNReal}
(ht : t ∈ Set.Ioo 0 1)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
(hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
(hT : Subadditive_trunc T (↑A) f ν)
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(h₁T : HasWeakType T p₁ q₁ μ ν ↑C₁)
(h₂T : PreservesAEStrongMeasurability T p)
(hf : MemLp f p μ)
:
The main estimate for the real interpolation theorem, before taking roots, combining
the cases p₀ ≠ p₁ and p₀ = p₁.
def
MeasureTheory.C_realInterpolation_ENNReal
(p₀ p₁ q₀ q₁ q : ENNReal)
(C₀ C₁ A : NNReal)
(t : ENNReal)
:
The definition of the constant in the real interpolation theorem, when viewed as
an element of ℝ≥0∞.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constant occurring in the real interpolation theorem
Equations
- MeasureTheory.C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t = (MeasureTheory.C_realInterpolation_ENNReal p₀ p₁ q₀ q₁ q C₀ C₁ A t).toNNReal
Instances For
theorem
MeasureTheory.coe_C_realInterpolation
{t p₀ p₁ q₀ q₁ q : ENNReal}
{A : NNReal}
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(hq₀q₁ : q₀ ≠ q₁)
{C₀ C₁ : NNReal}
(ht : t ∈ Set.Ioo 0 1)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
:
↑(C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t) = C_realInterpolation_ENNReal p₀ p₁ q₀ q₁ q C₀ C₁ A t
theorem
MeasureTheory.Subadditive_trunc_from_SubadditiveOn_Lp₀p₁
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{f : α → E₁}
{t : ENNReal}
{T : (α → E₁) → α' → E₂}
{p₀ p₁ p : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hp₀ : 0 < p₀)
(hp₁ : 0 < p₁)
{A : NNReal}
(hA : 1 ≤ A)
(ht : t ∈ Set.Ioo 0 1)
(hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
(hT : AESubadditiveOn T (fun (f : α → E₁) => MemLp f p₀ μ ∨ MemLp f p₁ μ) (↑A) ν)
(hf : MemLp f p μ)
:
Subadditive_trunc T (↑A) f ν
theorem
MeasureTheory.exists_hasStrongType_real_interpolation
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{t : ENNReal}
{T : (α → E₁) → α' → E₂}
{p₀ p₁ q₀ q₁ p q : ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[MeasurableSpace E₁]
[BorelSpace E₁]
[TopologicalSpace.PseudoMetrizableSpace E₁]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hp₀ : p₀ ∈ Set.Ioc 0 q₀)
(hp₁ : p₁ ∈ Set.Ioc 0 q₁)
(hq₀q₁ : q₀ ≠ q₁)
{C₀ C₁ A : NNReal}
(hA : 1 ≤ A)
(ht : t ∈ Set.Ioo 0 1)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
(hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
(hmT : ∀ (f : α → E₁), MemLp f p μ → AEStronglyMeasurable (T f) ν)
(hT : AESubadditiveOn T (fun (f : α → E₁) => MemLp f p₀ μ ∨ MemLp f p₁ μ) (↑A) ν)
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(h₁T : HasWeakType T p₁ q₁ μ ν ↑C₁)
:
HasStrongType T p q μ ν ↑(C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t)
Marcinkiewicz real interpolation theorem