Source indexedtheorem · leanprover/lean4:v4.32.0

measure_biUnion_le_lintegral

Carleson.ToMathlib.HardyLittlewood · Carleson/ToMathlib/HardyLittlewood.lean:143 to 154

Mathematical statement

Exact Lean statement

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 ∂μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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)