internlm/Lean-Github huggingface dataset:
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ (fun x => 1) x • deriv f ((fun x => x + T) x) = deriv f ((fun x => x + T) x)
Tactic:
simp
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
⊢ ∃ C, ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
Tactic:
have h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x := by
  intro x _
  rw [hasDerivAt_deriv_iff]
  apply fdiff.differentiable (by norm_num)
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
⊢ ∃ C, ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
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
⊢ ∃ C, ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
Tactic:
have h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x := by
  intro x _
  rw [hasDerivAt_deriv_iff]
  apply (contDiff_succ_iff_deriv.mp fdiff).2.differentiable (by norm_num)
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
⊢ ∃ C, ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
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
⊢ ∃ C, ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
Tactic:
have fourierCoeffOn_eq {n : ℤ} (hn : n ≠ 0): (fourierCoeffOn Real.two_pi_pos f n) = - 1 / (n^2) * fourierCoeffOn Real.two_pi_pos (fun x ↦ deriv (deriv f) x) n := by
  rw [fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h, fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h']
  . have := periodicf 0
    simp at this
    simp [this]
    have periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi) := periodic_deriv (fdiff.of_le one_le_two) periodicf
    have := periodic_deriv_f 0
    simp at this
    simp [this]
    ring_nf
    simp
    left
    rw [mul_inv_cancel, one_mul]
    simp
    exact Real.pi_pos.ne.symm
  . apply Continuous.intervalIntegrable
    exact (contDiff_one_iff_deriv.mp (contDiff_succ_iff_deriv.mp fdiff).2).2
  . apply Continuous.intervalIntegrable
    exact (contDiff_succ_iff_deriv.mp fdiff).2.continuous
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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
⊢ ∃ C, ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
⊢ ∃ C, ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
Tactic:
obtain ⟨C, hC⟩ := fourierCoeffOn_bound (contDiff_one_iff_deriv.mp (contDiff_succ_iff_deriv.mp fdiff).2).2
Proof state after:
case intro
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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
⊢ ∃ C, ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
case intro
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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
⊢ ∃ C, ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
Tactic:
use C
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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
⊢ ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
⊢ ∀ (n : ℤ), n ≠ 0 → Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
Tactic:
intro n hn
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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / ↑n ^ 2
Tactic:
rw [fourierCoeffOn_eq hn]
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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ Complex.abs (-1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n) ≤ C / ↑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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ Complex.abs (-1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n) ≤ C / ↑n ^ 2
Tactic:
simp only [Nat.cast_one, Int.cast_pow, map_mul, map_div₀, map_neg_eq_map, map_one, map_pow,
  Complex.abs_intCast, sq_abs, one_div]
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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ (↑n ^ 2)⁻¹ * Complex.abs (fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n) ≤ C / ↑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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ (↑n ^ 2)⁻¹ * Complex.abs (fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n) ≤ C / ↑n ^ 2
Tactic:
rw [div_eq_mul_inv, mul_comm]
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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ Complex.abs (fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n) * (↑n ^ 2)⁻¹ ≤ C * (↑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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ Complex.abs (fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n) * (↑n ^ 2)⁻¹ ≤ C * (↑n ^ 2)⁻¹
Tactic:
gcongr
Proof state after:
case h.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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ Complex.abs (fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n) ≤ C
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
case h.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
fourierCoeffOn_eq :
  ∀ {n : ℤ},
    n ≠ 0 →
      fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
C : ℝ
hC : ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos (deriv (deriv f)) n) ≤ C
n : ℤ
hn : n ≠ 0
⊢ Complex.abs (fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n) ≤ C
Tactic:
exact hC n
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
⊢ ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x
Tactic:
intro x _
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ HasDerivAt f (deriv f x) x
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ HasDerivAt f (deriv f x) x
Tactic:
rw [hasDerivAt_deriv_iff]
Proof state after:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ DifferentiableAt ℝ f x
Theorem: fourierCoeffOn_ContDiff_two_bound
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ DifferentiableAt ℝ f x
Tactic:
apply fdiff.differentiable (by norm_num)
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
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ 1 ≤ 2
Tactic:
norm_num
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
⊢ ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x
Tactic:
intro x _
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
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ HasDerivAt (deriv f) (deriv (deriv f) x) x
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
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ HasDerivAt (deriv f) (deriv (deriv f) x) x
Tactic:
rw [hasDerivAt_deriv_iff]
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
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ DifferentiableAt ℝ (deriv f) x
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
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ DifferentiableAt ℝ (deriv f) x
Tactic:
apply (contDiff_succ_iff_deriv.mp fdiff).2.differentiable (by norm_num)
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
x : ℝ
a✝ : x ∈ Set.uIcc 0 (2 * Real.pi)
⊢ 1 ≤ ↑1
Tactic:
norm_num
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
⊢ fourierCoeffOn Real.two_pi_pos f n = -1 / ↑n ^ 2 * fourierCoeffOn Real.two_pi_pos (fun x => deriv (deriv f) x) n
Tactic:
rw [fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h, fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h']
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
⊢ 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

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)

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

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)

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:
. have := periodicf 0
  simp at this
  simp [this]
  have periodic_deriv_f : Function.Periodic (deriv f) (2 * Real.pi) := periodic_deriv (fdiff.of_le one_le_two) periodicf
  have := periodic_deriv_f 0
  simp at this
  simp [this]
  ring_nf
  simp
  left
  rw [mul_inv_cancel, one_mul]
  simp
  exact Real.pi_pos.ne.symm
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
⊢ IntervalIntegrable (fun x => deriv (deriv f) x) MeasureTheory.volume 0 (2 * Real.pi)

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

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
  exact (contDiff_one_iff_deriv.mp (contDiff_succ_iff_deriv.mp fdiff).2).2
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
⊢ IntervalIntegrable (fun x => deriv f x) MeasureTheory.volume 0 (2 * Real.pi)
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
  exact (contDiff_succ_iff_deriv.mp fdiff).2.continuous
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
⊢ 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:
have := periodicf 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 (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