English
For a real interval [a,b] with a<b, the Fourier coefficients of a function f:ℝ→E on this interval are defined as the Fourier coefficients of the unique (b−a)-periodic function that agrees with f on the interval Ioc[a,b].
Русский
Для функции f: ℝ→E и отрезка [a,b] с a<b коэффициенты Фурье на этом отрезке определяются как коэффициенты Фурье уникальной функции с периодом (b−a), которая совпадает с f на подотрезке Ioc[a,b].
LaTeX
$$$$ \\text{fourierCoeffOn}_{[a,b]}(f,n) := \\text{fourierCoeff}((\\text{AddCircle}.liftIoc(b-a,a,f)),n) $$$$
Lean4
/-- For a function on `ℝ`, the Fourier coefficients of `f` on `[a, b]` are defined as the
Fourier coefficients of the unique periodic function agreeing with `f` on `Ioc a b`. -/
def fourierCoeffOn {a b : ℝ} (hab : a < b) (f : ℝ → E) (n : ℤ) : E :=
haveI := Fact.mk (by linarith : 0 < b - a)
fourierCoeff (AddCircle.liftIoc (b - a) a f) n
