lintegral_indicator_const_comp — Mathlib

English

For a measurable f and measurable set s and a constant c ≥ 0, the lintegral of s.indicator (const c) (f) equals c times μ preimage of s under f.

Русский

Для измеримой f, множества s и константы c≥0: ∫ s.indicator (const c) (f) dμ = c · μ(f^{-1}(s)).

LaTeX

$$$$ \int f\!\text{ over } s (\text{indicator}(c)\circ f) \, dμ = c \cdot μ(f^{-1}(s)). $$$$

Lean4

theorem lintegral_indicator_const_comp {f : α → β} {s : Set β} (hf : Measurable f) (hs : MeasurableSet s) (c : ℝ≥0∞) :
    ∫⁻ a, s.indicator (fun _ => c) (f a) ∂μ = c * μ (f ⁻¹' s) :=
  by
  erw [lintegral_comp (measurable_const.indicator hs) hf]
  rw [lintegral_indicator_const hs, Measure.map_apply hf hs]

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