integral_preimage — Mathlib

English

The integral of a measurable function over Ioc t (t+1) in UnitAddCircle equals the integral over UnitAddCircle with the lifted function.

Русский

Интеграл по Ioc(t,t+1) в UnitAddCircle равен интегралу по 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 an almost-everywhere strongly measurable function over `UnitAddCircle` is
equal to the integral over an interval (t, t + 1] in `ℝ` of its lift to `ℝ`. -/
protected theorem integral_preimage (t : ℝ) (f : UnitAddCircle → E) :
    (∫ a in Ioc t (t + 1), f a) = ∫ b : UnitAddCircle, f b :=
  AddCircle.integral_preimage 1 t f

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