mono — Mathlib

English

Specialized lemma about HasFiniteIntegral with ENorm and pointwise bound in AE; yields HasFiniteIntegral f.

Русский

Специализированная лемма для HasFiniteIntegral с ENorm и точным неравенством ae; выводит HasFiniteIntegral f.

LaTeX

$$$ \\text{HasFiniteIntegral } f \\mu \\Rightarrow \\Big( \\|f(a)\\| \\le g(a) \\Big) \\Rightarrow \\text{HasFiniteIntegral } f \\mu $$$

Lean4

theorem mono {f : α → β} {g : α → γ} (hg : HasFiniteIntegral g μ) (h : ∀ᵐ a ∂μ, ‖f a‖ ≤ ‖g a‖) :
    HasFiniteIntegral f μ :=
  hg.mono_enorm <| h.mono fun _x hx ↦ enorm_le_iff_norm_le.mpr hx

Похожие утверждения