Theorem: fourierConv_ofTwiceDifferentiable
Proof state before:
case h.e'_3.h.e'_6
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
⊢ f x - partialFourierSum f N x = g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x
Tactic:
congr 1
Proof state after:
case h.e'_3.h.e'_6.e_a
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
⊢ f x = g ↑x

case h.e'_3.h.e'_6.e_a
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
⊢ partialFourierSum f N x = ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x