hasWeakType_maximalFunction_one

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. -/ public theorem lintegral_ball_le_volume_mul_globalMaximalFunction [ProperSpace X] [IsFiniteMeasureOnCompacts μ] {z : X} {r : ℝ} (h : dist x z < r) : ∫⁻ y in ball z r, ‖u y‖ₑ ∂μ ≤ μ (ball z r) * globalMaximalFunction μ 1 u x := by have : IsFiniteMeasure (μ.restrict (ball z r)) := isFiniteMeasure_restrict.mpr (by finiteness) rw [← measure_mul_laverage] simp only [MeasurableSet.univ, Measure.restrict_apply, univ_inter] gcongr exact laverage_le_globalMaximalFunction h

lemma indicator_rpow {α : Type*} {p : ℝ} (hp : 0 < p) {s : Set α} {f : α → ℝ≥0∞} : s.indicator (fun y ↦ f y ^ p) = (s.indicator f) ^ p := indicator_comp_of_zero (g := fun a => a ^ p) (ENNReal.zero_rpow_of_pos hp)

lemma maximalFunction_eq_maximalFunction_one_rpow (hp : 0 < p) : maximalFunction μ 𝓑 c r p u x = (maximalFunction μ 𝓑 c r 1 (‖u ·‖ ^ p) x) ^ p⁻¹ := by simp only [maximalFunction, indicator_rpow (inv_pos_of_pos hp), Pi.pow_apply, rpow_one, inv_one, iSup_rpow (inv_pos_of_pos hp)] congr! 8 rw [Real.enorm_rpow_of_nonneg (by positivity) hp.le, enorm_norm]

-- The average that appears in the definition of MB variable (μ c r) in private def T (i : ι) (u : X → E) := ⨍⁻ (y : X) in ball (c i) (r i), ‖u y‖ₑ ∂μ

-- We replace the criterion P used in MeasureTheory.AESublinearOn.maximalFunction with the -- weaker criterion AEMeasurable that is closed under addition and scalar multiplication.

private lemma T.add_le [MeasurableSpace E] [BorelSpace E] {i} {f g : X → E} (hf : AEMeasurable f μ) : ‖T μ c r i (f + g)‖ₑ ≤ ‖T μ c r i f‖ₑ + ‖T μ c r i g‖ₑ := by simp only [T, Pi.add_apply, enorm_eq_self] rw [← laverage_add_left hf.restrict.enorm] exact laverage_mono (fun x ↦ enorm_add_le (f x) (g x))

-- move to ENNReal.Basic or similar lemma NNReal.smul_ennreal_eq_mul (x : ℝ≥0) (y : ℝ≥0∞) : x • y = x * y := rfl

private lemma T.smul [NormedSpace ℝ E] {c r} {i : ι} {d : ℝ≥0} : T μ c r i (d • u) = d • T μ c r i u := by simp [T, NNReal.smul_def, NNReal.smul_ennreal_eq_mul, laverage_const_mul (by finiteness), enorm_smul]

section MeasureBiUnionBall

variable {ι : Type*} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ}

theorem measure_biUnion_le_lintegral_aux [OpensMeasurableSpace X] [SeparableSpace X] (l : ℝ≥0∞) (u : X → ℝ≥0∞) (R : ℝ) (hR : ∀ a ∈ 𝓑, r a ≤ R) (h2u : ∀ i ∈ 𝓑, l * μ (ball (c i) (r i)) ≤ ∫⁻ x in ball (c i) (r i), u x ∂μ) : l * μ (⋃ i ∈ 𝓑, ball (c i) (r i)) ≤ A ^ 2 * ∫⁻ x, u x ∂μ := by let 𝓑' := { a ∈ 𝓑 | 0 < r a } obtain ⟨B, hB𝓑, hB, h2B⟩ := exists_disjoint_subfamily_covering_enlargement_ball 𝓑' c r R (fun a ha => hR a ha.1) (2 ^ 2) (by norm_num) have : Countable B := hB.countable_of_isOpen (fun _ _ => isOpen_ball) (fun a ha => nonempty_ball.mpr (hB𝓑 ha).right) have disj := fun i j hij ↦ hB (Subtype.coe_prop i) (Subtype.coe_prop j) (Subtype.coe_ne_coe.mpr hij) calc l * μ (⋃ i ∈ 𝓑, ball (c i) (r i)) ≤ l * μ (⋃ i ∈ B, ball (c i) (2 ^ 2 * r i)) := by refine mul_right_mono (μ.mono fun x hx ↦ ?) push _ ∈ _ at hx rcases hx with ⟨i, i𝓑, hi⟩ have i𝓑' : i ∈ 𝓑' := .intro i𝓑 (nonempty_ball.mp (nonempty_of_mem hi)) obtain ⟨b, bB, hb⟩ := h2B i i𝓑' exact mem_iUnion₂.mpr ⟨b, bB, hb <| mem_ball.mpr hi⟩ _ ≤ l * ∑' i : B, μ (ball (c i) (2 ^ 2 * r i)) := mul_right_mono <| measure_biUnion_le μ this fun i ↦ ball (c i) (2 ^ 2 * r i) _ ≤ l * ∑' i : B, A ^ 2 * μ (ball (c i) (r i)) := by refine mul_right_mono <| ENNReal.tsum_le_tsum (fun i ↦ ?) rw [sq, sq, mul_assoc, mul_assoc] apply (measure_ball_two_le_same (c i) (2 * r i)).trans gcongr; exact measure_ball_two_le_same (c i) (r i) _ = A ^ 2 * ∑' i : B, l * μ (ball (c i) (r i)) := by rw [ENNReal.tsum_mul_left, ENNReal.tsum_mul_left, ← mul_assoc, ← mul_assoc, mul_comm l] _ ≤ A ^ 2 * ∑' i : B, ∫⁻ x in ball (c i) (r i), u x ∂μ := by gcongr; exact h2u _ (hB𝓑 (Subtype.coe_prop _)).left _ = A ^ 2 * ∫⁻ x in ⋃ i ∈ B, ball (c i) (r i), u x ∂μ := by congr; simpa using (lintegral_iUnion (fun i ↦ measurableSet_ball) disj u).symm _ ≤ A ^ 2 * ∫⁻ x, u x ∂μ := by gcongr; exact Measure.restrict_le_self

variable (𝓑 r) in def tr (k : ℕ) : Set ι := {i | i ∈ 𝓑 ∧ r i ≤ k}

lemma tr_mono : Monotone (tr 𝓑 r) := by intro i j hij rintro k ⟨hi₁, hi₂⟩ exact ⟨hi₁, hi₂.trans (Nat.cast_le.mpr hij)⟩

lemma tr_union (𝓑) (r : ι → ℝ) : 𝓑 = ⋃ k, tr 𝓑 r k := by apply eq_of_subset_of_subset · intro i hi rcases exists_nat_ge (r i) with ⟨k, hk⟩ exact mem_iUnion.mpr ⟨k, hi, hk⟩ · intro i hi exact (mem_iUnion.mp hi).elim (fun _ p => p.left)

public theorem measure_biUnion_le_lintegral [OpensMeasurableSpace X] [SeparableSpace X] (𝓑 : Set ι) (l : ℝ≥0∞) (u : X → ℝ≥0∞) (h2u : ∀ i ∈ 𝓑, l * μ (ball (c i) (r i)) ≤ ∫⁻ x in ball (c i) (r i), u x ∂μ) : l * μ (⋃ i ∈ 𝓑, ball (c i) (r i)) ≤ A ^ 2 * ∫⁻ x, u x ∂μ := by have : μ (⋃ i ∈ 𝓑, ball (c i) (r i)) = ⨆ k, μ (⋃ i ∈ tr 𝓑 r k, ball (c i) (r i)) := by conv_lhs => rw [tr_union 𝓑 r, biUnion_iUnion] have : Monotone (⋃ x ∈ tr 𝓑 r ·, ball (c x) (r x)) := fun i j hij ↦ biUnion_mono (tr_mono hij) (fun _ _ ↦ by rfl) rw [this.measure_iUnion] rw [this, mul_iSup] exact iSup_le fun R ↦ measure_biUnion_le_lintegral_aux l u R (fun i hi ↦ hi.2) (fun i hi ↦ h2u i hi.1)

end MeasureBiUnionBall

public lemma lowerSemiContinuous_maximalFunction : LowerSemicontinuous (maximalFunction μ 𝓑 c r p u) := by intro x s hxr have ⟨i, hi, h⟩ := exists_lt_of_lt_ciSup₂' hxr have hx : x ∈ ball (c i) (r i) := mem_of_indicator_ne_zero (h.trans_le' bot_le |>.ne.symm) rw [indicator_of_mem hx] at h apply eventually_of_mem · exact isOpen_ball.mem_nhds hx · intro y hy apply LT.lt.trans_le _ (le_iSup₂ i hi) rwa [indicator_of_mem hy]

public theorem measurable_maximalFunction [BorelSpace X] : Measurable (maximalFunction μ 𝓑 c r p u) := lowerSemiContinuous_maximalFunction.measurable

public theorem maximalFunction_one_le_eLpNormEssSup : maximalFunction μ 𝓑 c r 1 u x ≤ eLpNormEssSup u μ := calc _ ≤ ⨆ i ∈ 𝓑, (ball (c i) (r i)).indicator (x := x) fun _x ↦ ⨍⁻ _ in ball (c i) (r i), eLpNormEssSup u μ ∂μ := by simp_rw [maximalFunction, inv_one, ENNReal.rpow_one] gcongr exact MeasureTheory.enorm_ae_le_eLpNormEssSup u μ _ ≤ ⨆ i ∈ 𝓑, (ball (c i) (r i)).indicator (x := x) fun _ ↦ eLpNormEssSup u μ := by gcongr; apply setLaverage_const_le _ ≤ ⨆ i ∈ 𝓑, eLpNormEssSup u μ := by gcongr; apply indicator_le_self _ ≤ eLpNormEssSup u μ := by simp_rw [iSup_le_iff, le_refl, implies_true]

theorem MeasureTheory.MemLp.maximalFunction_lt_top (hp₁ : 0 < p) (hu : MemLp u ⊤ μ) : maximalFunction μ 𝓑 c r p u x < ∞ := by rw [maximalFunction_eq_maximalFunction_one_rpow (by positivity)] apply rpow_lt_top_of_nonneg (by positivity) (lt_top_iff_ne_top.mp _) have : MemLp (fun x ↦ ‖u x‖ ^ p) ⊤ μ := by rw [← toReal_ofReal hp₁.le, show ∞ = ∞ / (ENNReal.ofReal p) from ENNReal.top_div_of_ne_top (by finiteness) |>.symm] exact hu.norm_rpow_div _ refine lt_of_le_of_lt maximalFunction_one_le_eLpNormEssSup this.eLpNormEssSup_lt_top

theorem hasStrongType_maximalFunction_top [BorelSpace X] : HasStrongType (maximalFunction (E := E) μ 𝓑 c r 1) ⊤ ⊤ μ μ 1 := by intro f _ use measurable_maximalFunction.aestronglyMeasurable simp only [one_mul, eLpNorm_exponent_top] exact essSup_le_of_ae_le _ (Eventually.of_forall fun x ↦ maximalFunction_one_le_eLpNormEssSup)

/- The proof is roughly between (9.0.12)-(9.0.22).