This should roughly contain the contents of chapter 9.
noncomputable def
maximalFunction
{X : Type u_1}
{Īµ : Type u_2}
[PseudoMetricSpace X]
[MeasurableSpace X]
[ENorm Īµ]
{Ī¹ : Type u_4}
(Ī¼ : MeasureTheory.Measure X)
(š : Set Ī¹)
(c : Ī¹ ā X)
(r : Ī¹ ā ā)
(p : ā)
(u : X ā Īµ)
(x : X)
:
The uncentered Hardy-Littlewood maximal function, for a family of balls.
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 āĪ¼) ^ pā»Ā¹) x
Instances For
noncomputable def
globalMaximalFunction
{X : Type u_1}
{Īµ : Type u_2}
[PseudoMetricSpace X]
[MeasurableSpace X]
[ENorm Īµ]
(Ī¼ : MeasureTheory.Measure X)
(p : ā)
(u : X ā Īµ)
(x : X)
:
The uncentered Hardy-Littlewood maximal function.
Equations
- globalMaximalFunction Ī¼ p u x = maximalFunction Ī¼ Set.univ (fun (x : X Ć ā) => x.1) (fun (x : X Ć ā) => x.2) p u x
Instances For
theorem
laverage_le_globalMaximalFunction
{X : Type u_1}
{Īµ : Type u_2}
[PseudoMetricSpace X]
[MeasurableSpace X]
[ENorm Īµ]
{Ī¼ : MeasureTheory.Measure X}
{u : X ā Īµ}
{x z : X}
{r : ā}
(h : dist x z < r)
:
The average of the norm of a function over a particular ball is smaller than the value of the
globalMaximalFuntion at a point inside that ball.
theorem
lintegral_ball_le_volume_mul_globalMaximalFunction
{X : Type u_1}
{Īµ : Type u_2}
[PseudoMetricSpace X]
[MeasurableSpace X]
[ENorm Īµ]
{Ī¼ : MeasureTheory.Measure X}
{u : X ā Īµ}
{x : X}
[ProperSpace X]
[MeasureTheory.IsFiniteMeasureOnCompacts Ī¼]
{z : X}
{r : ā}
(h : dist x z < r)
:
ā«ā» (y : X) in Metric.ball z r, āu yāā āĪ¼ ā¤ Ī¼ (Metric.ball z r) * globalMaximalFunction Ī¼ 1 u x
The integral of the norm of a function over a particular ball is smaller than the volume of the
ball times the value of the globalMaximalFuntion at a point inside that ball.
theorem
measure_biUnion_le_lintegral
{X : Type u_1}
{A : NNReal}
[PseudoMetricSpace X]
[MeasurableSpace X]
{Ī¼ : MeasureTheory.Measure X}
[Ī¼.IsDoubling A]
{Ī¹ : Type u_5}
{c : Ī¹ ā X}
{r : Ī¹ ā ā}
[OpensMeasurableSpace X]
[TopologicalSpace.SeparableSpace X]
(š : Set Ī¹)
(l : ENNReal)
(u : X ā ENNReal)
(h2u : ā i ā š, l * Ī¼ (Metric.ball (c i) (r i)) ā¤ ā«ā» (x : X) in Metric.ball (c i) (r i), u x āĪ¼)
:
theorem
lowerSemiContinuous_maximalFunction
{X : Type u_1}
{Īµ : Type u_2}
[PseudoMetricSpace X]
[MeasurableSpace X]
[ENorm Īµ]
{Ī¼ : MeasureTheory.Measure X}
{Ī¹ : Type u_4}
{š : Set Ī¹}
{c : Ī¹ ā X}
{r : Ī¹ ā ā}
{p : ā}
{u : X ā Īµ}
:
LowerSemicontinuous (maximalFunction Ī¼ š c r p u)
theorem
measurable_maximalFunction
{X : Type u_1}
{Īµ : Type u_2}
[PseudoMetricSpace X]
[MeasurableSpace X]
[ENorm Īµ]
{Ī¼ : MeasureTheory.Measure X}
{Ī¹ : Type u_4}
{š : Set Ī¹}
{c : Ī¹ ā X}
{r : Ī¹ ā ā}
{p : ā}
{u : X ā Īµ}
[BorelSpace X]
:
Measurable (maximalFunction Ī¼ š c r p u)
theorem
maximalFunction_one_le_eLpNormEssSup
{X : Type u_1}
{Īµ : Type u_2}
[PseudoMetricSpace X]
[MeasurableSpace X]
[ENorm Īµ]
{Ī¼ : MeasureTheory.Measure X}
{Ī¹ : Type u_4}
{š : Set Ī¹}
{c : Ī¹ ā X}
{r : Ī¹ ā ā}
{u : X ā Īµ}
{x : X}
:
theorem
hasStrongType_maximalFunction_one
{X : Type u_1}
{Īµ' : Type u_3}
{A : NNReal}
[PseudoMetricSpace X]
[MeasurableSpace X]
{Ī¼ : MeasureTheory.Measure X}
[Ī¼.IsDoubling A]
{Ī¹ : Type u_4}
{š : Set Ī¹}
{c : Ī¹ ā X}
{r : Ī¹ ā ā}
[TopologicalSpace Īµ']
[ESeminormedAddMonoid Īµ']
[SMul NNReal Īµ']
[ENormSMulClass NNReal Īµ']
[TopologicalSpace.PseudoMetrizableSpace Īµ']
[MeasurableSpace Īµ']
[BorelSpace Īµ']
[BorelSpace X]
[MeasureTheory.IsFiniteMeasureOnCompacts Ī¼]
[ProperSpace X]
[Ī¼.IsOpenPosMeasure]
{p : NNReal}
(hp : 1 < p)
:
MeasureTheory.HasStrongType (maximalFunction Ī¼ š c r 1) (āp) (āp) Ī¼ Ī¼ ā(CMB A p)
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.
theorem
hasStrongType_maximalFunction
{X : Type u_1}
{Īµ' : Type u_3}
{A : NNReal}
[PseudoMetricSpace X]
[MeasurableSpace X]
{Ī¼ : MeasureTheory.Measure X}
[Ī¼.IsDoubling A]
{Ī¹ : Type u_4}
{š : Set Ī¹}
{c : Ī¹ ā X}
{r : Ī¹ ā ā}
[TopologicalSpace Īµ']
[ContinuousENorm Īµ']
[BorelSpace X]
[MeasureTheory.IsFiniteMeasureOnCompacts Ī¼]
[ProperSpace X]
[Ī¼.IsOpenPosMeasure]
{pā pā : NNReal}
(hpā : 0 < pā)
(hpāā : pā < pā)
:
MeasureTheory.HasStrongType (maximalFunction Ī¼ š c r āpā) (āpā) (āpā) Ī¼ Ī¼ ā(C2_0_6 A pā pā)
The maximalFunction has strong type when pā < pā.
theorem
hasWeakType_maximalFunction
{X : Type u_1}
{Īµ' : Type u_3}
{A : NNReal}
[PseudoMetricSpace X]
[MeasurableSpace X]
{Ī¼ : MeasureTheory.Measure X}
[Ī¼.IsDoubling A]
{Ī¹ : Type u_4}
{š : Set Ī¹}
{c : Ī¹ ā X}
{r : Ī¹ ā ā}
[TopologicalSpace Īµ']
[ContinuousENorm Īµ']
[BorelSpace X]
[MeasureTheory.IsFiniteMeasureOnCompacts Ī¼]
[ProperSpace X]
[Ī¼.IsOpenPosMeasure]
{pā pā : NNReal}
(hpā : 0 < pā)
(hpāā : pā ā¤ pā)
:
MeasureTheory.HasWeakType (fun (u : X ā Īµ') (x : X) => maximalFunction Ī¼ š c r (āpā) u x) (āpā) (āpā) Ī¼ Ī¼
(C_weakType_maximalFunction A pā pā)
hasStrongType_maximalFunction minus the assumption hR, but where pā = pā is possible and
we only conclude a weak-type estimate.