internlm/Lean-Github huggingface dataset:
Theorem: int_sum_nat
Proof state before:
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
⊢ -1 < ↑N + 1 + ↑N
Tactic:
linarith
Proof state after:
no goals
Theorem: int_sum_nat
Proof state before:
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
⊢ -Int.ofNat N.succ ≤ ↑N.succ
Tactic:
norm_num
Proof state after:
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
⊢ -1 ≤ ↑N + 1 + ↑N
Theorem: int_sum_nat
Proof state before:
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
⊢ -1 ≤ ↑N + 1 + ↑N
Tactic:
linarith
Proof state after:
no goals
Theorem: int_sum_nat
Proof state before:
case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ -Int.ofNat N.succ ∉ Icc (-Int.ofNat N) ↑N
Tactic:
simp
Proof state after:
no goals
Theorem: int_sum_nat
Proof state before:
case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ ↑N.succ ∉ insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N)
Tactic:
norm_num
Proof state after:
case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ ¬↑N + 1 = -1 + -↑N
Theorem: int_sum_nat
Proof state before:
case h.e'_3.h.succ
β : Type
inst✝² : AddCommGroup β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousAdd β
f : ℤ → β
a : β
hfa : HasSum f a
this✝¹ : Tendsto (fun n => ∑ i ∈ range n, (f ↑i + f (-↑i))) atTop (𝓝 (a + f 0))
this✝ : Tendsto (fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
N : ℕ
ih : ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
this : Icc (-Int.ofNat N.succ) ↑N.succ = insert (↑N.succ) (insert (-Int.ofNat N.succ) (Icc (-Int.ofNat N) ↑N))
⊢ ¬↑N + 1 = -1 + -↑N
Tactic:
linarith
Proof state after:
no goals
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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]
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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₀
Proof 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) ≤ ε
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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) ≤ ε