lintegral_preimage — Mathlib

English

For a measurable function f on UnitAddCircle, the lintegral over Ioc t (t+1) of f equals the lintegral over UnitAddCircle of f.

Русский

Для измеримой функции f на UnitAddCircle линегральный интеграл по Ioc(t,t+1) равен линегральному интегралу по UnitAddCircle.

LaTeX

$$$\\int_{a\\in \\mathrm{Ioc}(t,t+1)} f(a)\\,\\mathrm{d}a = \\int_{b\\in \\mathrm{UnitAddCircle}} f(b)\\,\\mathrm{d}b$$$

Lean4

/-- The integral of a measurable function over `UnitAddCircle` is equal to the integral over an
interval (t, t + 1] in `ℝ` of its lift to `ℝ`. -/
protected theorem lintegral_preimage (t : ℝ) (f : UnitAddCircle → ℝ≥0∞) :
    (∫⁻ a in Ioc t (t + 1), f a) = ∫⁻ b : UnitAddCircle, f b :=
  AddCircle.lintegral_preimage 1 t f

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