lintegral_comp

Mathlib.MeasureTheory.Integral.Lebesgue.Map

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MeasurePreserving.lintegral_comp

English

For measurable f and g, lintegral μ (f ∘ g) equals lintegral (map g μ) f.

Русский

Для измеримых f и g линеграл μ(f ∘ g) = линеграл map g μ (f).

LaTeX

$$$$ \operatorname{lintegral}_{μ}(f \circ g) = \operatorname{lintegral}_{map\ g\ μ}(f). $$$$

Lean4

theorem lintegral_comp {f : β → ℝ≥0∞} (hf : Measurable f) : ∫⁻ a, f (g a) ∂μ = ∫⁻ b, f b ∂ν := by
  rw [← hg.map_eq, lintegral_map hf hg.measurable]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru