This should roughly contain the contents of chapter 9.

theorem covering_separable_space (X : Type u_1) [PseudoMetricSpace X] [TopologicalSpace.SeparableSpace X] : ∃ (C : Set X), C.Countable ∧ ∀ r > 0, ⋃ c ∈ C, Metric.ball c r = Set.univ

theorem countable_globalMaximalFunction (X : Type u_1) [PseudoMetricSpace X] [TopologicalSpace.SeparableSpace X] : (⋯.choose ×ˢ Set.univ).Countable

def maximalFunction {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] [NormedAddCommGroup E] {ι : Type u_3} (μ : MeasureTheory.Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (p : ℝ) (u : X → E) (x : X) : ENNReal

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⁻¹

@[reducible, inline]

abbrev MB {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] [NormedAddCommGroup E] {ι : Type u_3} (μ : MeasureTheory.Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (u : X → E) (x : X) : ENNReal

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

theorem MeasureTheory.LocallyIntegrable.integrableOn_of_isBounded {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [ProperSpace X] {f : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) {s : Set X} (hs : Bornology.IsBounded s) : MeasureTheory.IntegrableOn f s μ

theorem MeasureTheory.LocallyIntegrable.integrableOn_ball {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [ProperSpace X] {f : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) {x : X} {r : ℝ} : MeasureTheory.IntegrableOn f (Metric.ball x r) μ

theorem MeasureTheory.LocallyIntegrable.laverage_ball_lt_top {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [BorelSpace X] [ProperSpace X] {f : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) {x₀ : X} {r : ℝ} : ⨍⁻ (x : X) in Metric.ball x₀ r, ↑‖f x‖₊ ∂μ < ⊤

theorem exists_disjoint_subfamily_covering_enlargement_closedBall' {ι : Type u_3} {α : Type u_4} [MetricSpace α] (t : Set ι) (x : ι → α) (r : ι → ℝ) (R : ℝ) (hr : ∀ a ∈ t, r a ≤ R) (τ : ℝ) (hτ : 3 < τ) : ∃ u ⊆ t, (u.PairwiseDisjoint fun (a : ι) => Metric.closedBall (x a) (r a)) ∧ ∀ a ∈ t, ∃ b ∈ u, Metric.closedBall (x a) (r a) ⊆ Metric.closedBall (x b) (τ * r b) ∧ ∀ u ∈ t, 0 ≤ r u → r a ≤ (τ - 1) / 2 * r b

theorem Vitali.exists_disjoint_subfamily_covering_enlargement_ball {ι : Type u_3} {α : Type u_4} [MetricSpace α] (t : Set ι) (x : ι → α) (r : ι → ℝ) (R : ℝ) (hr : ∀ a ∈ t, r a ≤ R) (τ : ℝ) (hτ : 3 < τ) : ∃ u ⊆ t, (u.PairwiseDisjoint fun (a : ι) => Metric.ball (x a) (r a)) ∧ ∀ a ∈ t, ∃ b ∈ u, Metric.ball (x a) (r a) ⊆ Metric.ball (x b) (τ * r b)

theorem Finset.exists_image_le {α : Type u_4} {β : Type u_5} [Nonempty β] [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] (s : Finset α) (f : α → β) : ∃ (b : β), ∀ a ∈ s, f a ≤ b

theorem Set.Finite.exists_image_le {α : Type u_4} {β : Type u_5} [Nonempty β] [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] {s : Set α} (hs : s.Finite) (f : α → β) : ∃ (b : β), ∀ a ∈ s, f a ≤ b

theorem Set.Countable.measure_biUnion_le_lintegral {X : Type u_1} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [OpensMeasurableSpace X] (h𝓑 : 𝓑.Countable) (l : ENNReal) (u : X → ENNReal) (R : ℝ) (hR : ∀ a ∈ 𝓑, r a ≤ R) (h2u : ∀ i ∈ 𝓑, l * μ (Metric.ball (c i) (r i)) ≤ ∫⁻ (x : X) in Metric.ball (c i) (r i), u x ∂μ) : l * μ (⋃ i ∈ 𝓑, Metric.ball (c i) (r i)) ≤ ↑A ^ 2 * ∫⁻ (x : X), u x ∂μ

theorem Finset.measure_biUnion_le_lintegral {X : Type u_1} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] {ι : Type u_3} {c : ι → X} {r : ι → ℝ} [OpensMeasurableSpace X] (𝓑 : Finset ι) (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 ∂μ) : l * μ (⋃ i ∈ 𝓑, Metric.ball (c i) (r i)) ≤ ↑A ^ 2 * ∫⁻ (x : X), u x ∂μ

theorem MeasureTheory.AEStronglyMeasurable.maximalFunction {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [BorelSpace X] {p : ℝ} {u : X → E} (h𝓑 : 𝓑.Countable) : MeasureTheory.AEStronglyMeasurable (maximalFunction μ 𝓑 c r p u) μ

theorem MeasureTheory.AEStronglyMeasurable.maximalFunction_toReal {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [BorelSpace X] {p : ℝ} {u : X → E} (h𝓑 : 𝓑.Countable) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => (maximalFunction μ 𝓑 c r p u x).toReal) μ

theorem MB_le_eLpNormEssSup {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} {u : X → E} {x : X} : MB μ 𝓑 c r u x ≤ MeasureTheory.eLpNormEssSup u μ

theorem HasStrongType.MB_top {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [BorelSpace X] (h𝓑 : 𝓑.Countable) : MeasureTheory.HasStrongType (fun (u : X → E) (x : X) => (MB μ 𝓑 c r u x).toReal) ⊤ ⊤ μ μ 1

theorem MeasureTheory.SublinearOn.maximalFunction {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [ProperSpace X] (h𝓑 : 𝓑.Finite) : MeasureTheory.SublinearOn (fun (u : X → E) (x : X) => (MB μ 𝓑 c r u x).toReal) (fun (f : X → E) => MeasureTheory.Memℒp f ⊤ μ ∨ MeasureTheory.Memℒp f 1 μ) 1

theorem HasWeakType.MB_one {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.IsDoubling A] [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [BorelSpace X] (h𝓑 : 𝓑.Countable) {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) : MeasureTheory.HasWeakType (fun (u : X → E) (x : X) => (MB μ 𝓑 c r u x).toReal) 1 1 μ μ (A ^ 2)

@[irreducible]

def CMB (A : NNReal) (p : NNReal) : NNReal

The constant factor in the statement that M_𝓑 has strong type.

Equations

• CMB = wrapped✝.1

theorem CMB_def (A : NNReal) (p : NNReal) : CMB A p = MeasureTheory.C_realInterpolation ⊤ 1 ⊤ 1 (↑p) 1 (A ^ 2) 1 (↑p)⁻¹

theorem hasStrongType_MB {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [ProperSpace X] [Nonempty X] [μ.IsOpenPosMeasure] (h𝓑 : 𝓑.Finite) {p : NNReal} (hp : 1 < p) : MeasureTheory.HasStrongType (fun (u : X → E) (x : X) => (MB μ 𝓑 c r u x).toReal) (↑p) (↑p) μ μ (CMB A p)

@[irreducible]

def C2_0_6 (A : NNReal) (p₁ : NNReal) (p₂ : NNReal) : NNReal

The constant factor in the statement that M_{𝓑, p} has strong type.

Equations

• C2_0_6 = wrapped✝.1

theorem C2_0_6_def (A : NNReal) (p₁ : NNReal) (p₂ : NNReal) : C2_0_6 A p₁ p₂ = sorryAx NNReal

theorem hasStrongType_maximalFunction {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} {p₁ : NNReal} {p₂ : NNReal} (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂) {u : X → E} (hu : MeasureTheory.AEStronglyMeasurable u μ) : MeasureTheory.HasStrongType (fun (u : X → E) (x : X) => (maximalFunction μ 𝓑 c r (↑p₁) u x).toReal) (↑p₂) (↑p₂) μ μ (C2_0_6 A p₁ p₂)

def globalMaximalFunction {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] (μ : MeasureTheory.Measure X) [NormedAddCommGroup E] [ProperSpace X] [μ.IsDoubling A] (p : ℝ) (u : X → E) (x : X) : ENNReal

The transformation M characterized in Proposition 2.0.6. p is 1 in the blueprint, and globalMaximalFunction μ p u = (M (u ^ p)) ^ p⁻¹

Equations

• globalMaximalFunction μ p u x = ↑A ^ 2 * maximalFunction μ (⋯.choose ×ˢ Set.univ) (fun (z : X × ℤ) => z.1) (fun (z : X × ℤ) => 2 ^ z.2) p u x

theorem globalMaximalFunction_lt_top {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] [ProperSpace X] {p : NNReal} (hp₁ : 1 ≤ p) {u : X → E} (hu : MeasureTheory.AEStronglyMeasurable u μ) (hu : Bornology.IsBounded (Set.range u)) {x : X} : globalMaximalFunction μ (↑p) u x < ⊤

theorem MeasureTheory.AEStronglyMeasurable.globalMaximalFunction {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] [ProperSpace X] [BorelSpace X] {p : ℝ} {u : X → E} : MeasureTheory.AEStronglyMeasurable (globalMaximalFunction μ p u) μ

theorem laverage_le_globalMaximalFunction {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] [ProperSpace X] {u : X → E} (hu : MeasureTheory.AEStronglyMeasurable u μ) (hu : Bornology.IsBounded (Set.range u)) {z : X} {x : X} {r : ℝ} (h : dist x z < r) : ⨍⁻ (y : X) in Metric.ball z r, ↑‖u y‖₊ ∂μ ≤ globalMaximalFunction μ 1 u x

def C2_0_6' (A : NNReal) (p₁ : NNReal) (p₂ : NNReal) : NNReal

The constant factor in the statement that M has strong type.

Equations

• C2_0_6' A p₁ p₂ = A ^ 2 * C2_0_6 A p₁ p₂

theorem hasStrongType_globalMaximalFunction {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] [ProperSpace X] {p₁ : NNReal} {p₂ : NNReal} (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂) {u : X → ℂ} (hu : MeasureTheory.AEStronglyMeasurable u μ) (hu : Bornology.IsBounded (Set.range u)) {z : X} {x : X} {r : ℝ} : MeasureTheory.HasStrongType (fun (u : X → E) (x : X) => (globalMaximalFunction μ (↑p₁) u x).toReal) (↑p₂) (↑p₂) μ μ (C2_0_6' A p₁ p₂)