[GOAL]
T : ℝ
⊢ Function.Periodic (fun x => ↑expMapCircle (2 * π / T * x)) T
[PROOFSTEP]
rcases eq_or_ne T 0 with (rfl | hT)
[GOAL]
case inl
⊢ Function.Periodic (fun x => ↑expMapCircle (2 * π / 0 * x)) 0
[PROOFSTEP]
intro x
[GOAL]
case inl
x : ℝ
⊢ (fun x => ↑expMapCircle (2 * π / 0 * x)) (x + 0) = (fun x => ↑expMapCircle (2 * π / 0 * x)) x
[PROOFSTEP]
simp
[GOAL]
case inr
T : ℝ
hT : T ≠ 0
⊢ Function.Periodic (fun x => ↑expMapCircle (2 * π / T * x)) T
[PROOFSTEP]
intro x
[GOAL]
case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ (fun x => ↑expMapCircle (2 * π / T * x)) (x + T) = (fun x => ↑expMapCircle (2 * π / T * x)) x
[PROOFSTEP]
simp_rw [mul_add]
[GOAL]
case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ ↑expMapCircle (2 * π / T * x + 2 * π / T * T) = ↑expMapCircle (2 * π / T * x)
[PROOFSTEP]
rw [div_mul_cancel _ hT, periodic_expMapCircle]
[GOAL]
T : ℝ
x y : AddCircle T
⊢ toCircle (x + y) = toCircle x * toCircle y
[PROOFSTEP]
induction x using QuotientAddGroup.induction_on'
[GOAL]
case H
T : ℝ
y : AddCircle T
z✝ : ℝ
⊢ toCircle (↑z✝ + y) = toCircle ↑z✝ * toCircle y
[PROOFSTEP]
induction y using QuotientAddGroup.induction_on'
[GOAL]
case H.H
T z✝¹ z✝ : ℝ
⊢ toCircle (↑z✝¹ + ↑z✝) = toCircle ↑z✝¹ * toCircle ↑z✝
[PROOFSTEP]
rw [← QuotientAddGroup.mk_add]
[GOAL]
case H.H
T z✝¹ z✝ : ℝ
⊢ toCircle ↑(z✝¹ + z✝) = toCircle ↑z✝¹ * toCircle ↑z✝
[PROOFSTEP]
simp_rw [toCircle, Function.Periodic.lift_coe, mul_add, expMapCircle_add]
[GOAL]
T : ℝ
hT : T ≠ 0
⊢ Function.Injective toCircle
[PROOFSTEP]
intro a b h
[GOAL]
T : ℝ
hT : T ≠ 0
a b : AddCircle T
h : toCircle a = toCircle b
⊢ a = b
[PROOFSTEP]
induction a using QuotientAddGroup.induction_on'
[GOAL]
case H
T : ℝ
hT : T ≠ 0
b : AddCircle T
z✝ : ℝ
h : toCircle ↑z✝ = toCircle b
⊢ ↑z✝ = b
[PROOFSTEP]
induction b using QuotientAddGroup.induction_on'
[GOAL]
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : toCircle ↑z✝¹ = toCircle ↑z✝
⊢ ↑z✝¹ = ↑z✝
[PROOFSTEP]
simp_rw [toCircle, Function.Periodic.lift_coe] at h
[GOAL]
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : ↑expMapCircle (2 * π / T * z✝¹) = ↑expMapCircle (2 * π / T * z✝)
⊢ ↑z✝¹ = ↑z✝
[PROOFSTEP]
obtain ⟨m, hm⟩ := expMapCircle_eq_expMapCircle.mp h.symm
[GOAL]
case H.H.intro
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : ↑expMapCircle (2 * π / T * z✝¹) = ↑expMapCircle (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ↑z✝¹ = ↑z✝
[PROOFSTEP]
rw [QuotientAddGroup.eq]
[GOAL]
case H.H.intro
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : ↑expMapCircle (2 * π / T * z✝¹) = ↑expMapCircle (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ -z✝¹ + z✝ ∈ AddSubgroup.zmultiples T
[PROOFSTEP]
simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul]
[GOAL]
case H.H.intro
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : ↑expMapCircle (2 * π / T * z✝¹) = ↑expMapCircle (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ∃ k, ↑k * T = -z✝¹ + z✝
[PROOFSTEP]
use m
[GOAL]
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : ↑expMapCircle (2 * π / T * z✝¹) = ↑expMapCircle (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ↑m * T = -z✝¹ + z✝
[PROOFSTEP]
field_simp [Real.two_pi_pos.ne'] at hm
[GOAL]
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : ↑expMapCircle (2 * π / T * z✝¹) = ↑expMapCircle (2 * π / T * z✝)
m : ℤ
hm : 2 * π * z✝ = 2 * π * z✝¹ + ↑m * (2 * π) * T
⊢ ↑m * T = -z✝¹ + z✝
[PROOFSTEP]
rw [← mul_right_inj' Real.two_pi_pos.ne']
[GOAL]
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : ↑expMapCircle (2 * π / T * z✝¹) = ↑expMapCircle (2 * π / T * z✝)
m : ℤ
hm : 2 * π * z✝ = 2 * π * z✝¹ + ↑m * (2 * π) * T
⊢ 2 * π * (↑m * T) = 2 * π * (-z✝¹ + z✝)
[PROOFSTEP]
linarith
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ ↑(fourier n) ↑x = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
[PROOFSTEP]
rw [fourier_apply, ← QuotientAddGroup.mk_zsmul, toCircle, Function.Periodic.lift_coe, expMapCircle_apply,
  Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_mul, zsmul_eq_mul, Complex.ofReal_mul, Complex.ofReal_int_cast]
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (↑2 * ↑π / ↑T * (↑n * ↑x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
[PROOFSTEP]
norm_num
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (2 * ↑π / ↑T * (↑n * ↑x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
[PROOFSTEP]
congr 1
[GOAL]
case e_z
T : ℝ
n : ℤ
x : ℝ
⊢ 2 * ↑π / ↑T * (↑n * ↑x) * Complex.I = 2 * ↑π * Complex.I * ↑n * ↑x / ↑T
[PROOFSTEP]
ring
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ ↑(toCircle (n • ↑x)) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
[PROOFSTEP]
rw [← fourier_apply]
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ ↑(fourier n) ↑x = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
[PROOFSTEP]
exact fourier_coe_apply
[GOAL]
T : ℝ
x : AddCircle T
⊢ ↑(fourier 0) x = 1
[PROOFSTEP]
induction x using QuotientAddGroup.induction_on'
[GOAL]
case H
T z✝ : ℝ
⊢ ↑(fourier 0) ↑z✝ = 1
[PROOFSTEP]
simp only [fourier_coe_apply]
[GOAL]
case H
T z✝ : ℝ
⊢ Complex.exp (2 * ↑π * Complex.I * ↑0 * ↑z✝ / ↑T) = 1
[PROOFSTEP]
norm_num
[GOAL]
T : ℝ
x : AddCircle T
⊢ ↑(toCircle 0) = 1
[PROOFSTEP]
have : fourier 0 x = @toCircle T 0 := by rw [fourier_apply, zero_smul]
[GOAL]
T : ℝ
x : AddCircle T
⊢ ↑(fourier 0) x = ↑(toCircle 0)
[PROOFSTEP]
rw [fourier_apply, zero_smul]
[GOAL]
T : ℝ
x : AddCircle T
this : ↑(fourier 0) x = ↑(toCircle 0)
⊢ ↑(toCircle 0) = 1
[PROOFSTEP]
rw [← this]
[GOAL]
T : ℝ
x : AddCircle T
this : ↑(fourier 0) x = ↑(toCircle 0)
⊢ ↑(fourier 0) x = 1
[PROOFSTEP]
exact fourier_zero
[GOAL]
T : ℝ
n : ℤ
⊢ ↑(fourier n) 0 = 1
[PROOFSTEP]
rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero, zero_div, Complex.exp_zero]
[GOAL]
T : ℝ
x : AddCircle T
⊢ ↑(fourier 1) x = ↑(toCircle x)
[PROOFSTEP]
rw [fourier_apply, one_zsmul]
[GOAL]
T : ℝ
n : ℤ
x : AddCircle T
⊢ ↑(fourier (-n)) x = ↑(starRingEnd ((fun x => ℂ) x)) (↑(fourier n) x)
[PROOFSTEP]
induction x using QuotientAddGroup.induction_on'
[GOAL]
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(fourier (-n)) ↑z✝ = ↑(starRingEnd ((fun x => ℂ) ↑z✝)) (↑(fourier n) ↑z✝)
[PROOFSTEP]
simp_rw [fourier_apply, toCircle]
[GOAL]
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(Function.Periodic.lift (_ : Function.Periodic (fun x => ↑expMapCircle (2 * π / T * x)) T) (-n • ↑z✝)) =
    ↑(starRingEnd ℂ)
      ↑(Function.Periodic.lift (_ : Function.Periodic (fun x => ↑expMapCircle (2 * π / T * x)) T) (n • ↑z✝))
[PROOFSTEP]
rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_zsmul]
[GOAL]
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(Function.Periodic.lift (_ : Function.Periodic (fun x => ↑expMapCircle (2 * π / T * x)) T) ↑(-n • z✝)) =
    ↑(starRingEnd ℂ)
      ↑(Function.Periodic.lift (_ : Function.Periodic (fun x => ↑expMapCircle (2 * π / T * x)) T) ↑(n • z✝))
[PROOFSTEP]
simp_rw [Function.Periodic.lift_coe, ← coe_inv_circle_eq_conj, ← expMapCircle_neg, neg_smul, mul_neg]
[GOAL]
T : ℝ
n : ℤ
x : AddCircle T
⊢ ↑(toCircle (-(n • x))) = ↑(starRingEnd ((fun x => ℂ) x)) (↑(fourier n) x)
[PROOFSTEP]
rw [← neg_smul, ← fourier_apply]
[GOAL]
T : ℝ
n : ℤ
x : AddCircle T
⊢ ↑(fourier (-n)) x = ↑(starRingEnd ((fun x => ℂ) x)) (↑(fourier n) x)
[PROOFSTEP]
exact fourier_neg
[GOAL]
T : ℝ
m n : ℤ
x : AddCircle T
⊢ ↑(fourier (m + n)) x = ↑(fourier m) x * ↑(fourier n) x
[PROOFSTEP]
simp_rw [fourier_apply, add_zsmul, toCircle_add, coe_mul_unitSphere]
[GOAL]
T : ℝ
m n : ℤ
x : AddCircle T
⊢ ↑(toCircle ((m + n) • x)) = ↑(fourier m) x * ↑(fourier n) x
[PROOFSTEP]
rw [← fourier_apply]
[GOAL]
T : ℝ
m n : ℤ
x : AddCircle T
⊢ ↑(fourier (m + n)) x = ↑(fourier m) x * ↑(fourier n) x
[PROOFSTEP]
exact fourier_add
[GOAL]
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
⊢ ‖fourier n‖ = 1
[PROOFSTEP]
rw [ContinuousMap.norm_eq_iSup_norm]
[GOAL]
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
⊢ ⨆ (x : AddCircle T), ‖↑(fourier n) x‖ = 1
[PROOFSTEP]
have : ∀ x : AddCircle T, ‖fourier n x‖ = 1 := fun x => abs_coe_circle _
[GOAL]
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), ‖↑(fourier n) x‖ = 1
⊢ ⨆ (x : AddCircle T), ‖↑(fourier n) x‖ = 1
[PROOFSTEP]
simp_rw [this]
[GOAL]
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), ‖↑(fourier n) x‖ = 1
⊢ ⨆ (x : AddCircle T), 1 = 1
[PROOFSTEP]
exact @ciSup_const _ _ _ Zero.nonempty _
[GOAL]
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(fourier n) (x + ↑(T / 2 / ↑n)) = -↑(fourier n) x
[PROOFSTEP]
rw [fourier_apply, zsmul_add, ← QuotientAddGroup.mk_zsmul, toCircle_add, coe_mul_unitSphere]
[GOAL]
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(toCircle (n • x)) * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -↑(fourier n) x
[PROOFSTEP]
have : (n : ℂ) ≠ 0 := by simpa using hn
[GOAL]
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑n ≠ 0
[PROOFSTEP]
simpa using hn
[GOAL]
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : ↑n ≠ 0
⊢ ↑(toCircle (n • x)) * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -↑(fourier n) x
[PROOFSTEP]
have : (@toCircle T (n • (T / 2 / n) : ℝ) : ℂ) = -1 :=
  by
  rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, expMapCircle_apply]
  replace hT := Complex.ofReal_ne_zero.mpr hT.ne'
  convert Complex.exp_pi_mul_I using 3
  field_simp; ring
[GOAL]
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : ↑n ≠ 0
⊢ ↑(toCircle ↑(n • (T / 2 / ↑n))) = -1
[PROOFSTEP]
rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, expMapCircle_apply]
[GOAL]
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : ↑n ≠ 0
⊢ Complex.exp (↑(2 * π / T * (↑n * (T / 2 / ↑n))) * Complex.I) = -1
[PROOFSTEP]
replace hT := Complex.ofReal_ne_zero.mpr hT.ne'
[GOAL]
T : ℝ
n : ℤ
hn : n ≠ 0
x : AddCircle T
this : ↑n ≠ 0
hT : ↑T ≠ 0
⊢ Complex.exp (↑(2 * π / T * (↑n * (T / 2 / ↑n))) * Complex.I) = -1
[PROOFSTEP]
convert Complex.exp_pi_mul_I using 3
[GOAL]
case h.e'_2.h.e'_1.h.e'_5
T : ℝ
n : ℤ
hn : n ≠ 0
x : AddCircle T
this : ↑n ≠ 0
hT : ↑T ≠ 0
⊢ ↑(2 * π / T * (↑n * (T / 2 / ↑n))) = ↑π
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_2.h.e'_1.h.e'_5
T : ℝ
n : ℤ
hn : n ≠ 0
x : AddCircle T
this : ↑n ≠ 0
hT : ↑T ≠ 0
⊢ 2 * ↑π * (↑n * ↑T) = ↑π * (↑T * (2 * ↑n))
[PROOFSTEP]
ring
[GOAL]
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this✝ : ↑n ≠ 0
this : ↑(toCircle ↑(n • (T / 2 / ↑n))) = -1
⊢ ↑(toCircle (n • x)) * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -↑(fourier n) x
[PROOFSTEP]
rw [this]
[GOAL]
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this✝ : ↑n ≠ 0
this : ↑(toCircle ↑(n • (T / 2 / ↑n))) = -1
⊢ ↑(toCircle (n • x)) * -1 = -↑(fourier n) x
[PROOFSTEP]
simp
[GOAL]
T : ℝ
⊢ ∀ {a : C(AddCircle T, ℂ)},
    a ∈ (adjoin ℂ (range fourier)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      star a ∈ (adjoin ℂ (range fourier)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
show Algebra.adjoin ℂ (range (fourier (T := T))) ≤ star (Algebra.adjoin ℂ (range (fourier (T := T))))
[GOAL]
T : ℝ
⊢ adjoin ℂ (range fourier) ≤ star (adjoin ℂ (range fourier))
[PROOFSTEP]
refine adjoin_le ?_
[GOAL]
T : ℝ
⊢ range fourier ⊆ ↑(star (adjoin ℂ (range fourier)))
[PROOFSTEP]
rintro - ⟨n, rfl⟩
[GOAL]
case intro
T : ℝ
n : ℤ
⊢ fourier n ∈ ↑(star (adjoin ℂ (range fourier)))
[PROOFSTEP]
exact subset_adjoin ⟨-n, ext fun _ => fourier_neg⟩
[GOAL]
T : ℝ
⊢ ↑Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra = span ℂ (range fourier)
[PROOFSTEP]
apply adjoin_eq_span_of_subset
[GOAL]
case hs
T : ℝ
⊢ ↑(Submonoid.closure (range fourier)) ⊆ ↑(span ℂ (range fourier))
[PROOFSTEP]
refine' Subset.trans _ Submodule.subset_span
[GOAL]
case hs
T : ℝ
⊢ ↑(Submonoid.closure (range fourier)) ⊆ range fourier
[PROOFSTEP]
intro x hx
[GOAL]
case hs
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ x ∈ range fourier
[PROOFSTEP]
refine Submonoid.closure_induction hx (fun _ => id) ⟨0, ?_⟩ ?_
[GOAL]
case hs.refine_1
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ fourier 0 = 1
[PROOFSTEP]
ext1 z
[GOAL]
case hs.refine_1.h
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
z : AddCircle T
⊢ ↑(fourier 0) z = ↑1 z
[PROOFSTEP]
exact fourier_zero
[GOAL]
case hs.refine_2
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ ∀ (x y : C(AddCircle T, ℂ)), x ∈ range fourier → y ∈ range fourier → x * y ∈ range fourier
[PROOFSTEP]
rintro _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
[GOAL]
case hs.refine_2.intro.intro
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
⊢ fourier m * fourier n ∈ range fourier
[PROOFSTEP]
refine' ⟨m + n, _⟩
[GOAL]
case hs.refine_2.intro.intro
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
⊢ fourier (m + n) = fourier m * fourier n
[PROOFSTEP]
ext1 z
[GOAL]
case hs.refine_2.intro.intro.h
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
z : AddCircle T
⊢ ↑(fourier (m + n)) z = ↑(fourier m * fourier n) z
[PROOFSTEP]
exact fourier_add
[GOAL]
T : ℝ
hT : Fact (0 < T)
⊢ Subalgebra.SeparatesPoints fourierSubalgebra.toSubalgebra
[PROOFSTEP]
intro x y hxy
[GOAL]
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ∃ f, f ∈ (fun f => ↑f) '' ↑fourierSubalgebra.toSubalgebra ∧ f x ≠ f y
[PROOFSTEP]
refine' ⟨_, ⟨fourier 1, subset_adjoin ⟨1, rfl⟩, rfl⟩, _⟩
[GOAL]
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ (fun f => ↑f) (fourier 1) x ≠ (fun f => ↑f) (fourier 1) y
[PROOFSTEP]
dsimp only
[GOAL]
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ↑(fourier 1) x ≠ ↑(fourier 1) y
[PROOFSTEP]
rw [fourier_one, fourier_one]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ↑(toCircle x) ≠ ↑(toCircle y)
[PROOFSTEP]
contrapose! hxy
[GOAL]
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : ↑(toCircle x) = ↑(toCircle y)
⊢ x = y
[PROOFSTEP]
rw [Subtype.coe_inj] at hxy
[GOAL]
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : toCircle x = toCircle y
⊢ x = y
[PROOFSTEP]
exact injective_toCircle hT.elim.ne' hxy
[GOAL]
T : ℝ
hT : Fact (0 < T)
⊢ topologicalClosure (span ℂ (range fourier)) = ⊤
[PROOFSTEP]
rw [← fourierSubalgebra_coe]
[GOAL]
T : ℝ
hT : Fact (0 < T)
⊢ topologicalClosure (↑Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra) = ⊤
[PROOFSTEP]
exact congr_arg (Subalgebra.toSubmodule <| StarSubalgebra.toSubalgebra ·) fourierSubalgebra_closure_eq_top
[GOAL]
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
⊢ topologicalClosure (span ℂ (range (fourierLp p))) = ⊤
[PROOFSTEP]
convert
  (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) hp ℂ).topologicalClosure_map_submodule
    span_fourier_closure_eq_top
[GOAL]
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiringComplex = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (range (fourierLp p)) = Submodule.map (↑(toLp p haarAddCircle ℂ)) (span ℂ (range fourier))
[PROOFSTEP]
erw [map_span, range_comp]
[GOAL]
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiringComplex = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (↑(toLp p haarAddCircle ℂ) '' range fun n => fourier n) = span ℂ (↑↑(toLp p haarAddCircle ℂ) '' range fourier)
[PROOFSTEP]
simp only [ContinuousLinearMap.coe_coe]
[GOAL]
T : ℝ
hT : Fact (0 < T)
⊢ Orthonormal ℂ (fourierLp 2)
[PROOFSTEP]
rw [orthonormal_iff_ite]
[GOAL]
T : ℝ
hT : Fact (0 < T)
⊢ ∀ (i j : ℤ), inner (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0
[PROOFSTEP]
intro i j
[GOAL]
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ inner (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0
[PROOFSTEP]
rw [ContinuousMap.inner_toLp (@haarAddCircle T hT) (fourier i) (fourier j)]
[GOAL]
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ ∫ (x : AddCircle T), ↑(starRingEnd ((fun x => ℂ) x)) (↑(fourier i) x) * ↑(fourier j) x ∂haarAddCircle =
    if i = j then 1 else 0
[PROOFSTEP]
simp_rw [← fourier_neg, ← fourier_add]
[GOAL]
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ ∫ (x : AddCircle T), ↑(fourier (-i + j)) x ∂haarAddCircle = if i = j then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ∫ (x : AddCircle T), ↑(fourier (-i + j)) x ∂haarAddCircle = 1
[PROOFSTEP]
simp_rw [h, neg_add_self]
[GOAL]
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ∫ (x : AddCircle T), ↑(fourier 0) x ∂haarAddCircle = 1
[PROOFSTEP]
have : ⇑(@fourier T 0) = (fun _ => 1 : AddCircle T → ℂ) := by ext1; exact fourier_zero
[GOAL]
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ↑(fourier 0) = fun x => 1
[PROOFSTEP]
ext1
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
x✝ : AddCircle T
⊢ ↑(fourier 0) x✝ = 1
[PROOFSTEP]
exact fourier_zero
[GOAL]
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
this : ↑(fourier 0) = fun x => 1
⊢ ∫ (x : AddCircle T), ↑(fourier 0) x ∂haarAddCircle = 1
[PROOFSTEP]
rw [this, integral_const, measure_univ, ENNReal.one_toReal, Complex.real_smul, Complex.ofReal_one, mul_one]
[GOAL]
case neg
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ ∫ (x : AddCircle T), ↑(fourier (-i + j)) x ∂haarAddCircle = 0
[PROOFSTEP]
have hij : -i + j ≠ 0 := by
  rw [add_comm]
  exact sub_ne_zero.mpr (Ne.symm h)
[GOAL]
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ -i + j ≠ 0
[PROOFSTEP]
rw [add_comm]
[GOAL]
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ j + -i ≠ 0
[PROOFSTEP]
exact sub_ne_zero.mpr (Ne.symm h)
[GOAL]
case neg
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
hij : -i + j ≠ 0
⊢ ∫ (x : AddCircle T), ↑(fourier (-i + j)) x ∂haarAddCircle = 0
[PROOFSTEP]
convert integral_eq_zero_of_add_right_eq_neg (μ := haarAddCircle) (fourier_add_half_inv_index hij hT.elim)
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : AddCircle T → E
n : ℤ
a : ℝ
⊢ fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, ↑(fourier (-n)) ↑x • f ↑x
[PROOFSTEP]
have : ∀ x : ℝ, @fourier T (-n) x • f x = (fun z : AddCircle T => @fourier T (-n) z • f z) x := by intro x; rfl
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : AddCircle T → E
n : ℤ
a : ℝ
⊢ ∀ (x : ℝ), ↑(fourier (-n)) ↑x • f ↑x = (fun z => ↑(fourier (-n)) z • f z) ↑x
[PROOFSTEP]
intro x
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : AddCircle T → E
n : ℤ
a x : ℝ
⊢ ↑(fourier (-n)) ↑x • f ↑x = (fun z => ↑(fourier (-n)) z • f z) ↑x
[PROOFSTEP]
rfl
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : AddCircle T → E
n : ℤ
a : ℝ
this : ∀ (x : ℝ), ↑(fourier (-n)) ↑x • f ↑x = (fun z => ↑(fourier (-n)) z • f z) ↑x
⊢ fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, ↑(fourier (-n)) ↑x • f ↑x
[PROOFSTEP]
simp_rw [this]
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : AddCircle T → E
n : ℤ
a : ℝ
this : ∀ (x : ℝ), ↑(fourier (-n)) ↑x • f ↑x = (fun z => ↑(fourier (-n)) z • f z) ↑x
⊢ fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fun z => ↑(fourier (-n)) z • f z) ↑x
[PROOFSTEP]
rw [fourierCoeff, AddCircle.intervalIntegral_preimage T a (fun z => _ • _), volume_eq_smul_haarAddCircle,
  integral_smul_measure, ENNReal.toReal_ofReal hT.out.le, ← smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne',
  one_smul]
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : AddCircle T → E
c : ℂ
n : ℤ
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n
[PROOFSTEP]
simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul, smul_assoc, integral_smul]
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
hab : a < b
f : ℝ → E
n : ℤ
⊢ 0 < b - a
[PROOFSTEP]
linarith
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace 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
[PROOFSTEP]
haveI := Fact.mk (by linarith : 0 < b - a)
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
⊢ 0 < b - a
[PROOFSTEP]
linarith
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
rw [fourierCoeffOn, fourierCoeff_eq_intervalIntegral _ _ a, add_sub, add_sub_cancel']
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x • liftIoc (b - a) a f ↑x =
    (1 / (b - a)) • ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
congr 1
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
simp_rw [intervalIntegral.integral_of_le hab.le]
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ ∫ (x : ℝ) in Ioc a b, ↑(fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = ∫ (x : ℝ) in Ioc a b, ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
refine' set_integral_congr measurableSet_Ioc fun x hx => _
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ ↑(fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
rw [liftIoc_coe_apply]
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ x ∈ Ioc a (a + (b - a))
[PROOFSTEP]
rwa [add_sub, add_sub_cancel']
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
⊢ fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n
[PROOFSTEP]
haveI := Fact.mk (by linarith : 0 < b - a)
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
⊢ 0 < b - a
[PROOFSTEP]
linarith
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n
[PROOFSTEP]
apply fourierCoeff.const_smul
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIoc T a f) n = fourierCoeffOn (_ : a < a + T) f n
[PROOFSTEP]
rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral, add_sub_cancel' a T]
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in ?a..?a + T, ↑(fourier (-n)) ↑x • liftIoc T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, ↑(fourier (-n)) ↑x • f x
case a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ℝ
case a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ℝ
[PROOFSTEP]
congr 1
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in ?a..?a + T, ↑(fourier (-n)) ↑x • liftIoc T a f ↑x = ∫ (x : ℝ) in a..a + T, ↑(fourier (-n)) ↑x • f x
case a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ℝ
case a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ℝ
[PROOFSTEP]
refine' intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => _)
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ι a (a + T)
⊢ ↑(fourier (-n)) ↑x • liftIoc T a f ↑x = ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
rw [liftIoc_coe_apply]
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ι a (a + T)
⊢ x ∈ Ioc a (a + T)
[PROOFSTEP]
rwa [uIoc_of_le (lt_add_of_pos_right a hT.out).le] at hx
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIco T a f) n = fourierCoeffOn (_ : a < a + T) f n
[PROOFSTEP]
rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral _ _ a, add_sub_cancel' a T]
[GOAL]
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in a..a + T, ↑(fourier (-n)) ↑x • liftIco T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
congr 1
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in a..a + T, ↑(fourier (-n)) ↑x • liftIco T a f ↑x = ∫ (x : ℝ) in a..a + T, ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
simp_rw [intervalIntegral.integral_of_le (lt_add_of_pos_right a hT.out).le]
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in Ioc a (a + T), ↑(fourier (-n)) ↑x • liftIco T a f ↑x =
    ∫ (x : ℝ) in Ioc a (a + T), ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
iterate 2 rw [integral_Ioc_eq_integral_Ioo]
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in Ioc a (a + T), ↑(fourier (-n)) ↑x • liftIco T a f ↑x =
    ∫ (x : ℝ) in Ioc a (a + T), ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
rw [integral_Ioc_eq_integral_Ioo]
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (t : ℝ) in Ioo a (a + T), ↑(fourier (-n)) ↑t • liftIco T a f ↑t =
    ∫ (x : ℝ) in Ioc a (a + T), ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
rw [integral_Ioc_eq_integral_Ioo]
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (t : ℝ) in Ioo a (a + T), ↑(fourier (-n)) ↑t • liftIco T a f ↑t =
    ∫ (t : ℝ) in Ioo a (a + T), ↑(fourier (-n)) ↑t • f t
[PROOFSTEP]
refine' set_integral_congr measurableSet_Ioo fun x hx => _
[GOAL]
case e_a
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ioo a (a + T)
⊢ ↑(fourier (-n)) ↑x • liftIco T a f ↑x = ↑(fourier (-n)) ↑x • f x
[PROOFSTEP]
rw [liftIco_coe_apply (Ioo_subset_Ico_self hx)]
[GOAL]
T : ℝ
hT : Fact (0 < T)
⊢ 2 ≠ ⊤
[PROOFSTEP]
norm_num
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
i : ℤ
⊢ ↑(↑fourierBasis.repr f) i = fourierCoeff (↑↑f) i
[PROOFSTEP]
trans ∫ t : AddCircle T, conj ((@fourierLp T hT 2 _ i : AddCircle T → ℂ) t) * f t ∂haarAddCircle
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
i : ℤ
⊢ ↑(↑fourierBasis.repr f) i = ∫ (t : AddCircle T), ↑(starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle
[PROOFSTEP]
rw [fourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_fourierBasis]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
i : ℤ
⊢ ∫ (a : AddCircle T), inner (↑↑(fourierLp 2 i) a) (↑↑f a) ∂haarAddCircle =
    ∫ (t : AddCircle T), ↑(starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle
[PROOFSTEP]
simp only [IsROrC.inner_apply]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
i : ℤ
⊢ ∫ (t : AddCircle T), ↑(starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle = fourierCoeff (↑↑f) i
[PROOFSTEP]
apply integral_congr_ae
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
i : ℤ
⊢ (fun a => ↑(starRingEnd ℂ) (↑↑(fourierLp 2 i) a) * ↑↑f a) =ᶠ[ae haarAddCircle] fun a => ↑(fourier (-i)) a • ↑↑f a
[PROOFSTEP]
filter_upwards [coeFn_fourierLp 2 i] with _ ht
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
i : ℤ
a✝ : AddCircle T
ht : ↑↑(fourierLp 2 i) a✝ = ↑(fourier i) a✝
⊢ ↑(starRingEnd ℂ) (↑↑(fourierLp 2 i) a✝) * ↑↑f a✝ = ↑(fourier (-i)) a✝ • ↑↑f a✝
[PROOFSTEP]
rw [ht, ← fourier_neg, smul_eq_mul]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
⊢ HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f
[PROOFSTEP]
simp_rw [← fourierBasis_repr]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
⊢ HasSum (fun i => ↑(↑fourierBasis.repr f) i • fourierLp 2 i) f
[PROOFSTEP]
rw [← coe_fourierBasis]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
⊢ HasSum
    (fun i => ↑(↑fourierBasis.repr f) i • (fun i => ↑(LinearIsometryEquiv.symm fourierBasis.repr) (lp.single 2 i 1)) i)
    f
[PROOFSTEP]
exact HilbertBasis.hasSum_repr fourierBasis f
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
⊢ ∑' (i : ℤ), ‖fourierCoeff (↑↑f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
[PROOFSTEP]
simp_rw [← fourierBasis_repr]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
⊢ ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
[PROOFSTEP]
have H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' i, ‖fourierBasis.repr f i‖ ^ 2 :=
  by
  apply_mod_cast lp.norm_rpow_eq_tsum ?_ (fourierBasis.repr f)
  norm_num
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
⊢ ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
[PROOFSTEP]
apply_mod_cast lp.norm_rpow_eq_tsum ?_ (fourierBasis.repr f)
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
⊢ 0 < ENNReal.toReal 2
[PROOFSTEP]
norm_num
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
⊢ ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
[PROOFSTEP]
have H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
⊢ ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
[PROOFSTEP]
simp
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
⊢ ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
[PROOFSTEP]
have H₃ := congr_arg IsROrC.re (@L2.inner_def (AddCircle T) ℂ ℂ _ _ _ _ _ f f)
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ↑IsROrC.re (inner f f) = ↑IsROrC.re (∫ (a : AddCircle T), inner (↑↑f a) (↑↑f a) ∂haarAddCircle)
⊢ ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
[PROOFSTEP]
rw [← integral_re] at H₃
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ↑IsROrC.re (inner f f) = ∫ (a : AddCircle T), ↑IsROrC.re (inner (↑↑f a) (↑↑f a)) ∂haarAddCircle
⊢ ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
[PROOFSTEP]
simp only [← norm_sq_eq_inner] at H₃
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (a : AddCircle T), ↑IsROrC.re (inner (↑↑f a) (↑↑f a)) ∂haarAddCircle
⊢ ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
[PROOFSTEP]
conv_rhs at H₃ => enter [2, a]; rw [← norm_sq_eq_inner]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (a : AddCircle T), ↑IsROrC.re (inner (↑↑f a) (↑↑f a)) ∂haarAddCircle
| ∫ (a : AddCircle T), ↑IsROrC.re (inner (↑↑f a) (↑↑f a)) ∂haarAddCircle
[PROOFSTEP]
enter [2, a]; rw [← norm_sq_eq_inner]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (a : AddCircle T), ↑IsROrC.re (inner (↑↑f a) (↑↑f a)) ∂haarAddCircle
| ∫ (a : AddCircle T), ↑IsROrC.re (inner (↑↑f a) (↑↑f a)) ∂haarAddCircle
[PROOFSTEP]
enter [2, a]; rw [← norm_sq_eq_inner]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (a : AddCircle T), ↑IsROrC.re (inner (↑↑f a) (↑↑f a)) ∂haarAddCircle
| ∫ (a : AddCircle T), ↑IsROrC.re (inner (↑↑f a) (↑↑f a)) ∂haarAddCircle
[PROOFSTEP]
enter [2, a]
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (a : AddCircle T), ↑IsROrC.re (inner (↑↑f a) (↑↑f a)) ∂haarAddCircle
a : AddCircle T
| ↑IsROrC.re (inner (↑↑f a) (↑↑f a))
[PROOFSTEP]
rw [← norm_sq_eq_inner]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (a : AddCircle T), ‖↑↑f a‖ ^ 2 ∂haarAddCircle
⊢ ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
[PROOFSTEP]
rw [← H₁, H₂, H₃]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : { x // x ∈ Lp ℂ 2 }
H₁ : ‖↑fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(↑fourierBasis.repr f) i‖ ^ 2
H₂ : ‖↑fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ↑IsROrC.re (inner f f) = ↑IsROrC.re (∫ (a : AddCircle T), inner (↑↑f a) (↑↑f a) ∂haarAddCircle)
⊢ Integrable fun a => inner (↑↑f a) (↑↑f a)
[PROOFSTEP]
exact L2.integrable_inner f f
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
n : ℤ
⊢ ∀ (x : AddCircle T), (fun t => ↑(fourier (-n)) t) x = (fun t => ↑(fourier (-n)) t) x
[PROOFSTEP]
tauto
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ↑f)
⊢ HasSum (fun i => fourierCoeff (↑f) i • fourier i) f
[PROOFSTEP]
have sum_L2 := hasSum_fourier_series_L2 (toLp (E := ℂ) 2 haarAddCircle ℂ f)
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ↑f)
sum_L2 :
  HasSum (fun i => fourierCoeff (↑↑(↑(toLp 2 haarAddCircle ℂ) f)) i • fourierLp 2 i) (↑(toLp 2 haarAddCircle ℂ) f)
⊢ HasSum (fun i => fourierCoeff (↑f) i • fourier i) f
[PROOFSTEP]
simp_rw [fourierCoeff_toLp] at sum_L2
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ↑f)
sum_L2 : HasSum (fun i => fourierCoeff (↑f) i • fourierLp 2 i) (↑(toLp 2 haarAddCircle ℂ) f)
⊢ HasSum (fun i => fourierCoeff (↑f) i • fourier i) f
[PROOFSTEP]
refine' ContinuousMap.hasSum_of_hasSum_Lp (summable_of_summable_norm _) sum_L2
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ↑f)
sum_L2 : HasSum (fun i => fourierCoeff (↑f) i • fourierLp 2 i) (↑(toLp 2 haarAddCircle ℂ) f)
⊢ Summable fun a => ‖fourierCoeff (↑f) a • fourier a‖
[PROOFSTEP]
simp_rw [norm_smul, fourier_norm, mul_one, summable_norm_iff]
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ↑f)
sum_L2 : HasSum (fun i => fourierCoeff (↑f) i • fourierLp 2 i) (↑(toLp 2 haarAddCircle ℂ) f)
⊢ Summable fun x => fourierCoeff (↑f) x
[PROOFSTEP]
exact h
[GOAL]
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ↑f)
x : AddCircle T
⊢ HasSum (fun i => fourierCoeff (↑f) i • ↑(fourier i) x) (↑f x)
[PROOFSTEP]
convert (ContinuousMap.evalClm ℂ x).hasSum (hasSum_fourier_series_of_summable h)
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => ↑(fourier n) ↑y) (2 * ↑π * I * ↑n / ↑T * ↑(fourier n) ↑x) x
[PROOFSTEP]
simp_rw [fourier_coe_apply]
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => exp (2 * ↑π * I * ↑n * ↑y / ↑T)) (2 * ↑π * I * ↑n / ↑T * exp (2 * ↑π * I * ↑n * ↑x / ↑T)) x
[PROOFSTEP]
refine' (_ : HasDerivAt (fun y => exp (2 * π * I * n * y / T)) _ _).comp_ofReal
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => exp (2 * ↑π * I * ↑n * y / ↑T)) (2 * ↑π * I * ↑n / ↑T * exp (2 * ↑π * I * ↑n * ↑x / ↑T)) ↑x
[PROOFSTEP]
rw [(fun α β => by ring : ∀ α β : ℂ, α * exp β = exp β * α)]
[GOAL]
T : ℝ
n : ℤ
x : ℝ
α β : ℂ
⊢ α * exp β = exp β * α
[PROOFSTEP]
ring
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => exp (2 * ↑π * I * ↑n * y / ↑T)) (exp (2 * ↑π * I * ↑n * ↑x / ↑T) * (2 * ↑π * I * ↑n / ↑T)) ↑x
[PROOFSTEP]
refine' (hasDerivAt_exp _).comp ↑x _
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => 2 * ↑π * I * ↑n * y / ↑T) (2 * ↑π * I * ↑n / ↑T) ↑x
[PROOFSTEP]
convert hasDerivAt_mul_const (2 * ↑π * I * ↑n / T) using 1
[GOAL]
case h.e'_6
T : ℝ
n : ℤ
x : ℝ
⊢ (fun y => 2 * ↑π * I * ↑n * y / ↑T) = fun x => x * (2 * ↑π * I * ↑n / ↑T)
[PROOFSTEP]
ext1 y
[GOAL]
case h.e'_6.h
T : ℝ
n : ℤ
x : ℝ
y : ℂ
⊢ 2 * ↑π * I * ↑n * y / ↑T = y * (2 * ↑π * I * ↑n / ↑T)
[PROOFSTEP]
ring
[GOAL]
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => ↑(fourier (-n)) ↑y) (-2 * ↑π * I * ↑n / ↑T * ↑(fourier (-n)) ↑x) x
[PROOFSTEP]
simpa using hasDerivAt_fourier T (-n) x
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => ↑T / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑y) (↑(fourier (-n)) ↑x) x
[PROOFSTEP]
convert (hasDerivAt_fourier_neg T n x).div_const (-2 * π * I * n / T) using 1
[GOAL]
case h.e'_6
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fun y => ↑T / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑y) = fun x => ↑(fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)
[PROOFSTEP]
ext1 y
[GOAL]
case h.e'_6.h
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ ↑T / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑y = ↑(fourier (-n)) ↑y / (-2 * ↑π * I * ↑n / ↑T)
[PROOFSTEP]
rw [div_div_eq_mul_div]
[GOAL]
case h.e'_6.h
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ ↑T / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑y = ↑(fourier (-n)) ↑y * ↑T / (-2 * ↑π * I * ↑n)
[PROOFSTEP]
ring
[GOAL]
case h.e'_7
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ ↑(fourier (-n)) ↑x = -2 * ↑π * I * ↑n / ↑T * ↑(fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)
[PROOFSTEP]
rw [mul_div_cancel_left]
[GOAL]
case h.e'_7.ha
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ -2 * ↑π * I * ↑n / ↑T ≠ 0
[PROOFSTEP]
simp only [Ne.def, div_eq_zero_iff, neg_eq_zero, mul_eq_zero, bit0_eq_zero, one_ne_zero, ofReal_eq_zero, false_or_iff,
  Int.cast_eq_zero, not_or]
[GOAL]
case h.e'_7.ha
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (((¬2 = 0 ∧ ¬π = 0) ∧ ¬I = 0) ∧ ¬n = 0) ∧ ¬T = 0
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_7.ha
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ ((¬π = 0 ∧ ¬I = 0) ∧ ¬n = 0) ∧ ¬T = 0
[PROOFSTEP]
exact ⟨⟨⟨Real.pi_ne_zero, I_ne_zero⟩, hn⟩, hT.out.ne'⟩
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
⊢ fourierCoeffOn hab f n =
    1 / (-2 * ↑π * I * ↑n) * (↑(fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
[PROOFSTEP]
rw [← ofReal_sub]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
⊢ fourierCoeffOn hab f n =
    1 / (-2 * ↑π * I * ↑n) * (↑(fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * fourierCoeffOn hab f' n)
[PROOFSTEP]
have hT : Fact (0 < b - a) := ⟨by linarith⟩
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
⊢ 0 < b - a
[PROOFSTEP]
linarith
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ fourierCoeffOn hab f n =
    1 / (-2 * ↑π * I * ↑n) * (↑(fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * fourierCoeffOn hab f' n)
[PROOFSTEP]
simp_rw [fourierCoeffOn_eq_integral, smul_eq_mul, real_smul, ofReal_div, ofReal_one]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ 1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f x =
    1 / (-2 * ↑π * I * ↑n) *
      (↑(fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f' x))
[PROOFSTEP]
conv => pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [mul_comm])
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| 1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f x =
    1 / (-2 * ↑π * I * ↑n) *
      (↑(fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f' x))
[PROOFSTEP]
pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [mul_comm])
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| 1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f x =
    1 / (-2 * ↑π * I * ↑n) *
      (↑(fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f' x))
[PROOFSTEP]
pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [mul_comm])
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| 1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f x =
    1 / (-2 * ↑π * I * ↑n) *
      (↑(fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f' x))
[PROOFSTEP]
pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [mul_comm])
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| 1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f x =
    1 / (-2 * ↑π * I * ↑n) *
      (↑(fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, ↑(fourier (-n)) ↑x * f' x))
[PROOFSTEP]
pattern (occs := 1 2 3) fourier _ _ * _
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| ↑(fourier (-n)) ↑x * f x
[PROOFSTEP]
(rw [mul_comm])
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| ↑(fourier (-n)) ↑x * f x
[PROOFSTEP]
rw [mul_comm]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| ↑(fourier (-n)) ↑x * f x
[PROOFSTEP]
rw [mul_comm]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| ↑(fourier (-n)) ↑x * f x
[PROOFSTEP]
rw [mul_comm]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| ↑(fourier (-n)) ↑a * (f b - f a)
[PROOFSTEP]
(rw [mul_comm])
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| ↑(fourier (-n)) ↑a * (f b - f a)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| ↑(fourier (-n)) ↑a * (f b - f a)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
| ↑(fourier (-n)) ↑a * (f b - f a)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| ↑(fourier (-n)) ↑x * f' x
[PROOFSTEP]
(rw [mul_comm])
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| ↑(fourier (-n)) ↑x * f' x
[PROOFSTEP]
rw [mul_comm]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| ↑(fourier (-n)) ↑x * f' x
[PROOFSTEP]
rw [mul_comm]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
x : ℝ
| ↑(fourier (-n)) ↑x * f' x
[PROOFSTEP]
rw [mul_comm]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ 1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f x * ↑(fourier (-n)) ↑x =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * ↑(fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x))
[PROOFSTEP]
rw [integral_mul_deriv_eq_deriv_mul hf (fun x _ => has_antideriv_at_fourier_neg hT hn x) hf'
    (((map_continuous (fourier (-n))).comp (AddCircle.continuous_mk' _)).intervalIntegrable _ _)]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑b) -
          f a * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, f' x * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * ↑(fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x))
[PROOFSTEP]
dsimp only
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑b) -
          f a * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, f' x * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * ↑(fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x))
[PROOFSTEP]
have : ∀ u v w : ℂ, u * ((b - a : ℝ) / v * w) = (b - a : ℝ) / v * (u * w) := by intros; ring
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
[PROOFSTEP]
intros
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
u✝ v✝ w✝ : ℂ
⊢ u✝ * (↑(b - a) / v✝ * w✝) = ↑(b - a) / v✝ * (u✝ * w✝)
[PROOFSTEP]
ring
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑b) -
          f a * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, f' x * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * ↑(fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x))
[PROOFSTEP]
conv in intervalIntegral _ _ _ _ => congr; ext; rw [this]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| ∫ (x : ℝ) in a..b, f' x * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑x)
[PROOFSTEP]
congr; ext; rw [this]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| ∫ (x : ℝ) in a..b, f' x * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑x)
[PROOFSTEP]
congr; ext; rw [this]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| ∫ (x : ℝ) in a..b, f' x * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑x)
[PROOFSTEP]
congr
[GOAL]
case f
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| fun x => f' x * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑x)
case a
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| a
case b
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| b
case μ
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| volume
[PROOFSTEP]
ext
[GOAL]
case f.h
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
x✝ : ℝ
| f' x✝ * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑x✝)
case a
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| a
case b
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| b
case μ
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
| volume
[PROOFSTEP]
rw [this]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑b) -
          f a * (↑(b - a) / (-2 * ↑π * I * ↑n) * ↑(fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, ↑(b - a) / (-2 * ↑π * I * ↑n) * (f' x * ↑(fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * ↑(fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x))
[PROOFSTEP]
rw [(by ring : ((b - a : ℝ) : ℂ) / (-2 * π * I * n) = ((b - a : ℝ) : ℂ) * (1 / (-2 * π * I * n)))]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ ↑(b - a) / (-2 * ↑π * I * ↑n) = ↑(b - a) * (1 / (-2 * ↑π * I * ↑n))
[PROOFSTEP]
ring
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑b) -
          f a * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, ↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (f' x * ↑(fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * ↑(fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x))
[PROOFSTEP]
have s2 : (b : AddCircle (b - a)) = (a : AddCircle (b - a)) := by simpa using coe_add_period (b - a) a
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ ↑b = ↑a
[PROOFSTEP]
simpa using coe_add_period (b - a) a
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑b) -
          f a * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, ↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (f' x * ↑(fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * ↑(fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x))
[PROOFSTEP]
rw [s2, integral_const_mul, ← sub_mul, mul_sub, mul_sub]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
⊢ 1 / ↑(b - a) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑a)) -
      1 / ↑(b - a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x) =
    1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * ↑(fourier (-n)) ↑a) -
      1 / (-2 * ↑π * I * ↑n) * (↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
⊢ 1 / ↑(b - a) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑a)) =
    1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * ↑(fourier (-n)) ↑a)
[PROOFSTEP]
conv_lhs => rw [mul_comm, mul_div, mul_one]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
| 1 / ↑(b - a) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑a))
[PROOFSTEP]
rw [mul_comm, mul_div, mul_one]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
| 1 / ↑(b - a) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑a))
[PROOFSTEP]
rw [mul_comm, mul_div, mul_one]
[GOAL]
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
| 1 / ↑(b - a) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑a))
[PROOFSTEP]
rw [mul_comm, mul_div, mul_one]
[GOAL]
case e_a
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
⊢ (f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑a) / ↑(b - a) =
    1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * ↑(fourier (-n)) ↑a)
[PROOFSTEP]
rw [div_eq_iff (ofReal_ne_zero.mpr hT.out.ne')]
[GOAL]
case e_a
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
⊢ (f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ↑(fourier (-n)) ↑a) =
    1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * ↑(fourier (-n)) ↑a) * ↑(b - a)
[PROOFSTEP]
ring
[GOAL]
case e_a
T a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
⊢ 1 / ↑(b - a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x) =
    1 / (-2 * ↑π * I * ↑n) * (↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * ↑(fourier (-n)) ↑x))
[PROOFSTEP]
ring