setIntegral_trim — Mathlib

English

If f is measure-preserving and a measurable embedding, then ∫_{f''s} g ≤ ∫_{s} g∘f with g: Y → E.

Русский

Если f сохраняет меру и измеримо вложение, то интеграл по образу f''s ≤ интегралу по s от g∘f.

LaTeX

$$$$ \\int_{y \\in f''s} g(y) \\, d\\nu(y) = \\int_{x \\in s} g(f(x)) \\, d\\mu(x) $$$$

Lean4

theorem setIntegral_trim {X} {m m0 : MeasurableSpace X} {μ : Measure X} (hm : m ≤ m0) {f : X → E}
    (hf_meas : StronglyMeasurable[m] f) {s : Set X} (hs : MeasurableSet[m] s) :
    ∫ x in s, f x ∂μ = ∫ x in s, f x ∂μ.trim hm := by rwa [integral_trim hm hf_meas, restrict_trim hm μ]

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