hasFiniteIntegral_norm_iff — Mathlib

English

For any f: α → β, HasFiniteIntegral (fun a ↦ ‖f a‖) μ ⇔ HasFiniteIntegral f μ.

Русский

Для любой функции f: α → β имеет место равенство: HasFiniteIntegral (функция a ↦ ‖f(a)‖) μ ⇔ HasFiniteIntegral f μ.

LaTeX

$$$HasFiniteIntegral\bigl(\,a \mapsto \|f(a)\|\bigr)\mu \iff HasFiniteIntegral f\mu$$$

Lean4

theorem hasFiniteIntegral_norm_iff (f : α → β) : HasFiniteIntegral (fun a => ‖f a‖) μ ↔ HasFiniteIntegral f μ :=
  hasFiniteIntegral_congr' <| Eventually.of_forall fun x => norm_norm (f x)

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