Theorem: fourierCoeffOn_mul (Carleson/Theorem1_1/Basic.lean)

State before:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ fourierCoeffOn hab (fun x => c * f x) n = c * fourierCoeffOn hab f n
Tactic:
simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
  fourier_coe_apply', Complex.ofReal_sub, smul_eq_mul, Complex.real_smul, Complex.ofReal_inv]
State after:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    c * ((↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)

State before:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    c * ((↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
Tactic:
rw [← mul_assoc, mul_comm c, mul_assoc _ c, mul_comm c, ← intervalIntegral.integral_mul_const]
State after:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c

State before:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c
Tactic:
congr
State after:
case e_a.e_f
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x)) = fun x =>
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c

State before:
case e_a.e_f
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x)) = fun x =>
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c
Tactic:
ext x
State after:
case e_a.e_f.h
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
x : ℝ
⊢ (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c

State before:
case e_a.e_f.h
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
x : ℝ
⊢ (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c
Tactic:
ring
State after:
no goals