internlm/Lean-Github huggingface dataset:
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this : f (0 + 2 * Real.pi) = f 0
⊢ 1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
      ((fourier (-n)) ↑0 * (f (2 * Real.pi) - f 0) -
        (↑(2 * Real.pi) - ↑0) *
          (1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
            ((fourier (-n)) ↑0 * (deriv f (2 * Real.pi) - deriv f 0) -
              (↑(2 * Real.pi) - ↑0) * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Tactic:
simp at this
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this : f (2 * Real.pi) = f 0
⊢ 1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
      ((fourier (-n)) ↑0 * (f (2 * Real.pi) - f 0) -
        (↑(2 * Real.pi) - ↑0) *
          (1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
            ((fourier (-n)) ↑0 * (deriv f (2 * Real.pi) - deriv f 0) -
              (↑(2 * Real.pi) - ↑0) * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this : f (2 * Real.pi) = f 0
⊢ 1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
      ((fourier (-n)) ↑0 * (f (2 * Real.pi) - f 0) -
        (↑(2 * Real.pi) - ↑0) *
          (1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
            ((fourier (-n)) ↑0 * (deriv f (2 * Real.pi) - deriv f 0) -
              (↑(2 * Real.pi) - ↑0) * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Tactic:
simp [this]
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this : f (2 * Real.pi) = f 0
⊢ -((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
        (2 * ↑Real.pi *
          ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
            (↑(AddCircle.toCircle 0) * (deriv f (2 * Real.pi) - deriv f 0) -
              2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n)))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this : f (2 * Real.pi) = f 0
⊢ -((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
        (2 * ↑Real.pi *
          ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
            (↑(AddCircle.toCircle 0) * (deriv f (2 * Real.pi) - deriv f 0) -
              2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n)))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Tactic:
have periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi) := periodic_deriv (fdiff.of_le one_le_two) periodicf
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
⊢ -((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
        (2 * ↑Real.pi *
          ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
            (↑(AddCircle.toCircle 0) * (deriv f (2 * Real.pi) - deriv f 0) -
              2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n)))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
⊢ -((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
        (2 * ↑Real.pi *
          ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
            (↑(AddCircle.toCircle 0) * (deriv f (2 * Real.pi) - deriv f 0) -
              2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n)))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Tactic:
have := periodic_deriv_f 0
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (0 + 2 * Real.pi) = deriv f 0
⊢ -((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
        (2 * ↑Real.pi *
          ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
            (↑(AddCircle.toCircle 0) * (deriv f (2 * Real.pi) - deriv f 0) -
              2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n)))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (0 + 2 * Real.pi) = deriv f 0
⊢ -((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
        (2 * ↑Real.pi *
          ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
            (↑(AddCircle.toCircle 0) * (deriv f (2 * Real.pi) - deriv f 0) -
              2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n)))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Tactic:
simp at this
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ -((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
        (2 * ↑Real.pi *
          ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
            (↑(AddCircle.toCircle 0) * (deriv f (2 * Real.pi) - deriv f 0) -
              2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n)))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ -((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
        (2 * ↑Real.pi *
          ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
            (↑(AddCircle.toCircle 0) * (deriv f (2 * Real.pi) - deriv f 0) -
              2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n)))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Tactic:
simp [this]
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ (-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
      (2 * ↑Real.pi *
        ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
          (2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ (-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
      (2 * ↑Real.pi *
        ((-(2 * ↑Real.pi * Complex.I * ↑n))⁻¹ *
          (2 * ↑Real.pi * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n))) =
    -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Tactic:
ring_nf
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ↑Real.pi ^ 2 * (↑Real.pi)⁻¹ ^ 2 * Complex.I⁻¹ ^ 2 * (↑n)⁻¹ ^ 2 * fourierCoeffOn ⋯ (fun x => deriv (deriv f) x) n =
    -((↑n)⁻¹ ^ 2 * fourierCoeffOn ⋯ (fun x => deriv (deriv f) x) n)
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ↑Real.pi ^ 2 * (↑Real.pi)⁻¹ ^ 2 * Complex.I⁻¹ ^ 2 * (↑n)⁻¹ ^ 2 * fourierCoeffOn ⋯ (fun x => deriv (deriv f) x) n =
    -((↑n)⁻¹ ^ 2 * fourierCoeffOn ⋯ (fun x => deriv (deriv f) x) n)
Tactic:
simp
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ↑Real.pi ^ 2 * (↑Real.pi ^ 2)⁻¹ * (↑n ^ 2)⁻¹ = (↑n ^ 2)⁻¹ ∨ fourierCoeffOn ⋯ (fun x => deriv (deriv f) x) n = 0
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ↑Real.pi ^ 2 * (↑Real.pi ^ 2)⁻¹ * (↑n ^ 2)⁻¹ = (↑n ^ 2)⁻¹ ∨ fourierCoeffOn ⋯ (fun x => deriv (deriv f) x) n = 0
Tactic:
left
Proof state after:
case h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ↑Real.pi ^ 2 * (↑Real.pi ^ 2)⁻¹ * (↑n ^ 2)⁻¹ = (↑n ^ 2)⁻¹
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
case h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ↑Real.pi ^ 2 * (↑Real.pi ^ 2)⁻¹ * (↑n ^ 2)⁻¹ = (↑n ^ 2)⁻¹
Tactic:
rw [mul_inv_cancel, one_mul]
Proof state after:
case h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ↑Real.pi ^ 2 ≠ 0
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
case h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ↑Real.pi ^ 2 ≠ 0
Tactic:
simp
Proof state after:
case h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ¬Real.pi = 0
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
case h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
this✝ : f (2 * Real.pi) = f 0
periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi)
this : deriv f (2 * Real.pi) = deriv f 0
⊢ ¬Real.pi = 0
Tactic:
exact Real.pi_pos.ne.symm
Proof state after:
no goals
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
⊢ IntervalIntegrable (fun x => deriv (deriv f) x) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
apply Continuous.intervalIntegrable
Proof state after:
case hu
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
⊢ Continuous fun x => deriv (deriv f) x
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
case hu
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
⊢ Continuous fun x => deriv (deriv f) x
Tactic:
exact (contDiff_one_iff_deriv.mp (contDiff_succ_iff_deriv.mp fdiff).2).2
Proof state after:
no goals
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
⊢ IntervalIntegrable (fun x => deriv f x) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
apply Continuous.intervalIntegrable
Proof state after:
case hu
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
⊢ Continuous fun x => deriv f x
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
case hu
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
n : ℤ
hn : n ≠ 0
⊢ Continuous fun x => deriv f x
Tactic:
exact (contDiff_succ_iff_deriv.mp fdiff).2.continuous
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
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
have := hfa.nat_add_neg.tendsto_sum_nat
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))
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
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))
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
have := (Filter.Tendsto.add_const (- (f 0))) this
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 k => ∑ i ∈ range k, (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 (a + f 0 + -f 0))
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
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 k => ∑ i ∈ range k, (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 (a + f 0 + -f 0))
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
simp at this
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 k => ∑ i ∈ range k, (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
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 k => ∑ i ∈ range k, (f ↑i + f (-↑i)) + -f 0) atTop (𝓝 a)
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
rw [←tendsto_add_atTop_iff_nat 1] at this
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)
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
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)
⊢ Tendsto (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) atTop (𝓝 a)
Tactic:
convert this using 1
Proof state after:
case h.e'_3
β : 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)
⊢ (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) = fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0
Theorem: int_sum_nat
Proof state before:
case h.e'_3
β : 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)
⊢ (fun N => ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n) = fun n => ∑ i ∈ range (n + 1), (f ↑i + f (-↑i)) + -f 0
Tactic:
ext N
Proof state after:
case h.e'_3.h
β : 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 : ℕ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
Theorem: int_sum_nat
Proof state before:
case h.e'_3.h
β : 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 : ℕ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, f n = ∑ i ∈ range (N + 1), (f ↑i + f (-↑i)) + -f 0
Tactic:
induction' N with N ih
Proof state after:
case h.e'_3.h.zero
β : 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 ∈ Icc (-Int.ofNat 0) ↑0, f n = ∑ i ∈ range (0 + 1), (f ↑i + f (-↑i)) + -f 0

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
⊢ ∑ n ∈ Icc (-Int.ofNat (N + 1)) ↑(N + 1), f n = ∑ i ∈ range (N + 1 + 1), (f ↑i + f (-↑i)) + -f 0