Superlevel sets and weak-type bounds #
Two elementary facts about the superlevel sets {y | ofReal t < T v y} of an operator T that
are used in Marcinkiewicz interpolation but need no interpolation theory.
Main statements #
TauCeti.setOf_ofReal_lt_ae_le_union: ifT v ≤ T g₁ + T g₂almost everywhere andd + e ≤ 1, the superlevel set ofT vis almost everywhere covered by those ofT g₁andT g₂.TauCeti.meas_ofReal_lt_le_of_weak: a weak-type bound at the heightrbounds the measure of the superlevel set at that height.
theorem
TauCeti.setOf_ofReal_lt_ae_le_union
{α : Type u_1}
{β : Type u_2}
{G : Type u_3}
{T : (α → G) → β → ENNReal}
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
{v g₁ g₂ : α → G}
{d e t : ℝ}
(ht : 0 ≤ t)
(hd : 0 ≤ d)
(he : 0 ≤ e)
(hde : d + e ≤ 1)
(hTv : T v ≤ᵐ[ν] T g₁ + T g₂)
:
If T v ≤ T g₁ + T g₂ almost everywhere and d + e ≤ 1, then the superlevel set of T v at
the height t is almost everywhere covered by the superlevel set of T g₁ at the height d * t
and that of T g₂ at the height e * t.
theorem
TauCeti.meas_ofReal_lt_le_of_weak
{α : Type u_1}
{β : Type u_2}
{G : Type u_3}
{T : (α → G) → β → ENNReal}
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
{w : α → G}
{q r : ℝ}
{B : ENNReal}
(hr : 0 < r)
(hweak : ENNReal.ofReal r ^ q * ν {y : β | ENNReal.ofReal r < T w y} ≤ B)
:
A weak-type bound at the height r bounds the measure of the superlevel set at that height:
r ^ q * ν {T w > r} ≤ B gives ν {T w > r} ≤ r ^ (-q) * B. The right side B is arbitrary, so
the same step serves weak-type bounds of any form, such as A * ∫⁻ ‖w‖ₑ ^ p or
A * (∫⁻ ‖w‖ₑ ^ p) ^ (q / p).