Source indexedtheorem · leanprover/lean4:v4.32.0

MeasureTheory.BoundedCompactSupport.mono_norm

Carleson.ToMathlib.BoundedCompactSupport · Carleson/ToMathlib/BoundedCompactSupport.lean:282 to 291

Mathematical statement

Exact Lean statement

theorem mono_norm {g : X → ℝ} (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_norm {g : X → ℝ} (hg : BoundedCompactSupport g μ) (hf : AEStronglyMeasurable f μ)    (hfg : ∀ x, ‖f x‖ ≤ g x) : BoundedCompactSupport f μ where  memLp_top := ⟨hf, eLpNorm_mono_real 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, norm_le_zero_iff, hfx] at hfg