Source indexedtheorem · leanprover/lean4:v4.32.0

MeasureTheory.BoundedCompactSupport.mono

Carleson.ToMathlib.BoundedCompactSupport · Carleson/ToMathlib/BoundedCompactSupport.lean:270 to 279

Source documentation

If ‖f‖ is bounded by g and g is bounded compactly supported, then so is f.

Exact Lean statement

theorem mono {g : X → ℝ≥0∞} (hg : BoundedCompactSupport g μ) (hf : AEStronglyMeasurable f μ)
    (hfg : ∀ x, ‖f x‖ₑ ≤ g x) : BoundedCompactSupport f μ where
  memLp_top

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem mono {g : X → ℝ≥0∞} (hg : BoundedCompactSupport g μ) (hf : AEStronglyMeasurable f μ)    (hfg : ∀ x, ‖f x‖ₑ ≤ g x) : BoundedCompactSupport f μ where  memLp_top := ⟨hf, eLpNorm_mono_enorm hfg |>.trans_lt hg.memLp_top.eLpNorm_lt_top⟩  hasCompactSupport := by    refine hg.hasCompactSupport.mono ?_    by_contra h    simp only [support_subset_iff, ne_eq, mem_support, not_forall, Decidable.not_not] at h    obtain ⟨x, hfx, hgx⟩ := h    specialize hfg x    simp_rw [hgx, nonpos_iff_eq_zero, enorm_eq_zero, hfx] at hfg