instMeasureSpaceUnitAddCircle — Mathlib

English

A variant asserting the same relation as the previous item but stated for Ioo and using a version of the derivative condition HasDerivAt.

Русский

Вариант, утверждающий ту же связь, что и в предыдущем пункте, но для Ioo и с условием HasDerivAt.

LaTeX

$$$$ \\text{fourierCoeffOn}_{hab} f n = \\frac{1}{-2 i \\pi n} ( \\mathrm{fourier}(-n)(a) (f(b)-f(a)) - (b-a) \\mathrm{fourierCoeffOn}_{hab} f' n ) $$$$

Lean4

/-- In this file we normalise the measure on `ℝ / ℤ` to have total volume 1. -/
local instance : MeasureSpace UnitAddCircle :=
  ⟨AddCircle.haarAddCircle⟩

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