mono'_enorm — Mathlib

English

If f and g have equal ENorm a.e., HasFiniteIntegral transfers from f to g and vice versa.

Русский

Если нормы ENorm f и g равны почти на μ-мераже, то HasFiniteIntegral переносится между f и g.

LaTeX

$$$ \\text{HasFiniteIntegral } f \\mu \\rightarrow \\Big( \\|f\\| = \\|g\\| \\text{ a.e.} \\Big) \\rightarrow \\text{HasFiniteIntegral } g \\mu $$$

Lean4

theorem mono'_enorm {f : α → ε} {g : α → ℝ≥0∞} (hg : HasFiniteIntegral g μ) (h : ∀ᵐ a ∂μ, ‖f a‖ₑ ≤ g a) :
    HasFiniteIntegral f μ :=
  hg.mono_enorm <| h.mono fun _x hx ↦ le_trans hx le_rfl

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