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
Upstreaming status: the result is highly desirable; the ideal proof strategy is not yet clear. It may be nicer to generalise this to Lorentz spaces first, and then upstream the proof there. (Useful ingredients for this proof also belong into mathlib.) Prioritise other files first (e.g., about weak type or the prerequisites files).
def
MeasureTheory.Subadditive
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ESeminormedAddMonoid ε₁]
[ENorm ε]
(T : (α → ε₁) → α' → ε)
:
Equations
Instances For
def
MeasureTheory.Subadditive_trunc
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
[TopologicalSpace ε₁]
[ESeminormedAddMonoid ε₁]
[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 ε₁]
[ESeminormedAddMonoid ε₁]
[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 ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{ν : 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 ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ESeminormedAddMonoid ε₂]
{ν : 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 ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{ν : 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 ε₁]
[ESeminormedAddMonoid ε₁]
{ν : 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 ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{ν : 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 ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{ν : 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 ε₁]
[ESeminormedAddMonoid ε₁]
[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 ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ESeminormedAddMonoid ε₂]
{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]
[ESeminormedAddCommMonoid 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₁]
[ESeminormedAddCommMonoid E₁]
[TopologicalSpace E₂]
[ESeminormedAddCommMonoid 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₁]
[ESeminormedAddCommMonoid 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₁]
[ESeminormedAddCommMonoid 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₁]
[ESeminormedAddCommMonoid 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₁]
[ESeminormedAddCommMonoid 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₁]
[ESeminormedAddCommMonoid 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₁]
[ESeminormedAddCommMonoid 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₁]
[ESeminormedAddCommMonoid 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