intervalIntegral_preimage — Mathlib

English

Similarly, the interval integral preimage for UnitAddCircle matches the interval integral on A d dCircle with lifted f.

Русский

Аналогично, предобраз интервального интеграла в UnitAddCircle совпадает с интервальным интегралом на AddCircle с функцией-лифтингом.

LaTeX

$$$\\int_{a\\in 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 intervalIntegral_preimage (t : ℝ) (f : UnitAddCircle → E) :
    ∫ a in t..t + 1, f a = ∫ b : UnitAddCircle, f b :=
  AddCircle.intervalIntegral_preimage 1 t f

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