integrable_comp — Mathlib

English

Let f be a linear isometry between inner product spaces and g a function. Then g composed with f is integrable iff g is integrable.

Русский

Пусть f — линейное изометрическое отображение между пространствами с скалярным произведением, а g функция. Тогда g ∘ f интегрируема ⇔ g интегрируема.

LaTeX

$$$\\operatorname{Integrable}(g \\circ f) \\iff \\operatorname{Integrable}(g),$ где $f$ — линейное изоморфизмо-фона.$$

Lean4

theorem integrable_comp (g : F' → A) : Integrable (g ∘ f) ↔ Integrable g :=
  f.measurePreserving.integrable_comp_emb f.toMeasurableEquiv.measurableEmbedding

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