Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.laverage_le_biInf_MB'

Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:285 to 292

Mathematical statement

Exact Lean statement

lemma laverage_le_biInf_MB' {c₀ : X} {r₀ : ℝ} (hr : 4 * D ^ s J + dist (c J) c₀ ≤ r₀)
    (h : ∃ i ∈ 𝓑, c𝓑 i = c₀ ∧ r𝓑 i = r₀) :
    ⨍⁻ x in ball c₀ r₀, ‖f x‖ₑ ∂volume ≤ ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma laverage_le_biInf_MB' {c₀ : X} {r₀ : ℝ} (hr : 4 * D ^ s J + dist (c J) c₀ ≤ r₀)    (h : ∃ i ∈ 𝓑, c𝓑 i = c₀ ∧ r𝓑 i = r₀) :    ⨍⁻ x in ball c₀ r₀, ‖f x‖ₑ ∂volume ≤ ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by  simp_rw [maximalFunction, inv_one, ENNReal.rpow_one, le_iInf_iff]  intro y my; obtain ⟨b, mb, cb, rb⟩ := h  replace my : y ∈ ball (c𝓑 b) (r𝓑 b) := by    rw [cb, rb]; refine Grid_subset_ball.trans (ball_subset_ball' hr) my  exact le_iSup₂_of_le b mb (by rw [indicator_of_mem my, cb, rb])