Extending an operator from L² ∩ Lᵖ to Lᵖ #
An operator initially defined on L² often admits an Lᵖ estimate on functions in both spaces.
For 1 < p < ∞, the intersection is dense in Lᵖ: finite-measure simple functions lie in
both spaces. A uniform estimate therefore gives a unique bounded operator on all of Lᵖ.
This is the final density step in the Calderón–Zygmund strong-type theorem.
The construction uses Mathlib's Lp.simpleFunc.dense and LinearMap.extendOfNorm.
Bounds from simple functions #
An Lᵖ → L^q bound for a bounded operator T : Lʳ → Lˢ, r < ∞, 1 ≤ p < ∞, needs only to be
checked on simple functions in Lʳ: it then holds for every f ∈ Lʳ ∩ Lᵖ
(ContinuousLinearMap.eLpNorm_apply_le_of_forall_simpleFunc). The simple approximants of f
converge to f in Lʳ and Lᵖ at once, and Fatou's lemma bounds ‖T f‖_q. The operator norm
bound itself reads ‖T f‖_s ≤ M ‖f‖_r in eLpNorm form
(ContinuousLinearMap.eLpNorm_apply_le_of_norm_le).
Finite-measure simple functions are in L² at every finite exponent p ≥ 1.
The Lᵖ functions which also belong to L².
Instances For
Membership in Lᵖ ∩ L² means that the Lᵖ representative also has finite L² norm.
The L² membership proof carried by an element of Lᵖ ∩ L².
An Lᵖ ∩ L² function, read as an element of L².
Instances For
The L² and Lᵖ views of an intersection function agree almost everywhere.
The intersection Lᵖ ∩ L² is dense in Lᵖ when p < ∞.
A strong-type estimate on L² makes the operator's value an Lᵖ function whenever its
argument lies in L² ∩ Lᵖ.
The strong-type operator on the dense intersection, with values read in Lᵖ.
Instances For
On the intersection, the strong-type map has the same pointwise values almost everywhere
as the given L² operator.
The Lᵖ bound on L² ∩ Lᵖ, expressed in ordinary operator norms.
The unique continuous Lᵖ extension of an L² operator satisfying a strong-type
estimate. It agrees with the original operator on L² ∩ Lᵖ.
Instances For
On the dense intersection the extension equals the original L² operator, interpreted in
Lᵖ.
The operator norm of the extended map is bounded by the strong-type constant.
The Lᵖ extension agrees almost everywhere with the original L² operator on every
function in L² ∩ Lᵖ.
A bounded operator on Lᵖ agreeing with the strong-type estimate on the dense intersection
is the extension constructed above.
Agreement almost everywhere on every L² ∩ Lᵖ function characterizes the Lᵖ extension.
Bounds from simple functions #
An operator norm bound ‖T‖ ≤ M for T : Lʳ → Lˢ is the bound ‖T f‖_s ≤ M ‖f‖_r in
eLpNorm form.
A bound for T : Lʳ → Lˢ, r < ∞, from Lᵖ to L^q, 1 ≤ p < ∞, on simple functions in
Lʳ passes to every f ∈ Lʳ ∩ Lᵖ, for any finite constant C.