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

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

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

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

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

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

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

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

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

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]
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)⁻¹

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

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
State after:
no goals

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

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

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)
State after:
no goals

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
State after:
no goals

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

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

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)
State after:
no goals

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
State after:
no goals

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

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

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

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
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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
State after:
no goals

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

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
State after:
no goals

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

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
State after:
no goals