Source indexedlemma · leanprover/lean4:v4.32.0

globalMaximalFunction_zero_enorm_ae_zero

Carleson.TwoSidedCarleson.NontangentialOperator · Carleson/TwoSidedCarleson/NontangentialOperator.lean:517 to 526

Mathematical statement

Exact Lean statement

lemma globalMaximalFunction_zero_enorm_ae_zero (hR : 0 < R) {f : X → ℂ} (hf : AEStronglyMeasurable f)
    (hMzero : globalMaximalFunction volume 1 f x = 0) :
    ∀ᵐ x' ∂(volume.restrict (ball x R)), ‖f x'‖ₑ = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma globalMaximalFunction_zero_enorm_ae_zero (hR : 0 < R) {f : X → ℂ} (hf : AEStronglyMeasurable f)    (hMzero : globalMaximalFunction volume 1 f x = 0) :    ∀ᵐ x' ∂(volume.restrict (ball x R)), ‖f x'‖ₑ = 0 := by  change (fun x' ↦ ‖f x'‖ₑ) =ᶠ[ae (volume.restrict (ball x R))] 0  rw [← lintegral_eq_zero_iff' (by fun_prop)]  rw [← bot_eq_zero, ← le_bot_iff, bot_eq_zero]  apply le_of_le_of_eq (lintegral_ball_le_volume_mul_globalMaximalFunction _)  · rw [hMzero]    simp  · simp [hR]