hasFiniteIntegral_congr' — Mathlib

English

Let f, g be functions from α to a normed space, and suppose ‖f(a)‖ = ‖g(a)‖ for μ-almost every a. Then f has a finite L1-integral with respect to μ if and only if g does.

Русский

Пусть f, g : α → β, и пусть для μ-покрытия μ-a.e. выполнено ‖f(x)‖ = ‖g(x)‖. Тогда f имеет конечно интеграл Л1 по μ тогда и только тогда, когда и у g имеется такой интеграл.

LaTeX

$$$\\forall f,g:\\alpha\\to\\varepsilon\\,\\big(\\forall^{\\mathrm{a}} a\\,\\partial\\mu,\\ \\|f(a)\\|_\\varepsilon = \\|g(a)\\|_\\varepsilon\\big) \\Rightarrow \\HasFiniteIntegral f\\mu \\leftrightarrow \\HasFiniteIntegral g\\mu$$$

Lean4

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

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