∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} (f : ℝ → E) (n : ℤ) (hab : a < b),
  fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x