Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.distribution_le

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:352 to 363

Mathematical statement

Exact Lean statement

lemma distribution_le [MeasurableSpace ε] [OpensMeasurableSpace ε]
    {c : ℝ≥0∞} (hc : c ≠ 0) {μ : Measure α} (hf : AEMeasurable f μ) :
    distribution f c μ ≤ c⁻¹ * (∫⁻ y, ‖f y‖ₑ ∂μ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma distribution_le [MeasurableSpace ε] [OpensMeasurableSpace ε]    {c : ℝ≥0∞} (hc : c ≠ 0) {μ : Measure α} (hf : AEMeasurable f μ) :    distribution f c μ ≤ c⁻¹ * (∫⁻ y, ‖f y‖ₑ ∂μ) := by  by_cases hc_top : c = ⊤  · simp [hc_top]  apply (mul_le_iff_le_inv hc hc_top).mp  simp_rw [distribution, ← setLIntegral_one, ← lintegral_const_mul' _ _ hc_top, mul_one]  refine le_trans (lintegral_mono_ae ?_) (setLIntegral_le_lintegral _ _)  simp only [Filter.Eventually, ae, mem_ofCountableUnion]  rw [Measure.restrict_apply₀']  · convert measure_empty (μ := μ); ext; simpa using le_of_lt  · exact hf.enorm.nullMeasurableSet_preimage measurableSet_Ioi