hasFiniteIntegral_congr'_enorm — Mathlib

English

If f and g coincide in ENorm almost everywhere, then HasFiniteIntegral is equivalent for f and g.

Русский

Если по ENorm совпадают почти всюду, то HasFiniteIntegral совпадает для f и g.

LaTeX

$$$ \\text{HasFiniteIntegral } f \\mu \\iff \\text{HasFiniteIntegral } g \\mu $ при условии, что ENorm f a = ENorm g a почти всюду.$$

Lean4

theorem hasFiniteIntegral_congr'_enorm {f : α → ε} {g : α → ε'} (h : ∀ᵐ a ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) :
    HasFiniteIntegral f μ ↔ HasFiniteIntegral g μ :=
  ⟨fun hf => hf.congr'_enorm h, fun hg => hg.congr'_enorm <| EventuallyEq.symm h⟩

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