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].
The file consists of the following sections:
- Convience results for working with (interpolated) exponents
- Results about the particular choice of exponent
- Interface for using cutoff functions
- Results about the particular choice of scale
- Some tools for measure theory computations
- Results about truncations of a function
- Measurability properties of truncations
- Truncations and Lp spaces
- Some results about the integrals of truncations
- Minkowski's integral inequality
- Apply Minkowski's integral inequality to truncations
- Weaktype estimates applied to truncations
- Definitions
- Proof of the real interpolation theorem
Convenience results for working with (interpolated) exponents #
Results about the particular choice of exponent #
The proof of the real interpolation theorem will estimate
`distribution (trunc f A(t)) t` and `distribution (trunc_compl f A(t)) t` for a
function `A`. The function `A` can be given a closed-form expression that works for
_all_ cases in the real interpolation theorem, because of the computation rules available
for elements in `ℝ≥0∞` that avoid the need for a limiting procedure, e.g. `⊤⁻¹ = 0`.
The function `A` will be of the form `A(t) = (t / d) ^ σ` for particular choices of `d` and
`σ`. This section contatins results about the exponents `σ`.
Interface for using cutoff functions #
A ToneCouple is an couple of two monotone functions that are practically inverses of each other. It is used in the proof of the real interpolation theorem.
Note: originally it seemed useful to make the possible choice of this function general in the proof of the real inteprolation theorem. However, in the end really only one function works for all the different cases. This infrastructure, however, could potentially still be useful, if one would like to try to improve the constant.
- mon : Bool
- ton_is_ton : if self.mon = true then StrictMonoOn self.ton (Set.Ioi 0) else StrictAntiOn self.ton (Set.Ioi 0)
A scaled power function gives rise to a ToneCouple.
Equations
- One or more equations did not get rendered due to their size.
Results about the particular choice of scale #
The proof of the real interpolation theorem will estimate
`distribution (trunc f A(t)) t` and `distribution (trunc_compl f A(t)) t` for a
function `A`. The function `A` can be given a closed-form expression that works for
_all_ cases in the real interpolation theorem, because of the computation rules available
for elements in `ℝ≥0∞` that avoid the need for a limiting procedure, e.g. `⊤⁻¹ = 0`.
The function `A` will be of the form `A(t) = (t / d) ^ σ` for particular choices of `d` and
`σ`. This section contatins results about the scale `d`.
Equations
- One or more equations did not get rendered due to their size.
The particular choice of scaled power function that works in the proof of the real interpolation theorem.
Equations
- ChoiceScale.spf_ch ht hq₀q₁ hp₀ hq₀ hp₁ hq₁ hp₀p₁ hC₀ hC₁ hF = { σ := ComputationsChoiceExponent.ζ, d := ChoiceScale.d, hd := ⋯, hσ := ⋯ }
Some tools for measure theory computations #
A collection of small lemmas to help with integral manipulations.
Results about truncations of a function #
The t
-truncation of a function f
.
Equations
- MeasureTheory.trunc f t x = if ‖f x‖ ≤ t then f x else 0
The complement of a t
-truncation of a function f
.
Equations
- MeasureTheory.trunc_compl f t = f - MeasureTheory.trunc f t
A function to deal with truncations and complement of truncations in one go.
Equations
- MeasureTheory.trnc false f t = f - MeasureTheory.trunc f t
- MeasureTheory.trnc true f t = MeasureTheory.trunc f t
A function is the complement if its truncation and the complement of the truncation.
If the truncation parameter is non-positive, the truncation vanishes.
If the truncation parameter is non-positive, the complement of the truncation is the function itself.
Measurability properties of truncations #
A small lemma that is helpful for rewriting
The norm of the truncation is monotone in the truncation parameter
The norm of the complement of the truncation is antitone in the truncation parameter
The norm of the truncation is meaurable in the truncation parameter
The norm of the complement of the truncation is measurable in the truncation parameter
Truncations and L-p spaces #
If f
is in Lp
, the truncation is element of Lq
for q > p
.
If f
is in Lp
, the complement of the truncation is in Lq
for q < p
.
Some results about the integrals of truncations #
Equations
- MeasureTheory.decidableMemRes = Classical.propDecidable (t ∈ MeasureTheory.res j β)
Extract expressions for the lower Lebesgue integral of power functions
Minkowski's integral inequality #
Equations
- MeasureTheory.trunc_cut f μ n = (MeasureTheory.spanningSets μ n).indicator fun (x : α) => f x ⊓ ↑n
Characterization of ∫⁻ x : α, f x ^ p ∂μ
by a duality argument.
Minkowsi's integral inequality
Apply Minkowski's integral inequality to truncations #
One of the key estimates for the real interpolation theorem, not yet using
the particular choice of exponent and scale in the ScaledPowerFunction
.
Equations
- MeasureTheory.sel true p₀ p₁ = p₁
- MeasureTheory.sel false p₀ p₁ = p₀
One of the key estimates for the real interpolation theorem, now using
the particular choice of exponent, but not yet using the
particular choice of scale in the ScaledPowerFunction
.
Weaktype estimates applied to truncations #
If T
has weaktype p₀
-p₁
, f
is AEStronglyMeasurable
and the p
-norm of f
vanishes, then the q
-norm of T f
vanishes.
Equations
- One or more equations did not get rendered due to their size.
The operator is subadditive on functions satisfying P
with constant A
.
The operator is sublinear on functions satisfying P
with constant A
.
Equations
- MeasureTheory.AESublinearOn T P A ν = (MeasureTheory.AESubAdditiveOn T P A ν ∧ ∀ (f : α → E₁) (c : ℝ), P f → c ≥ 0 → T (c • f) =ᵐ[ν] c • T f)
Proof of the real interpolation theorem #
In this section the estimates are combined to finally give a proof of the
real interpolation theorem.
Proposition that expresses that the map T
map between function spaces preserves
AE strong measurability on L^p.
Equations
- MeasureTheory.PreservesAEStrongMeasurability T p = ∀ ⦃f : α → E₁⦄, MeasureTheory.Memℒp f p μ → MeasureTheory.AEStronglyMeasurable (T f) ν
Equations
- One or more equations did not get rendered due to their size.
The trivial case for the estimate in the real interpolation theorem
when the function Lp
norm of f
vanishes.
The estimate for the real interpolation theorem in case p₀ < p₁
.
The main estimate in the real interpolation theorem for p₀ = p₁
, before taking roots,
for the case q₀ < q₁
.
The main estimate for the real interpolation theorem for p₀ = p₁
, requiring
q₀ ≠ q₁
, before taking roots.
The main estimate for the real interpolation theorem, before taking roots, combining
the cases p₀ ≠ p₁
and p₀ = p₁
.
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
Marcinkiewicz real interpolation theorem.