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 continuous_average_ball {X : Type u_1} {E : Type u_2} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] {f : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) : ContinuousOn (fun (x : X × ℝ) => ⨍⁻ (y : X) in Metric.ball x.1 x.2, ‖f y‖ₑ ∂μ) (Set.univ ×ˢ Set.Ioi 0)

Use the dominated convergence theorem e.g. [Folland, Real Analysis. Modern Techniques and Their Applications, Lemma 3.16]

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 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).toReal) ⊤ ⊤ μ μ 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 HasWeakType.MB_one_toReal {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)

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 μ

@[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_def (A 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𝓑 : 𝓑.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)

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

Equation (2.0.44). The proof is given between (9.0.34) and (9.0.36).

theorem hasStrongType_maximalFunction_todo {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) (hp₁ : 1 ≤ 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 : ι → ℝ} (hf : MeasureTheory.LocallyIntegrable f μ) : LowerSemicontinuous (MB μ 𝓑 c r f)

Use lowerSemicontinuous_iff_isOpen_preimage and continuous_average_ball

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] [Nonempty X] [μ.IsOpenPosMeasure] {p₁ p₂ : NNReal} (h𝓑 : 𝓑.Countable) (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ ≤ p₂) : MeasureTheory.HasWeakType (fun (u : X → E) (x : X) => maximalFunction μ 𝓑 c r (↑p₁) u x) (↑p₂) (↑p₂) μ μ (A ^ 2)

hasStrongType_maximalFunction minus the assumption hR, but where p₁ = p₂ is possible and we only conclude a weak-type estimate. The proof of this should be basically the same as that of hasStrongType_maximalFunction + hasStrongType_maximalFunction_todo, but starting with HasWeakType.MB_one instead of hasStrongType_MB. (For p₂ > p₁ you can also derive this from hasStrongType_maximalFunction_todo)

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).

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 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 μ] [Nonempty X] [μ.IsOpenPosMeasure] {p₁ p₂ : NNReal} (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂) : MeasureTheory.HasStrongType (fun (u : X → E) (x : X) => (globalMaximalFunction μ (↑p₁) u x).toReal) (↑p₂) (↑p₂) μ μ (C2_0_6' A p₁ p₂)

Equation (2.0.46). Easy from hasStrongType_maximalFunction. Ideally prove separately HasStrongType.const_smul and HasStrongType.const_mul.

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 μ] [Nonempty X] [μ.IsOpenPosMeasure] {p₁ p₂ : NNReal} (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ ≤ p₂) : MeasureTheory.HasWeakType (fun (u : X → E) (x : X) => (globalMaximalFunction μ (↑p₁) u x).toReal) (↑p₂) (↑p₂) μ μ (A ^ 4)

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] (hf : MeasureTheory.LocallyIntegrable f μ) : LowerSemicontinuous (globalMaximalFunction μ 1 f)

Use lowerSemiContinuous_MB