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

Lemma 9.0.2

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

theorem exists_ball_subset_ball_two {X : Type u_1} [PseudoMetricSpace X] [TopologicalSpace.SeparableSpace X] (c : X) {r : ℝ} (hr : 0 < r) : ∃ c' ∈ ⋯.choose, ∃ (m : ℤ), Metric.ball c r ⊆ Metric.ball c' (2 ^ m) ∧ 2 ^ m ≤ 2 * r ∧ Metric.ball c' (2 ^ m) ⊆ Metric.ball c (4 * r)

theorem lowerSemiContinuousOn_integral_ball {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {f : X → E} [OpensMeasurableSpace X] (hf2 : MeasureTheory.AEStronglyMeasurable f μ) : LowerSemicontinuousOn (fun (x : X × ℝ) => ∫⁻ (y : X) in Metric.ball x.1 x.2, ‖f y‖ₑ ∂μ) (Set.univ ×ˢ Set.Ioi 0)

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 MB_def {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {f : X → E} {x : X} {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} : MB μ 𝓑 c r f x = ⨆ i ∈ 𝓑, (Metric.ball (c i) (r i)).indicator (fun (x : X) => ⨍⁻ (y : X) in Metric.ball (c i) (r i), ‖f y‖ₑ ∂μ) x

theorem maximalFunction_eq_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 : ι → ℝ} {p : ℝ} {u : X → E} {x : X} (hp : 0 ≤ p) : maximalFunction μ 𝓑 c r p u x = MB μ 𝓑 c r (fun (x : X) => ‖u x‖ ^ p) x ^ p⁻¹

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

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

theorem continuous_integral_ball {X : Type u_1} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] (g : X → ENNReal) (hg : ∀ (x : X), ∀ r > 0, ∫⁻ (y : X) in Metric.ball x r, g y ∂μ < ⊤) (hg2 : AEMeasurable g μ) (hμ : ∀ (z : X), ∀ r > 0, μ (Metric.sphere z r) = 0) : ContinuousOn (fun (x : X × ℝ) => ∫⁻ (y : X) in Metric.ball x.1 x.2, g y ∂μ) (Set.univ ×ˢ Set.Ioi 0)

theorem continuous_average_ball {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {f : X → E} [μ.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [OpensMeasurableSpace X] [ProperSpace X] (hf : MeasureTheory.LocallyIntegrable f μ) (hμ : ∀ (z : X), ∀ r > 0, μ (Metric.sphere z r) = 0) : ContinuousOn (fun (x : X × ℝ) => ⨍⁻ (y : X) in Metric.ball x.1 x.2, ‖f y‖ₑ ∂μ) (Set.univ ×ˢ Set.Ioi 0)

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

theorem NNReal.smul_ennreal_eq_mul (x : NNReal) (y : ENNReal) : x • y = ↑x * y

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] {μ : Measure X} [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [BorelSpace X] {p : ℝ} {u : X → E} (h𝓑 : 𝓑.Countable) : AEStronglyMeasurable (maximalFunction μ 𝓑 c r p u) μ

theorem MeasureTheory.AEStronglyMeasurable.maximalFunction_toReal {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : Measure X} [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [BorelSpace X] {p : ℝ} {u : X → E} (h𝓑 : 𝓑.Countable) : 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) ⊤ ⊤ μ μ 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 (MB μ 𝓑 c r) 1 1 μ μ (↑A ^ 2)

theorem MB_ae_ne_top {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) {u : X → E} (hu : MeasureTheory.MemLp u 1 μ) : ∀ᵐ (x : X) ∂μ, MB μ 𝓑 c r u x ≠ ⊤

theorem MeasureTheory.MemLp.eLpNormEssSup_lt_top {E : Type u_2} [NormedAddCommGroup E] {α : Type u_4} [MeasurableSpace α] {μ : Measure α} {u : α → E} (hu : MemLp u ⊤ μ) : eLpNormEssSup u μ < ⊤

theorem MB_ae_ne_top' {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) ⦃u : X → E⦄ (hu : MeasureTheory.MemLp u ⊤ μ ∨ MeasureTheory.MemLp u 1 μ) : ∀ᵐ (x : X) ∂μ, MB μ 𝓑 c r u x ≠ ⊤

theorem MeasureTheory.AESublinearOn.maximalFunction {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [IsFiniteMeasureOnCompacts μ] [ProperSpace X] (h𝓑 : 𝓑.Countable) {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) : AESublinearOn (fun (u : X → E) (x : X) => MB μ 𝓑 c r u x) (fun (f : X → E) => MemLp f ⊤ μ ∨ MemLp f 1 μ) 1 μ

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

@[irreducible]

def CMB (A p : NNReal) : NNReal

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

Equations

• CMB A p = MeasureTheory.C_realInterpolation ⊤ 1 ⊤ 1 (↑p) 1 (A ^ 2) 1 (↑p)⁻¹

theorem CMB_eq_of_one_lt_q {b q : NNReal} (hq : 1 < q) : CMB b q = 2 * (q / (q - 1) * b ^ 2) ^ (↑q)⁻¹

theorem CMB_defaultA_two_eq {a : ℕ} : CMB (↑(defaultA a)) 2 = 2 ^ (↑a + 3 / 2)

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𝓑 : 𝓑.Countable) {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) {p : NNReal} (hp : 1 < p) : MeasureTheory.HasStrongType (fun (u : X → E) (x : X) => MB μ 𝓑 c r u x) (↑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_MB_finite {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) (↑p) (↑p) μ μ ↑(CMB A p)

@[irreducible]

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

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

Equations

• C2_0_6 A p₁ p₂ = CMB A (p₂ / p₁) ^ (↑p₁)⁻¹

theorem C2_0_6_def (A p₁ p₂ : NNReal) : C2_0_6 A p₁ p₂ = CMB A (p₂ / p₁) ^ (↑p₁)⁻¹

theorem hasStrongType_maximalFunction_aux {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] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [ProperSpace X] [Nonempty X] [μ.IsOpenPosMeasure] {p₁ p₂ : NNReal} (h𝓑 : 𝓑.Countable) {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) (hp₁ : 0 < p₁) (hp₁₂ : p₁ < p₂) : MeasureTheory.HasStrongType (fun (u : X → E) (x : X) => maximalFunction μ 𝓑 c r (↑p₁) u x) (↑p₂) (↑p₂) μ μ ↑(C2_0_6 A p₁ p₂)

Equation (2.0.44). The proof is given between (9.0.34) and (9.0.36). This is a special case of hasStrongType_maximalFunction below, which doesn't have the assumption hR (but uses this result in its proof).

def tr {ι : Type u_3} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) (k : ℕ) : Set ι

Equations

• tr h𝓑 k = (fun (g : ↑𝓑 → ℕ) (hg : Function.Injective g) => Subtype.val '' (g ⁻¹' {x : ℕ | x ≤ k})) (Classical.choose ⋯) ⋯

theorem tr_finite {ι : Type u_3} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) (k : ℕ) : (tr h𝓑 k).Finite

theorem tr_radius_bound {ι : Type u_3} {r : ι → ℝ} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) (k : ℕ) : ∃ (R : ℝ), ∀ i ∈ tr h𝓑 k, r i ≤ R

def maximalFunction_seq {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] [NormedAddCommGroup E] {ι : Type u_3} (μ : MeasureTheory.Measure X) {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) (c : ι → X) (r : ι → ℝ) (q : ℝ) (v : X → E) (k : ℕ) (z : X) : ENNReal

Equations

• maximalFunction_seq μ h𝓑 c r q v k z = maximalFunction μ (tr h𝓑 k) c r q v z

theorem maximalFunction_seq_mono {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {ι : Type u_3} {c : ι → X} {r : ι → ℝ} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) {p : NNReal} (hp : 0 < p) (u : X → E) : Monotone (maximalFunction_seq μ h𝓑 c r (↑p) u)

theorem maximalFunction_seq_eq {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {ι : Type u_3} {c : ι → X} {r : ι → ℝ} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) {p : NNReal} (hp : 0 < p) (u : X → E) (x : X) : maximalFunction μ 𝓑 c r (↑p) u x = ⨆ (k : ℕ), maximalFunction_seq μ h𝓑 c r (↑p) u k x

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 : ι → ℝ} [BorelSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [ProperSpace X] [μ.IsOpenPosMeasure] {p₁ p₂ : NNReal} (h𝓑 : 𝓑.Countable) (hp₁ : 0 < p₁) (hp₁₂ : p₁ < p₂) : MeasureTheory.HasStrongType (fun (u : X → E) (x : X) => maximalFunction μ 𝓑 c r (↑p₁) u x) (↑p₂) (↑p₂) μ μ ↑(C2_0_6 A p₁ p₂)

hasStrongType_maximalFunction minus the assumption hR. A proof for basically this result is given in Chapter 9, everything following after equation (9.0.36).

theorem lowerSemiContinuous_MB {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {f : X → E} {ι : Type u_3} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} : LowerSemicontinuous (MB μ 𝓑 c r f)

theorem hasWeakType_maximalFunction_equal_exponents₀ {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] {p : NNReal} (h𝓑 : 𝓑.Countable) {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) (hp : 0 < p) : MeasureTheory.HasWeakType (fun (u : X → E) (x : X) => maximalFunction μ 𝓑 c r (↑p) u x) (↑p) (↑p) μ μ (↑A ^ (2 / ↑p))

theorem hasWeakType_maximalFunction_equal_exponents {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] {p : NNReal} (h𝓑 : 𝓑.Countable) (hp : 0 < p) : MeasureTheory.HasWeakType (fun (u : X → E) (x : X) => maximalFunction μ 𝓑 c r (↑p) u x) (↑p) (↑p) μ μ (↑A ^ (2 / ↑p))

def C_weakType_maximalFunction (A p₁ p₂ : NNReal) : ENNReal

Equations

• C_weakType_maximalFunction A p₁ p₂ = if p₁ = p₂ then ↑A ^ (2 / ↑p₁) else ↑(C2_0_6 A p₁ p₂)

theorem C_weakType_maximalFunction_lt_top {A p₁ p₂ : NNReal} : C_weakType_maximalFunction A p₁ p₂ < ⊤

theorem hasWeakType_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 : ι → ℝ} [BorelSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [ProperSpace X] [μ.IsOpenPosMeasure] {p₁ p₂ : NNReal} (h𝓑 : 𝓑.Countable) (hp₁ : 0 < p₁) (hp₁₂ : p₁ ≤ p₂) : MeasureTheory.HasWeakType (fun (u : X → E) (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.

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 (x : X × ℤ) => x.1) (fun (x : X × ℤ) => 2 ^ x.2) p u x

theorem MeasureTheory.AEStronglyMeasurable.globalMaximalFunction {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] [ProperSpace X] [BorelSpace X] {p : ℝ} {u : X → E} : 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] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] {u : X → E} {z x : X} {r : ℝ} (h : dist x z < r) : ⨍⁻ (y : X) in Metric.ball z r, ‖u y‖ₑ ∂μ ≤ globalMaximalFunction μ 1 u x

Equation (2.0.45)

theorem lintegral_ball_le_volume_globalMaximalFunction {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] {u : X → E} {z x : X} {r : ℝ} (h : dist x z < r) : ∫⁻ (y : X) in Metric.ball z r, ‖u y‖ₑ ∂μ ≤ μ (Metric.ball z r) * globalMaximalFunction μ 1 u x

def C2_0_6' (A p₁ 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 C2_0_6'_defaultA_one_two_eq {a : ℕ} : C2_0_6' (↑(defaultA a)) 1 2 = 2 ^ (3 * ↑a + 3 / 2)

theorem C2_0_6'_defaultA_one_le {a : ℕ} {q : NNReal} (hq : 1 < q) : C2_0_6' (↑(defaultA a)) 1 q ≤ 2 ^ (4 * a + 1) * (q / (q - 1))

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] [BorelSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] {p₁ p₂ : NNReal} (hp₁ : 0 < p₁) (hp₁₂ : p₁ < p₂) : MeasureTheory.HasStrongType (globalMaximalFunction μ ↑p₁) (↑p₂) (↑p₂) μ μ ↑(C2_0_6' A p₁ p₂)

Equation (2.0.46). Easy from hasStrongType_maximalFunction

def C_weakType_globalMaximalFunction (A p₁ p₂ : NNReal) : ENNReal

Equations

• C_weakType_globalMaximalFunction A p₁ p₂ = ↑A ^ 2 * C_weakType_maximalFunction A p₁ p₂

theorem C_weakType_globalMaximalFunction_lt_top {A p₁ p₂ : NNReal} : C_weakType_globalMaximalFunction A p₁ p₂ < ⊤

theorem hasWeakType_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] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] {p₁ p₂ : NNReal} (hp₁ : 0 < p₁) (hp₁₂ : p₁ ≤ p₂) : MeasureTheory.HasWeakType (globalMaximalFunction μ ↑p₁) (↑p₂) (↑p₂) μ μ (C_weakType_globalMaximalFunction A p₁ p₂)

theorem lowerSemiContinuous_globalMaximalFunction {X : Type u_1} {E : Type u_2} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] {f : X → E} [ProperSpace X] : LowerSemicontinuous (globalMaximalFunction μ 1 f)

Use lowerSemiContinuous_MB

theorem globalMaximalFunction_ae_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] [BorelSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] {p₁ p₂ : NNReal} (hp₁ : 0 < p₁) (hp₁₂ : p₁ < p₂) {u : X → E} (hu : MeasureTheory.MemLp u (↑p₂) μ) : ∀ᵐ (x : X) ∂μ, globalMaximalFunction μ (↑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₁ : 0 < p) {u : X → E} (hu : MeasureTheory.MemLp u ⊤ μ) {x : X} : globalMaximalFunction μ (↑p) u x < ⊤