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

State before:
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
Tactic:
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, Complex.real_smul,
  Complex.ofReal_inv]
State after:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    ((↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x) +
      (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

State before:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    ((↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x) +
      (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x
Tactic:
rw [← mul_add, ← intervalIntegral.integral_add]
State after:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    (↑b - ↑a)⁻¹ *
      ∫ (x : ℝ) in a..b,
        (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
          (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b

State before:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    (↑b - ↑a)⁻¹ *
      ∫ (x : ℝ) in a..b,
        (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
          (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b
Tactic:
congr
State after:
case e_a.e_f
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x)) = fun x =>
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
      (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b

State before:
case e_a.e_f
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x)) = fun x =>
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
      (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

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

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b

State before:
case e_a.e_f.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
x : ℝ
⊢ (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
      (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b
Tactic:
ring
State after:
case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b

State before:
case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b
Tactic:
. apply hf.continuousOn_mul
  apply Continuous.continuousOn
  continuity
State after:
case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b

State before:
case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b
Tactic:
. apply hg.continuousOn_mul
  apply Continuous.continuousOn
  continuity
State after:
no goals

State before:
case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b
Tactic:
apply hf.continuousOn_mul
State after:
case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ ContinuousOn (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp) (Set.uIcc a b)

State before:
case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ ContinuousOn (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp) (Set.uIcc a b)
Tactic:
apply Continuous.continuousOn
State after:
case hf.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ Continuous fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp

State before:
case hf.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ Continuous fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp
Tactic:
continuity
State after:
no goals

State before:
case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b
Tactic:
apply hg.continuousOn_mul
State after:
case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ ContinuousOn (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp) (Set.uIcc a b)

State before:
case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ ContinuousOn (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp) (Set.uIcc a b)
Tactic:
apply Continuous.continuousOn
State after:
case hg.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ Continuous fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp

State before:
case hg.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ Continuous fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp
Tactic:
continuity
State after:
no goals