internlm/Lean-Github huggingface dataset:
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 : ℕ
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
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)
this : dist (g ↑x) ((∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeff (⇑g) n • fourier n) ↑x) < ε
⊢ 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 : ℕ
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
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)
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) ≤ ε
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 : ℕ
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
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)
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) ≤ ε
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 : ℕ
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
Proof 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
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
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
⊢ Fact (0 < 2 * Real.pi)
Tactic:
rw [fact_iff]
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
⊢ 0 < 2 * Real.pi
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
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
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]
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
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
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
⊢ Summable (fourierCoeff ⇑g)
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
⊢ Summable (fourierCoeff ⇑g)
Tactic:
obtain ⟨C, hC⟩ := fourierCoeffOn_ContDiff_two_bound periodicf fdiff
Proof 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)
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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)
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
Proof 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)
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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]
Proof 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‖
Theorem: fourierConv_ofTwiceDifferentiable
Proof 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
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
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
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
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
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
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
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
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
Proof state after:
no goals