Theorems · Theorem · harmonic analysis

fourierCoeffOn_of_hasDeriv_right

∀ {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ},
  n ≠ 0 →
    ContinuousOn f (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
        IntervalIntegrable f' MeasureTheory.volume a b →
          fourierCoeffOn hab f n =
            1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
              ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)

Express Fourier coefficients of f on an interval in terms of those of its derivative.

Defined in

Mathlib.Analysis.Fourier.AddCircle

Cited by

1 results in Mathlib

Foundations

Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound