Theorem: fourierConv_ofTwiceDifferentiable (Carleson/Theorem1_1/Approximation.lean)

State before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have fact_two_pi_pos : Fact (0 < 2 * Real.pi) := by
  rw [fact_iff]
  exact Real.two_pi_pos
State after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
set g : C(AddCircle (2 * Real.pi), ℂ) := ⟨AddCircle.liftIco (2*Real.pi) 0 f, AddCircle.liftIco_continuous ((periodicf 0).symm) fdiff.continuous.continuousOn⟩ with g_def
State after:
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 := ⋯ }
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
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 := ⋯ }
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have two_pi_pos' : 0 < 0 + 2 * Real.pi := by linarith [Real.two_pi_pos]
State after:
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
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
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
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have fourierCoeff_correspondence {i : ℤ} : fourierCoeff g i = fourierCoeffOn two_pi_pos' f i := fourierCoeff_liftIco_eq f i
State after:
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 two_pi_pos' f i
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
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 two_pi_pos' f i
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
simp at fourierCoeff_correspondence
State after:
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
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
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
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have function_sum : HasSum (fun (i : ℤ) => fourierCoeff g i • fourier i) g := by
  apply hasSum_fourier_series_of_summable
  obtain ⟨C, hC⟩ := fourierCoeffOn_ContDiff_two_bound periodicf fdiff
  set maj : ℤ → ℝ := fun i ↦ 1 / (i ^ 2) * C with maj_def
  have summable_maj : Summable maj := by
    by_cases Ceq0 : C = 0
    . rw [maj_def, Ceq0]
      simp only [one_div, mul_zero]
      exact summable_zero
    . rw [← summable_div_const_iff Ceq0]
      convert Real.summable_one_div_int_pow.mpr one_lt_two using 1
      rw [maj_def]
      ext i
      simp only [one_div]
      rw [mul_div_cancel_right₀]
      exact Ceq0
  rw [summable_congr @fourierCoeff_correspondence, ←summable_norm_iff]
  apply summable_of_le_on_nonzero _ _ summable_maj
  . intro i
    simp
  . intro i ine0
    rw [maj_def, Complex.norm_eq_abs]
    field_simp
    exact hC i ine0
State after:
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
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
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
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have := int_sum_nat function_sum
State after:
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 : Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeff (⇑g) n • fourier n) atTop (𝓝 g)
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
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 : Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeff (⇑g) n • fourier n) atTop (𝓝 g)
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
rw [ContinuousMap.tendsto_iff_tendstoUniformly, Metric.tendstoUniformly_iff] at this
State after:
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₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
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₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have := this ε εpos
State after:
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) < ε
this :
  ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
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) < ε
this :
  ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
rw [Filter.eventually_atTop] at this
State after:
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) < ε
this :
  ∃ a,
    ∀ b ≥ a,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
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) < ε
this :
  ∃ a,
    ∀ b ≥ a,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
⊢ ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
obtain ⟨N₀, hN₀⟩ := this
State after:
case intro
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₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro
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₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
use N₀
State after:
case h
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 > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case h
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 > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
intro N hN x hx
State after:
case h
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)
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case h
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)
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have := hN₀ N hN.le x
State after:
case h
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 : dist (g ↑x) ((∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeff (⇑g) n • fourier n) ↑x) < ε
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case h
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 : dist (g ↑x) ((∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeff (⇑g) n • fourier n) ↑x) < ε
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
rw [Complex.dist_eq] at this
State after:
case h
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 - (∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeff (⇑g) n • fourier n) ↑x) < ε
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case h
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 - (∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeff (⇑g) n • fourier n) ↑x) < ε
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
simp only [ContinuousMap.coe_sum, sum_apply] at this
State after:
case h
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) < ε
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case h
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) < ε
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
convert this.le using 2
State after:
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

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
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

State before:
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
Tactic:
. rw [g_def, ContinuousMap.coe_mk]
  by_cases h : x = 2 * Real.pi
  . conv => lhs; rw [h, ← zero_add  (2 * Real.pi), periodicf]
    have := AddCircle.coe_add_period (2 * Real.pi) 0
    rw [zero_add] at this
    rw [h, this, AddCircle.liftIco_coe_apply]
    simp [Real.pi_pos]
  . have : x ∈ Set.Ico 0 (2 * Real.pi) := by
      use hx.1
      apply lt_of_le_of_ne hx.2 h
    rw [AddCircle.liftIco_coe_apply]
    rw [zero_add]
    exact this
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) < ε
⊢ partialFourierSum f N x = ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x

State before:
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
Tactic:
. rw [partialFourierSum]
  congr
  ext n
  rw [fourierCoeff_correspondence]
  simp
State after:
no goals

State before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
⊢ Fact (0 < 2 * Real.pi)
Tactic:
rw [fact_iff]
State after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
⊢ 0 < 2 * Real.pi

State before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
⊢ 0 < 2 * Real.pi
Tactic:
exact Real.two_pi_pos
State after:
no goals

State before:
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 := ⋯ }
⊢ 0 < 0 + 2 * Real.pi
Tactic:
linarith [Real.two_pi_pos]
State after:
no goals

State before:
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
⊢ HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
Tactic:
apply hasSum_fourier_series_of_summable
State after:
case h
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
⊢ Summable (fourierCoeff ⇑g)

State before:
case h
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
⊢ Summable (fourierCoeff ⇑g)
Tactic:
obtain ⟨C, hC⟩ := fourierCoeffOn_ContDiff_two_bound periodicf fdiff
State after:
case h.intro
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
⊢ Summable (fourierCoeff ⇑g)

State before:
case h.intro
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
⊢ Summable (fourierCoeff ⇑g)
Tactic:
set maj : ℤ → ℝ := fun i ↦ 1 / (i ^ 2) * C with maj_def
State after:
case h.intro
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
⊢ Summable (fourierCoeff ⇑g)

State before:
case h.intro
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
⊢ Summable (fourierCoeff ⇑g)
Tactic:
have summable_maj : Summable maj := by
  by_cases Ceq0 : C = 0
  . rw [maj_def, Ceq0]
    simp only [one_div, mul_zero]
    exact summable_zero
  . rw [← summable_div_const_iff Ceq0]
    convert Real.summable_one_div_int_pow.mpr one_lt_two using 1
    rw [maj_def]
    ext i
    simp only [one_div]
    rw [mul_div_cancel_right₀]
    exact Ceq0
State after:
case h.intro
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ Summable (fourierCoeff ⇑g)

State before:
case h.intro
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ Summable (fourierCoeff ⇑g)
Tactic:
rw [summable_congr @fourierCoeff_correspondence, ←summable_norm_iff]
State after:
case h.intro
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ Summable fun x => ‖fourierCoeffOn ⋯ f x‖

State before:
case h.intro
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ Summable fun x => ‖fourierCoeffOn ⋯ f x‖
Tactic:
apply summable_of_le_on_nonzero _ _ summable_maj
State after:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ 0 ≤ fun x => ‖fourierCoeffOn ⋯ f x‖

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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ ∀ (i : ℤ), i ≠ 0 → ‖fourierCoeffOn ⋯ f i‖ ≤ maj i

State before:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ 0 ≤ fun x => ‖fourierCoeffOn ⋯ f x‖

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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ ∀ (i : ℤ), i ≠ 0 → ‖fourierCoeffOn ⋯ f i‖ ≤ maj i
Tactic:
. intro i
  simp
State after:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ ∀ (i : ℤ), i ≠ 0 → ‖fourierCoeffOn ⋯ f i‖ ≤ maj i

State before:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ ∀ (i : ℤ), i ≠ 0 → ‖fourierCoeffOn ⋯ f i‖ ≤ maj i
Tactic:
. intro i ine0
  rw [maj_def, Complex.norm_eq_abs]
  field_simp
  exact hC i ine0
State after:
no goals

State before:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
⊢ Summable maj
Tactic:
by_cases Ceq0 : C = 0
State after:
case pos
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : C = 0
⊢ Summable maj

case neg
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ Summable maj

State before:
case pos
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : C = 0
⊢ Summable maj

case neg
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ Summable maj
Tactic:
. rw [maj_def, Ceq0]
  simp only [one_div, mul_zero]
  exact summable_zero
State after:
case neg
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ Summable maj

State before:
case neg
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ Summable maj
Tactic:
. rw [← summable_div_const_iff Ceq0]
  convert Real.summable_one_div_int_pow.mpr one_lt_two using 1
  rw [maj_def]
  ext i
  simp only [one_div]
  rw [mul_div_cancel_right₀]
  exact Ceq0
State after:
no goals

State before:
case pos
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : C = 0
⊢ Summable maj
Tactic:
rw [maj_def, Ceq0]
State after:
case pos
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : C = 0
⊢ Summable fun i => 1 / ↑i ^ 2 * 0

State before:
case pos
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : C = 0
⊢ Summable fun i => 1 / ↑i ^ 2 * 0
Tactic:
simp only [one_div, mul_zero]
State after:
case pos
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : C = 0
⊢ Summable fun i => 0

State before:
case pos
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : C = 0
⊢ Summable fun i => 0
Tactic:
exact summable_zero
State after:
no goals

State before:
case neg
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ Summable maj
Tactic:
rw [← summable_div_const_iff Ceq0]
State after:
case neg
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ Summable fun i => maj i / C

State before:
case neg
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ Summable fun i => maj i / C
Tactic:
convert Real.summable_one_div_int_pow.mpr one_lt_two using 1
State after:
case h.e'_5
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ (fun i => maj i / C) = fun n => 1 / ↑n ^ 2

State before:
case h.e'_5
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ (fun i => maj i / C) = fun n => 1 / ↑n ^ 2
Tactic:
rw [maj_def]
State after:
case h.e'_5
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ (fun i => (fun i => 1 / ↑i ^ 2 * C) i / C) = fun n => 1 / ↑n ^ 2

State before:
case h.e'_5
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
⊢ (fun i => (fun i => 1 / ↑i ^ 2 * C) i / C) = fun n => 1 / ↑n ^ 2
Tactic:
ext i
State after:
case h.e'_5.h
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
i : ℤ
⊢ (fun i => 1 / ↑i ^ 2 * C) i / C = 1 / ↑i ^ 2

State before:
case h.e'_5.h
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
i : ℤ
⊢ (fun i => 1 / ↑i ^ 2 * C) i / C = 1 / ↑i ^ 2
Tactic:
simp only [one_div]
State after:
case h.e'_5.h
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
i : ℤ
⊢ (↑i ^ 2)⁻¹ * C / C = (↑i ^ 2)⁻¹

State before:
case h.e'_5.h
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
i : ℤ
⊢ (↑i ^ 2)⁻¹ * C / C = (↑i ^ 2)⁻¹
Tactic:
rw [mul_div_cancel_right₀]
State after:
case h.e'_5.h.hb
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
i : ℤ
⊢ C ≠ 0

State before:
case h.e'_5.h.hb
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
Ceq0 : ¬C = 0
i : ℤ
⊢ C ≠ 0
Tactic:
exact Ceq0
State after:
no goals

State before:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ 0 ≤ fun x => ‖fourierCoeffOn ⋯ f x‖
Tactic:
intro i
State after:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
i : ℤ
⊢ 0 i ≤ (fun x => ‖fourierCoeffOn ⋯ f x‖) i

State before:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
i : ℤ
⊢ 0 i ≤ (fun x => ‖fourierCoeffOn ⋯ f x‖) i
Tactic:
simp
State after:
no goals

State before:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
⊢ ∀ (i : ℤ), i ≠ 0 → ‖fourierCoeffOn ⋯ f i‖ ≤ maj i
Tactic:
intro i ine0
State after:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
i : ℤ
ine0 : i ≠ 0
⊢ ‖fourierCoeffOn ⋯ f i‖ ≤ maj i

State before:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
i : ℤ
ine0 : i ≠ 0
⊢ ‖fourierCoeffOn ⋯ f i‖ ≤ maj i
Tactic:
rw [maj_def, Complex.norm_eq_abs]
State after:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
i : ℤ
ine0 : i ≠ 0
⊢ Complex.abs (fourierCoeffOn ⋯ f i) ≤ (fun i => 1 / ↑i ^ 2 * C) i

State before:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
i : ℤ
ine0 : i ≠ 0
⊢ Complex.abs (fourierCoeffOn ⋯ f i) ≤ (fun i => 1 / ↑i ^ 2 * C) i
Tactic:
field_simp
State after:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
i : ℤ
ine0 : i ≠ 0
⊢ Complex.abs (fourierCoeffOn ⋯ f i) ≤ C / ↑i ^ 2

State before:
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
C : ℝ
hC : ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
maj : ℤ → ℝ := fun i => 1 / ↑i ^ 2 * C
maj_def : maj = fun i => 1 / ↑i ^ 2 * C
summable_maj : Summable maj
i : ℤ
ine0 : i ≠ 0
⊢ Complex.abs (fourierCoeffOn ⋯ f i) ≤ C / ↑i ^ 2
Tactic:
exact hC i ine0
State after:
no goals

State before:
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
Tactic:
rw [g_def, ContinuousMap.coe_mk]
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 = AddCircle.liftIco (2 * Real.pi) 0 f ↑x

State before:
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 = AddCircle.liftIco (2 * Real.pi) 0 f ↑x
Tactic:
by_cases h : x = 2 * Real.pi
State after:
case pos
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) < ε
h : x = 2 * Real.pi
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x

case neg
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) < ε
h : ¬x = 2 * Real.pi
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x

State before:
case pos
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) < ε
h : x = 2 * Real.pi
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x

case neg
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) < ε
h : ¬x = 2 * Real.pi
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x
Tactic:
. conv => lhs; rw [h, ← zero_add  (2 * Real.pi), periodicf]
  have := AddCircle.coe_add_period (2 * Real.pi) 0
  rw [zero_add] at this
  rw [h, this, AddCircle.liftIco_coe_apply]
  simp [Real.pi_pos]
State after:
case neg
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) < ε
h : ¬x = 2 * Real.pi
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x

State before:
case neg
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) < ε
h : ¬x = 2 * Real.pi
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x
Tactic:
. have : x ∈ Set.Ico 0 (2 * Real.pi) := by
    use hx.1
    apply lt_of_le_of_ne hx.2 h
  rw [AddCircle.liftIco_coe_apply]
  rw [zero_add]
  exact this
State after:
no goals

State before:
case pos
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) < ε
h : x = 2 * Real.pi
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x
Tactic:
conv => lhs; rw [h, ← zero_add  (2 * Real.pi), periodicf]
State after:
case pos
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) < ε
h : x = 2 * Real.pi
⊢ f 0 = AddCircle.liftIco (2 * Real.pi) 0 f ↑x

State before:
case pos
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) < ε
h : x = 2 * Real.pi
⊢ f 0 = AddCircle.liftIco (2 * Real.pi) 0 f ↑x
Tactic:
have := AddCircle.coe_add_period (2 * Real.pi) 0
State after:
case pos
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) < ε
h : x = 2 * Real.pi
this : ↑(0 + 2 * Real.pi) = ↑0
⊢ f 0 = AddCircle.liftIco (2 * Real.pi) 0 f ↑x

State before:
case pos
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) < ε
h : x = 2 * Real.pi
this : ↑(0 + 2 * Real.pi) = ↑0
⊢ f 0 = AddCircle.liftIco (2 * Real.pi) 0 f ↑x
Tactic:
rw [zero_add] at this
State after:
case pos
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) < ε
h : x = 2 * Real.pi
this : ↑(2 * Real.pi) = ↑0
⊢ f 0 = AddCircle.liftIco (2 * Real.pi) 0 f ↑x

State before:
case pos
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) < ε
h : x = 2 * Real.pi
this : ↑(2 * Real.pi) = ↑0
⊢ f 0 = AddCircle.liftIco (2 * Real.pi) 0 f ↑x
Tactic:
rw [h, this, AddCircle.liftIco_coe_apply]
State after:
case pos
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) < ε
h : x = 2 * Real.pi
this : ↑(2 * Real.pi) = ↑0
⊢ 0 ∈ Set.Ico 0 (0 + 2 * Real.pi)

State before:
case pos
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) < ε
h : x = 2 * Real.pi
this : ↑(2 * Real.pi) = ↑0
⊢ 0 ∈ Set.Ico 0 (0 + 2 * Real.pi)
Tactic:
simp [Real.pi_pos]
State after:
no goals

State before:
case neg
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) < ε
h : ¬x = 2 * Real.pi
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x
Tactic:
have : x ∈ Set.Ico 0 (2 * Real.pi) := by
  use hx.1
  apply lt_of_le_of_ne hx.2 h
State after:
case neg
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) < ε
h : ¬x = 2 * Real.pi
this : x ∈ Set.Ico 0 (2 * Real.pi)
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x

State before:
case neg
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) < ε
h : ¬x = 2 * Real.pi
this : x ∈ Set.Ico 0 (2 * Real.pi)
⊢ f x = AddCircle.liftIco (2 * Real.pi) 0 f ↑x
Tactic:
rw [AddCircle.liftIco_coe_apply]
State after:
case neg
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) < ε
h : ¬x = 2 * Real.pi
this : x ∈ Set.Ico 0 (2 * Real.pi)
⊢ x ∈ Set.Ico 0 (0 + 2 * Real.pi)

State before:
case neg
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) < ε
h : ¬x = 2 * Real.pi
this : x ∈ Set.Ico 0 (2 * Real.pi)
⊢ x ∈ Set.Ico 0 (0 + 2 * Real.pi)
Tactic:
rw [zero_add]
State after:
case neg
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) < ε
h : ¬x = 2 * Real.pi
this : x ∈ Set.Ico 0 (2 * Real.pi)
⊢ x ∈ Set.Ico 0 (2 * Real.pi)

State before:
case neg
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) < ε
h : ¬x = 2 * Real.pi
this : x ∈ Set.Ico 0 (2 * Real.pi)
⊢ x ∈ Set.Ico 0 (2 * Real.pi)
Tactic:
exact this
State after:
no goals

State before:
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) < ε
h : ¬x = 2 * Real.pi
⊢ x ∈ Set.Ico 0 (2 * Real.pi)
Tactic:
use hx.1
State after:
case right
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) < ε
h : ¬x = 2 * Real.pi
⊢ x < 2 * Real.pi

State before:
case right
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) < ε
h : ¬x = 2 * Real.pi
⊢ x < 2 * Real.pi
Tactic:
apply lt_of_le_of_ne hx.2 h
State after:
no goals

State before:
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
Tactic:
rw [partialFourierSum]
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) < ε
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x =
    ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x

State before:
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) < ε
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x =
    ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x
Tactic:
congr
State after:
case h.e'_3.h.e'_6.e_a.e_f
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) < ε
⊢ (fun n => fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x) = fun c => (fourierCoeff (⇑g) c • fourier c) ↑x

State before:
case h.e'_3.h.e'_6.e_a.e_f
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) < ε
⊢ (fun n => fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x) = fun c => (fourierCoeff (⇑g) c • fourier c) ↑x
Tactic:
ext n
State after:
case h.e'_3.h.e'_6.e_a.e_f.h
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) < ε
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x = (fourierCoeff (⇑g) n • fourier n) ↑x

State before:
case h.e'_3.h.e'_6.e_a.e_f.h
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) < ε
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x = (fourierCoeff (⇑g) n • fourier n) ↑x
Tactic:
rw [fourierCoeff_correspondence]
State after:
case h.e'_3.h.e'_6.e_a.e_f.h
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) < ε
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x = (fourierCoeffOn ⋯ f n • fourier n) ↑x

State before:
case h.e'_3.h.e'_6.e_a.e_f.h
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) < ε
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x = (fourierCoeffOn ⋯ f n • fourier n) ↑x
Tactic:
simp
State after:
no goals