Marcinkiewicz interpolation between weak type (1,1) and L^∞

A sublinear operator T that is simultaneously of weak type (1,1) and bounded on L^∞ is bounded on L^p for every 1 < p < ∞. This is the diagonal case p₀ = 1, p₁ = ∞ of the Marcinkiewicz interpolation theorem, and it is the mechanism that turns the Hardy–Littlewood maximal inequality into the strong (p,p) bounds, item 9 of Lane B of the PDE roadmap.

The statements proved here

The analytic engine is stated in terms of the distribution functions of T f and of f. The operator-level theorem then derives its hypothesis from subadditivity, weak type (1,1), and an L^∞ bound. For each height t, these hypotheses produce the single inequality

t * ν {T f > t} ≤ d⁻¹ * A * ∫⁻ x in {‖f‖ > c * t}, ‖f‖ ∂μ,

which says that only the part of f above the height c * t can push T f above t. That inequality is the hypothesis of TauCeti.lintegral_rpow_le_of_mul_meas_ofReal_lt_le, and its conclusion is the L^p bound

∫⁻ (T f) ^ p ∂ν ≤ (p * c ^ (1 - p) / (p - 1)) * d⁻¹ * A * ∫⁻ ‖f‖ ^ p ∂μ.

Retaining this distributional lemma keeps the analytic engine usable even when T is not defined on a whole function space. The operator theorem lets μ and ν live on different spaces and makes the dependence on the endpoint and splitting constants explicit. Its constant blows up as p → 1, exactly as it must — an operator of weak type (1,1) need not be bounded on L¹.

The proof

The layer cake formula (TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul) converts both sides into integrals in the height variable t. The hypothesis, multiplied by t ^ (p - 2), bounds the integrand by A * t ^ (p - 2) * ∫⁻ x in {‖f‖ > c * t}, ‖f‖ ∂μ; Tonelli's theorem then exchanges the t and x integrations, and for each fixed x the inner integral is the elementary ∫⁻ t in (0, ‖f x‖ / c), t ^ (p - 2) = (‖f x‖ / c) ^ (p - 1) / (p - 1), evaluated by TauCeti.lintegral_indicator_ofReal_rpow_Ioi, which reassembles into c ^ (1 - p) / (p - 1) * ‖f x‖ ^ p. Convergence of that inner integral at the origin is where 1 < p is used, and it is why the constant carries the factor 1 / (p - 1).

Tonelli's theorem needs μ to be s-finite, but the statement does not: both sides ignore the part of μ outside {f > 0}, and once ∫⁻ f ^ p ∂μ is finite that part is σ-finite, being exhausted by the level sets {f ≥ 1 / (n + 1)}, each of finite measure by Chebyshev.

Main declarations

• TauCeti.lintegral_rpow_le_of_mul_meas_ofReal_lt_le: the interpolation estimate.
• TauCeti.mul_meas_ofReal_lt_le_setLIntegral: the reusable truncation argument from subadditivity and the two endpoint bounds.
• TauCeti.lintegral_rpow_le_of_mul_meas_lt_le_of_le_eLpNormEssSup: operator-level Marcinkiewicz interpolation.

References

• L. Grafakos, Classical Fourier Analysis, Theorem 1.3.1.
• E. Stein, Singular Integrals and Differentiability Properties of Functions, Chapter I, §4.

theorem TauCeti.lintegral_rpow_le_of_mul_meas_ofReal_lt_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → ENNReal} {u : β → ENNReal} {p c : ℝ} {A : ENNReal} (hf : AEMeasurable f μ) (hu : AEMeasurable u ν) (hp : 1 < p) (hc : 0 < c) (h : ∀ (t : ℝ), 0 < t → ENNReal.ofReal t * ν {y : β | ENNReal.ofReal t < u y} ≤ A * ∫⁻ (x : α) in {x : α | ENNReal.ofReal (c * t) < f x}, f x ∂μ) : ∫⁻ (y : β), u y ^ p ∂ν ≤ ENNReal.ofReal (p * c ^ (1 - p) / (p - 1)) * A * ∫⁻ (x : α), f x ^ p ∂μ

Marcinkiewicz interpolation, the diagonal case p₀ = 1, p₁ = ∞, in distributional form.

If for every height t > 0 the superlevel set {u > t} obeys the weak-type bound

t * ν {u > t} ≤ A * ∫⁻ x in {f > c * t}, f ∂μ

against the part of f above c * t, then for every 1 < p < ∞

∫⁻ u ^ p ∂ν ≤ (p * c ^ (1 - p) / (p - 1)) * A * ∫⁻ f ^ p ∂μ.

Applied with u = T f for a sublinear T, the hypothesis is what the weak (1,1) and L^∞ endpoint bounds for T give after splitting f at the height c * t, and the conclusion is the strong type (p,p) bound. The constant degenerates as p → 1, as it must.

theorem TauCeti.mul_meas_ofReal_lt_le_setLIntegral {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {c : ℝ} {A : ENNReal} {G : Type u_3} [MeasurableSpace G] [TopologicalSpace G] [OpensMeasurableSpace G] [ESeminormedAddMonoid G] {T : (α → G) → β → ENNReal} {v : α → G} {b d t : ℝ} (hv : AEMeasurable v μ) (ht : 0 < t) (hb : 0 ≤ b) (hc : 0 < c) (hd : 0 < d) (hbcd : b * c + d ≤ 1) (hadd : ∀ (g h : α → G), AEMeasurable g μ → AEMeasurable h μ → T (g + h) ≤ᵐ[ν] T g + T h) (hweak : ∀ (g : α → G), AEMeasurable g μ → ∀ (s : ENNReal), s * ν {y : β | s < T g y} ≤ A * ∫⁻ (x : α), ‖g x‖ₑ ∂μ) (hinfty : ∀ (g : α → G), AEMeasurable g μ → T g ≤ᵐ[ν] fun (x : β) => ENNReal.ofReal b * MeasureTheory.eLpNormEssSup g μ) : ENNReal.ofReal t * ν {y : β | ENNReal.ofReal t < T v y} ≤ ENNReal.ofReal d⁻¹ * A * ∫⁻ (x : α) in {x : α | ENNReal.ofReal (c * t) < ‖v x‖ₑ}, ‖v x‖ₑ ∂μ

The reusable operator-level truncation argument for Marcinkiewicz interpolation.

Suppose T is subadditive, is of weak type (1,1) with constant A, and obeys the L^∞ bound T g ≤ b · ‖g‖_∞. Split v according to whether its extended norm exceeds c * t. If b * c + d ≤ 1, then the low part contributes at most b * c * t, so T v > t forces the image of the high part to exceed d * t. Applying the weak-type bound to that high part gives

t * ν {T v > t} ≤ d⁻¹ * A * ∫⁻ x in {‖v‖ₑ > c * t}, ‖v x‖ₑ ∂μ.

The parameters c and d expose the choice of truncation rather than fixing the customary c = d = 1 / 2 for a normalized L^∞ bound.

theorem TauCeti.lintegral_rpow_le_of_mul_meas_lt_le_of_le_eLpNormEssSup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {p c : ℝ} {A : ENNReal} {G : Type u_3} [MeasurableSpace G] [TopologicalSpace G] [OpensMeasurableSpace G] [ESeminormedAddMonoid G] {T : (α → G) → β → ENNReal} {v : α → G} {b d : ℝ} (hv : AEMeasurable v μ) (hTv : AEMeasurable (T v) ν) (hp : 1 < p) (hb : 0 ≤ b) (hc : 0 < c) (hd : 0 < d) (hbcd : b * c + d ≤ 1) (hadd : ∀ (g h : α → G), AEMeasurable g μ → AEMeasurable h μ → T (g + h) ≤ᵐ[ν] T g + T h) (hweak : ∀ (g : α → G), AEMeasurable g μ → ∀ (s : ENNReal), s * ν {y : β | s < T g y} ≤ A * ∫⁻ (x : α), ‖g x‖ₑ ∂μ) (hinfty : ∀ (g : α → G), AEMeasurable g μ → T g ≤ᵐ[ν] fun (x : β) => ENNReal.ofReal b * MeasureTheory.eLpNormEssSup g μ) : ∫⁻ (y : β), T v y ^ p ∂ν ≤ ENNReal.ofReal (p * c ^ (1 - p) / (p - 1)) * (ENNReal.ofReal d⁻¹ * A) * ∫⁻ (x : α), ‖v x‖ₑ ^ p ∂μ

Marcinkiewicz interpolation at operator level, between weak type (1,1) and L^∞.

This packages the operator-specific truncation step: a subadditive operator with weak-type constant A and L^∞ constant b is strong type (p,p) for 1 < p < ∞. The positive splitting parameters c, d may be chosen arbitrarily subject to b * c + d ≤ 1.