Source indexedlemma · leanprover/lean4:v4.32.0

fourierCoeffOn_add

Carleson.Classical.Basic · Carleson/Classical/Basic.lean:136 to 146

Mathematical statement

Exact Lean statement

@[simp]
lemma fourierCoeffOn_add {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}
    (hf : IntervalIntegrable f MeasureTheory.volume a b)
    (hg : IntervalIntegrable g MeasureTheory.volume a b) :
    fourierCoeffOn hab (f + g) n = fourierCoeffOn hab f n + fourierCoeffOn hab g n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp]lemma fourierCoeffOn_add {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}    (hf : IntervalIntegrable f MeasureTheory.volume a b)    (hg : IntervalIntegrable g MeasureTheory.volume a b) :    fourierCoeffOn hab (f + g) n = fourierCoeffOn hab f n + fourierCoeffOn hab g n:= by  simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',    fourier_coe_apply', Complex.ofReal_sub, Pi.add_apply, smul_eq_mul, mul_add]  rw [intervalIntegral.integral_add    (by ring_nf; exact hf.continuousOn_mul (by fun_prop))    (by ring_nf; exact hg.continuousOn_mul (by fun_prop)),    smul_add]