congr' — Mathlib

English

If f and g have equal norm a.e., HasFiniteIntegral equivalence holds.

Русский

Если ‖f‖ = ‖g‖ a.e., тогда HasFiniteIntegral f μ ⇔ HasFiniteIntegral g μ.

LaTeX

$$$ \\text{HasFiniteIntegral } f \\mu \\leftrightarrow \\text{HasFiniteIntegral } g \\mu $ под условием a.e. равенства норм.$$

Lean4

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

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