The Marcinkiewisz interpolation theorem for Lorentz spaces #
Upstreaming status: this file is under construction and being worked on. Don't upstream yet!
The constant occurring in the general real interpolation theorem (for Lorentz spaces)
Equations
- C_LorentzInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t = sorry
Instances For
theorem
exists_hasLorentzType_real_interpolation
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_5}
{E₂ : Type u_6}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α'}
{T : (α → E₁) → α' → E₂}
{p₀ p₁ r₀ r₁ q₀ q₁ s₀ s₁ p q : ENNReal}
[MeasurableSpace E₁]
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[MeasurableSpace E₂]
[TopologicalSpace E₂]
[ENormedAddCommMonoid E₂]
(hp₀ : 1 ≤ p₀)
(hp₁ : 1 ≤ p₁)
(hr₀ : 1 ≤ r₀)
(hr₁ : 1 ≤ r₁)
(hq₀ : 1 ≤ q₀)
(hq₁ : 1 ≤ q₁)
(hs₀ : 1 ≤ s₀)
(hs₁ : 1 ≤ s₁)
(hp₀p₁ : p₀ ≠ p₁)
(hq₀q₁ : q₀ ≠ q₁)
{C₀ C₁ t A : NNReal}
(hA : 0 < 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₁), MeasureTheory.MemLorentz f p q μ → MeasureTheory.AEStronglyMeasurable (T f) ν)
(hT :
MeasureTheory.AESubadditiveOn T
(fun (f : α → E₁) => MeasureTheory.MemLorentz f p₀ r₀ μ ∨ MeasureTheory.MemLorentz f p₁ r₁ μ) (↑A) ν)
(h₀T : MeasureTheory.HasLorentzType T p₀ r₀ q₀ s₀ μ ν ↑C₀)
(h₁T : MeasureTheory.HasLorentzType T p₁ r₁ q₁ s₁ μ ν ↑C₁)
(r : ENNReal)
:
0 < r → MeasureTheory.HasLorentzType T p r q r μ ν ↑(C_LorentzInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A ↑t)
General Marcinkiewicz real interpolation theorem