lintegral_comp — Mathlib

English

If f and g are measurable, then the lintegral of f ∘ g with respect to μ equals the lintegral of f with respect to the pushforward map μ under g: lintegral μ (f ∘ g) = lintegral (map g μ) f.

Русский

Если f и g измеримы, то линеграл f∘g по μ равен линегралу f по образующему measure map g μ: ∫ f∘g dμ = ∫ f d(map g μ).

LaTeX

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

Lean4

theorem lintegral_comp {f : β → ℝ≥0∞} {g : α → β} (hf : Measurable f) (hg : Measurable g) :
    lintegral μ (f ∘ g) = ∫⁻ a, f a ∂map g μ :=
  (lintegral_map hf hg).symm

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