congr'_enorm — Mathlib

English

If f and g have equal ENorm a.e., HasFiniteIntegral equivalence holds both ways.

Русский

Если ‖f‖ = ‖g‖ a.e., тогда HasFiniteIntegral f μ эквивалентно HasFiniteIntegral g μ.

LaTeX

$$$ \\text{HasFiniteIntegral } f \\mu \\leftrightarrow \\text{HasFiniteIntegral } g \\mu $ при a.e. равенстве ENorm.$$

Lean4

theorem congr'_enorm {f : α → ε} {g : α → ε'} (hf : HasFiniteIntegral f μ) (h : ∀ᵐ a ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) :
    HasFiniteIntegral g μ :=
  hf.mono_enorm <| EventuallyEq.le <| EventuallyEq.symm h

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