This should roughly contain the contents of chapter 9.
Lemma 9.0.2
The Hardy-Littlewood maximal function w.r.t. a collection of balls 𝓑. M_{𝓑, p} in the blueprint.
Equations
- maximalFunction μ 𝓑 c r p u x = (⨆ i ∈ 𝓑, (Metric.ball (c i) (r i)).indicator (fun (x : X) => ⨍⁻ (y : X) in Metric.ball (c i) (r i), ↑‖u y‖₊ ^ p ∂μ) x) ^ p⁻¹
Instances For
The Hardy-Littlewood maximal function w.r.t. a collection of balls 𝓑 with exponent 1. M_𝓑 in the blueprint.
Equations
- MB μ 𝓑 c r u x = maximalFunction μ 𝓑 c r 1 u x
Instances For
Special case of equation (2.0.44). The proof is given between (9.0.12) and (9.0.34). Use the real interpolation theorem instead of following the blueprint.
Equation (2.0.44). The proof is given between (9.0.34) and (9.0.36).
The transformation M
characterized in Proposition 2.0.6.
p
is 1
in the blueprint, and globalMaximalFunction μ p u = (M (u ^ p)) ^ p⁻¹
Equations
Instances For
Equation (2.0.45).
Equation (2.0.46).
Easy from hasStrongType_maximalFunction
. Ideally prove separately
HasStrongType.const_smul
and HasStrongType.const_mul
.