[GOAL]
k : ℕ
⊢ bernoulliFun k 0 = ↑(bernoulli k)
[PROOFSTEP]
rw [bernoulliFun, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]
[GOAL]
k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 1 = bernoulliFun k 0
[PROOFSTEP]
rw [bernoulliFun_eval_zero, bernoulliFun, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one,
  bernoulli_eq_bernoulli'_of_ne_one hk, eq_ratCast]
[GOAL]
k : ℕ
⊢ bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0
[PROOFSTEP]
rw [bernoulliFun, bernoulliFun_eval_zero, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one]
[GOAL]
k : ℕ
⊢ ↑(algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + if k = 1 then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
k : ℕ
h : k = 1
⊢ ↑(algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 1
[PROOFSTEP]
rw [h, bernoulli_one, bernoulli'_one, eq_ratCast]
[GOAL]
case pos
k : ℕ
h : k = 1
⊢ ↑(1 / 2) = ↑(-1 / 2) + 1
[PROOFSTEP]
push_cast
[GOAL]
case pos
k : ℕ
h : k = 1
⊢ 1 / ↑2 = -1 / ↑2 + 1
[PROOFSTEP]
ring
[GOAL]
case neg
k : ℕ
h : ¬k = 1
⊢ ↑(algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 0
[PROOFSTEP]
rw [bernoulli_eq_bernoulli'_of_ne_one h, add_zero, eq_ratCast]
[GOAL]
k : ℕ
x : ℝ
⊢ HasDerivAt (bernoulliFun k) (↑k * bernoulliFun (k - 1) x) x
[PROOFSTEP]
convert ((Polynomial.bernoulli k).map <| algebraMap ℚ ℝ).hasDerivAt x using 1
[GOAL]
case h.e'_7
k : ℕ
x : ℝ
⊢ ↑k * bernoulliFun (k - 1) x =
    Polynomial.eval x (↑Polynomial.derivative (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)))
[PROOFSTEP]
simp only [bernoulliFun, Polynomial.derivative_map, Polynomial.derivative_bernoulli k, Polynomial.map_mul,
  Polynomial.map_nat_cast, Polynomial.eval_mul, Polynomial.eval_nat_cast]
[GOAL]
k : ℕ
x : ℝ
⊢ HasDerivAt (fun x => bernoulliFun (k + 1) x / (↑k + 1)) (bernoulliFun k x) x
[PROOFSTEP]
convert (hasDerivAt_bernoulliFun (k + 1) x).div_const _ using 1
[GOAL]
case h.e'_7
k : ℕ
x : ℝ
⊢ bernoulliFun k x = ↑(k + 1) * bernoulliFun (k + 1 - 1) x / (↑k + 1)
[PROOFSTEP]
field_simp [Nat.cast_add_one_ne_zero k]
[GOAL]
case h.e'_7
k : ℕ
x : ℝ
⊢ bernoulliFun k x * (↑k + 1) = (↑k + 1) * bernoulliFun k x
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ ∫ (x : ℝ) in 0 ..1, bernoulliFun k x = 0
[PROOFSTEP]
rw [integral_eq_sub_of_hasDerivAt (fun x _ => antideriv_bernoulliFun k x)
    ((Polynomial.continuous _).intervalIntegrable _ _)]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ bernoulliFun (k + 1) 1 / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0
[PROOFSTEP]
rw [bernoulliFun_eval_one]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ (bernoulliFun (k + 1) 0 + if k + 1 = 1 then 1 else 0) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
k : ℕ
hk : k ≠ 0
h : k + 1 = 1
⊢ (bernoulliFun (k + 1) 0 + 1) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
k : ℕ
hk : k ≠ 0
h : k + 1 = 1
⊢ False
[PROOFSTEP]
exact hk (Nat.succ_inj'.mp h)
[GOAL]
case neg
k : ℕ
hk : k ≠ 0
h : ¬k + 1 = 1
⊢ (bernoulliFun (k + 1) 0 + 0) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0
[PROOFSTEP]
simp
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)
[PROOFSTEP]
unfold bernoulliFourierCoeff
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun k x)) n =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
[PROOFSTEP]
rw [fourierCoeffOn_of_hasDerivAt zero_lt_one hn (fun x _ => (hasDerivAt_bernoulliFun k x).ofReal_comp)
    ((continuous_ofReal.comp <| continuous_const.mul <| Polynomial.continuous _).intervalIntegrable _ _)]
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      (↑(fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        (↑1 - ↑0) * fourierCoeffOn (_ : 0 < 1) (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
[PROOFSTEP]
simp_rw [ofReal_one, ofReal_zero, sub_zero, one_mul]
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      (↑(fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        fourierCoeffOn (_ : 0 < 1) (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
[PROOFSTEP]
rw [QuotientAddGroup.mk_zero, fourier_eval_zero, one_mul, ← ofReal_sub, bernoulliFun_eval_one, add_sub_cancel']
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      (↑(if k = 1 then 1 else 0) - fourierCoeffOn (_ : 0 < 1) (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ ↑(if k = 1 then 1 else 0) = if k = 1 then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
k : ℕ
n : ℤ
hn : n ≠ 0
h✝ : k = 1
⊢ ↑1 = 1
[PROOFSTEP]
simp only [ofReal_one, ofReal_zero, one_mul]
[GOAL]
case neg
k : ℕ
n : ℤ
hn : n ≠ 0
h✝ : ¬k = 1
⊢ ↑0 = 0
[PROOFSTEP]
simp only [ofReal_one, ofReal_zero, one_mul]
[GOAL]
case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn (_ : 0 < 1) (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n =
    ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n
[PROOFSTEP]
simp_rw [ofReal_mul, ofReal_nat_cast, fourierCoeffOn.const_mul]
[GOAL]
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 0 n = 0
[PROOFSTEP]
simpa using bernoulliFourierCoeff_recurrence 0 hn
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = 0
[PROOFSTEP]
simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero, div_one, one_smul,
  intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk, ofReal_zero]
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = -↑k ! / (2 * ↑π * I * ↑0) ^ k
[PROOFSTEP]
rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow' _ hk, div_zero]
[GOAL]
case inr
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
refine' Nat.le_induction _ (fun k hk h'k => _) k (Nat.one_le_iff_ne_zero.mpr hk)
[GOAL]
case inr.refine'_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 1 n = -↑1! / (2 * ↑π * I * ↑n) ^ 1
[PROOFSTEP]
rw [bernoulliFourierCoeff_recurrence 1 hn]
[GOAL]
case inr.refine'_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if 1 = 1 then 1 else 0) - ↑1 * bernoulliFourierCoeff (1 - 1) n) =
    -↑1! / (2 * ↑π * I * ↑n) ^ 1
[PROOFSTEP]
simp only [Nat.cast_one, tsub_self, neg_mul, one_mul, eq_self_iff_true, if_true, Nat.factorial_one, pow_one, inv_I,
  mul_neg]
[GOAL]
case inr.refine'_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / -(2 * ↑π * I * ↑n) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * ↑π * I * ↑n)
[PROOFSTEP]
rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]
[GOAL]
case inr.refine'_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ bernoulliFourierCoeff (k + 1) n = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
[PROOFSTEP]
rw [bernoulliFourierCoeff_recurrence (k + 1) hn, Nat.add_sub_cancel k 1]
[GOAL]
case inr.refine'_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if k + 1 = 1 then 1 else 0) - ↑(k + 1) * bernoulliFourierCoeff k n) =
    -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : k + 1 = 1
⊢ 1 / (-2 * ↑π * I * ↑n) * (1 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : k + 1 = 1
⊢ False
[PROOFSTEP]
exact (ne_of_gt (Nat.lt_succ_iff.mpr hk)) h
[GOAL]
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ 1 / (-2 * ↑π * I * ↑n) * (0 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
[PROOFSTEP]
rw [h'k, Nat.factorial_succ, zero_sub, Nat.cast_mul, pow_add, pow_one, neg_div, mul_neg, mul_neg, mul_neg, neg_neg,
  neg_mul, neg_mul, neg_mul, div_neg]
[GOAL]
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ -(1 / (2 * ↑π * I * ↑n)) * (↑(k + 1) * (↑k ! / (2 * ↑π * I * ↑n) ^ k)) =
    -(↑(k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n))
[PROOFSTEP]
field_simp [Int.cast_ne_zero.mpr hn, I_ne_zero]
[GOAL]
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ -((↑k + 1) * ↑k !) / (2 * ↑π * I * ↑n * (2 * ↑π * I * ↑n) ^ k) =
    -((↑k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n))
[PROOFSTEP]
ring_nf
[GOAL]
k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 0 = bernoulliFun k 1
[PROOFSTEP]
exact_mod_cast (bernoulliFun_endpoints_eq_of_ne_one hk).symm
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ fourierCoeff (ofReal' ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
have : ((↑) ∘ periodizedBernoulli k : 𝕌 → ℂ) = AddCircle.liftIco 1 0 ((↑) ∘ bernoulliFun k) := by ext1 x; rfl
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ ofReal' ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k)
[PROOFSTEP]
ext1 x
[GOAL]
case h
k : ℕ
hk : k ≠ 0
n : ℤ
x : 𝕌
⊢ (ofReal' ∘ periodizedBernoulli k) x = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k) x
[PROOFSTEP]
rfl
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal' ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k)
⊢ fourierCoeff (ofReal' ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
rw [this, fourierCoeff_liftIco_eq]
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal' ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k)
⊢ fourierCoeffOn (_ : 0 < 0 + 1) (ofReal' ∘ bernoulliFun k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
simpa only [zero_add] using bernoulliFourierCoeff_eq hk n
[GOAL]
k : ℕ
hk : 2 ≤ k
⊢ Summable fun n => -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
have : ∀ n : ℤ, -(k ! : ℂ) / (2 * π * I * n) ^ k = -k ! / (2 * π * I) ^ k * (1 / (n : ℂ) ^ k) := by intro n;
  rw [mul_one_div, div_div, ← mul_pow]
[GOAL]
k : ℕ
hk : 2 ≤ k
⊢ ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
[PROOFSTEP]
intro n
[GOAL]
k : ℕ
hk : 2 ≤ k
n : ℤ
⊢ -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
[PROOFSTEP]
rw [mul_one_div, div_div, ← mul_pow]
[GOAL]
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n => -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
simp_rw [this]
[GOAL]
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n => -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
[PROOFSTEP]
apply Summable.mul_left
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun i => 1 / ↑i ^ k
[PROOFSTEP]
rw [← summable_norm_iff]
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun x => ‖1 / ↑x ^ k‖
[PROOFSTEP]
have : (fun x : ℤ => ‖1 / (x : ℂ) ^ k‖) = fun x : ℤ => |1 / (x : ℝ) ^ k| :=
  by
  ext1 x
  rw [norm_eq_abs, ← Complex.abs_ofReal]
  congr 1
  norm_cast
[GOAL]
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
[PROOFSTEP]
ext1 x
[GOAL]
case h
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
x : ℤ
⊢ ‖1 / ↑x ^ k‖ = |1 / ↑x ^ k|
[PROOFSTEP]
rw [norm_eq_abs, ← Complex.abs_ofReal]
[GOAL]
case h
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
x : ℤ
⊢ ↑Complex.abs (1 / ↑x ^ k) = ↑Complex.abs ↑(1 / ↑x ^ k)
[PROOFSTEP]
congr 1
[GOAL]
case h.h.e_6.h
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
x : ℤ
⊢ 1 / ↑x ^ k = ↑(1 / ↑x ^ k)
[PROOFSTEP]
norm_cast
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun x => ‖1 / ↑x ^ k‖
[PROOFSTEP]
simp_rw [this]
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun x => |1 / ↑x ^ k|
[PROOFSTEP]
rw [summable_abs_iff]
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun x => 1 / ↑x ^ k
[PROOFSTEP]
exact Real.summable_one_div_int_pow.mpr (one_lt_two.trans_le hk)
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
suffices
  ∀ {y : ℝ},
    y ∈ Ico (0 : ℝ) 1 →
      HasSum (λ (n : ℤ) => 1 / (n : ℂ) ^ k * fourier n y) (-(2 * (π : ℂ) * I) ^ k / k ! * bernoulliFun k y)
  by
  rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx 
  rcases hx with (hx | rfl)
  · exact this hx
  · convert this (left_mem_Ico.mpr zero_lt_one) using 1
    · rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]
    · rw [bernoulliFun_endpoints_eq_of_ne_one (by linarith : k ≠ 1)]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx 
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx✝ : x ∈ Icc 0 1
hx : x ∈ Ico 0 1 ∨ x = 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
rcases hx with (hx | rfl)
[GOAL]
case inl
k : ℕ
hk : 2 ≤ k
x : ℝ
hx✝ : x ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
hx : x ∈ Ico 0 1
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
exact this hx
[GOAL]
case inr
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑1) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 1))
[PROOFSTEP]
convert this (left_mem_Ico.mpr zero_lt_one) using 1
[GOAL]
case h.e'_5
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑1) = fun n => 1 / ↑n ^ k * ↑(fourier n) ↑0
[PROOFSTEP]
rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]
[GOAL]
case h.e'_6
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 1) = -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 0)
[PROOFSTEP]
rw [bernoulliFun_endpoints_eq_of_ne_one (by linarith : k ≠ 1)]
[GOAL]
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ k ≠ 1
[PROOFSTEP]
linarith
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
intro y hy
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
let B : C(𝕌, ℂ) :=
  ContinuousMap.mk ((↑) ∘ periodizedBernoulli k) (continuous_ofReal.comp (periodizedBernoulli.continuous (by linarith)))
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
⊢ k ≠ 1
[PROOFSTEP]
linarith
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
have step1 : ∀ n : ℤ, fourierCoeff B n = -k ! / (2 * π * I * n) ^ k := by rw [ContinuousMap.coe_mk];
  exact fourierCoeff_bernoulli_eq (by linarith : k ≠ 0)
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
⊢ ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
rw [ContinuousMap.coe_mk]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
⊢ ∀ (n : ℤ), fourierCoeff (ofReal' ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
exact fourierCoeff_bernoulli_eq (by linarith : k ≠ 0)
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
⊢ k ≠ 0
[PROOFSTEP]
linarith
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
have step2 :=
  has_pointwise_sum_fourier_series_of_summable ((summable_bernoulli_fourier hk).congr fun n => (step1 n).symm) y
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i => fourierCoeff (↑B) i • ↑(fourier i) ↑y) (↑B ↑y)
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
simp_rw [step1] at step2 
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
convert step2.mul_left (-(2 * ↑π * I) ^ k / (k ! : ℂ)) using 2 with n
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
n : ℤ
⊢ 1 / ↑n ^ k * ↑(fourier n) ↑y = -(2 * ↑π * I) ^ k / ↑k ! * (-↑k ! / (2 * ↑π * I * ↑n) ^ k) • ↑(fourier n) ↑y
case h.e'_6.h.e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
⊢ ↑(bernoulliFun k y) = ↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y
[PROOFSTEP]
rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel, neg_neg, mul_pow _ (n : ℂ), ← div_div, div_self]
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
n : ℤ
⊢ (2 * ↑π * I) ^ k ≠ 0
[PROOFSTEP]
rw [Ne.def, pow_eq_zero_iff', not_and_or]
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
n : ℤ
⊢ ¬2 * ↑π * I = 0 ∨ ¬k ≠ 0
[PROOFSTEP]
exact Or.inl two_pi_I_ne_zero
[GOAL]
case h.e'_5.h.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
n : ℤ
⊢ ↑k ! ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
[GOAL]
case h.e'_6.h.e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
⊢ ↑(bernoulliFun k y) = ↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y
[PROOFSTEP]
rw [ContinuousMap.coe_mk, Function.comp_apply, ofReal_inj, periodizedBernoulli,
  AddCircle.liftIco_coe_apply (by rwa [zero_add])]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
⊢ y ∈ Ico 0 (0 + 1)
[PROOFSTEP]
rwa [zero_add]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ k * (↑(fourier ↑n) ↑x + (-1) ^ k * ↑(fourier (-↑n)) ↑x))
    (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
convert (hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).sum_nat_of_sum_int using 1
[GOAL]
case h.e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n => 1 / ↑n ^ k * (↑(fourier ↑n) ↑x + (-1) ^ k * ↑(fourier (-↑n)) ↑x)) = fun n =>
    1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (↑(fourier ↑n) ↑x + (-1) ^ k * ↑(fourier (-↑n)) ↑x) =
    1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
rw [Int.cast_neg, mul_add, ← mul_assoc]
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * ↑(fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * ↑(fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
conv_rhs => rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
| 1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
| 1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
| 1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * ↑(fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * ↑(fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-1) ^ k / ↑↑n ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_5.h.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (-1) ^ k = 1 / (-1) ^ k / ↑↑n ^ k
[PROOFSTEP]
rw [div_mul_eq_mul_div₀, one_mul]
[GOAL]
case h.e'_5.h.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k / ↑n ^ k = 1 / (-1) ^ k / ↑↑n ^ k
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_5.h.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k = 1 / (-1) ^ k
[PROOFSTEP]
rw [eq_div_iff, ← mul_pow, ← neg_eq_neg_one_mul, neg_neg, one_pow]
[GOAL]
case h.e'_5.h.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case h.e'_5.h.e_a.e_a.e_a.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ -1 ≠ 0
[PROOFSTEP]
rw [neg_ne_zero]
[GOAL]
case h.e'_5.h.e_a.e_a.e_a.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
case h.e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) =
    -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 1 / ↑0 ^ k * ↑(fourier 0) ↑x
[PROOFSTEP]
rw [Int.cast_zero, zero_pow (by linarith : 0 < k), div_zero, zero_mul, add_zero]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ 0 < k
[PROOFSTEP]
linarith
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
have :
  HasSum (fun n : ℕ => 1 / (n : ℂ) ^ (2 * k) * (fourier n (x : 𝕌) + fourier (-n) (x : 𝕌)))
    ((-1 : ℂ) ^ (k + 1) * (2 * (π : ℂ)) ^ (2 * k) / (2 * k)! * bernoulliFun (2 * k) x) :=
  by
  convert hasSum_one_div_nat_pow_mul_fourier (by linarith [Nat.one_le_iff_ne_zero.mpr hk] : 2 ≤ 2 * k) hx using 3
  · rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
  · rw [pow_add, pow_one]
    conv_rhs =>
      rw [mul_pow]
      congr
      congr
      ·skip
      ·rw [pow_mul, I_sq]
    ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
[PROOFSTEP]
convert hasSum_one_div_nat_pow_mul_fourier (by linarith [Nat.one_le_iff_ne_zero.mpr hk] : 2 ≤ 2 * k) hx using 3
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ 2 ≤ 2 * k
[PROOFSTEP]
linarith [Nat.one_le_iff_ne_zero.mpr hk]
[GOAL]
case h.e'_5.h.h.e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
x✝ : ℕ
⊢ ↑(fourier ↑x✝) ↑x + ↑(fourier (-↑x✝)) ↑x = ↑(fourier ↑x✝) ↑x + (-1) ^ (2 * k) * ↑(fourier (-↑x✝)) ↑x
[PROOFSTEP]
rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
[GOAL]
case h.e'_6.h.e'_5.h.e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
rw [pow_add, pow_one]
[GOAL]
case h.e'_6.h.e'_5.h.e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
conv_rhs =>
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
rw [mul_pow]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -((2 * ↑π) ^ (2 * k) * I ^ (2 * k))
[PROOFSTEP]
congr
[GOAL]
case a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k) * I ^ (2 * k)
[PROOFSTEP]
congr
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k)
case a.a k : ℕ hk : k ≠ 0 x : ℝ hx : x ∈ Icc 0 1 | I ^ (2 * k)
[PROOFSTEP]
·skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)
[PROOFSTEP]
·rw [pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)
[PROOFSTEP]
rw [pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)
[PROOFSTEP]
rw [pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)
[PROOFSTEP]
rw [pow_mul, I_sq]
[GOAL]
case h.e'_6.h.e'_5.h.e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * (2 * ↑π) ^ (2 * k) = -((2 * ↑π) ^ (2 * k) * (-1) ^ k)
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
have ofReal_two : ((2 : ℝ) : ℂ) = 2 := by norm_cast
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
⊢ ↑2 = 2
[PROOFSTEP]
norm_cast
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
convert ((hasSum_iff _ _).mp (this.div_const 2)).1 with n
[GOAL]
case h.e'_5.h
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x) = (1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2).re
[PROOFSTEP]
convert (ofReal_re _).symm
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2 = ↑(1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x))
[PROOFSTEP]
rw [ofReal_mul]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2 = ↑(1 / ↑n ^ (2 * k)) * ↑(Real.cos (2 * π * ↑n * x))
[PROOFSTEP]
rw [← mul_div]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * ((↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2) = ↑(1 / ↑n ^ (2 * k)) * ↑(Real.cos (2 * π * ↑n * x))
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = ↑(1 / ↑n ^ (2 * k))
[PROOFSTEP]
rw [ofReal_div, ofReal_one, ofReal_pow]
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑↑n ^ (2 * k)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2 = ↑(Real.cos (2 * π * ↑n * x))
[PROOFSTEP]
rw [ofReal_cos, ofReal_mul, fourier_coe_apply, fourier_coe_apply, cos, ofReal_one, div_one, div_one, ofReal_mul,
  ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_ofNat, ofReal_nat_cast]
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (exp (2 * ↑π * I * ↑n * ↑x) + exp (2 * ↑π * I * -↑n * ↑x)) / 2 =
    (exp (2 * ↑π * ↑n * ↑x * I) + exp (-(2 * ↑π * ↑n * ↑x) * I)) / 2
[PROOFSTEP]
congr 3
[GOAL]
case h.e'_3.h.e'_1.e_a.e_a.e_a.e_z
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 2 * ↑π * I * ↑n * ↑x = 2 * ↑π * ↑n * ↑x * I
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.e'_1.e_a.e_a.e_a.e_z
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 2 * ↑π * I * -↑n * ↑x = -(2 * ↑π * ↑n * ↑x) * I
[PROOFSTEP]
ring
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))) =
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2).re
[PROOFSTEP]
convert (ofReal_re _).symm
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2 =
    ↑((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg, ofReal_nat_cast, ofReal_mul,
  ofReal_two, ofReal_one]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
rw [bernoulliFun]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! *
        ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) /
      2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
have :
  HasSum (fun n : ℕ => 1 / (n : ℂ) ^ (2 * k + 1) * (fourier n (x : 𝕌) - fourier (-n) (x : 𝕌)))
    ((-1 : ℂ) ^ (k + 1) * I * (2 * π : ℂ) ^ (2 * k + 1) / (2 * k + 1)! * bernoulliFun (2 * k + 1) x) :=
  by
  convert hasSum_one_div_nat_pow_mul_fourier (by linarith [Nat.one_le_iff_ne_zero.mpr hk] : 2 ≤ 2 * k + 1) hx using 1
  · ext1 n
    rw [pow_add (-1 : ℂ), pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul, pow_one, ← neg_eq_neg_one_mul, ←
      sub_eq_add_neg]
  · congr
    rw [pow_add, pow_one]
    conv_rhs =>
      rw [mul_pow]
      congr
      congr
      ·skip
      ·rw [pow_add, pow_one, pow_mul, I_sq]
    ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
[PROOFSTEP]
convert hasSum_one_div_nat_pow_mul_fourier (by linarith [Nat.one_le_iff_ne_zero.mpr hk] : 2 ≤ 2 * k + 1) hx using 1
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ 2 ≤ 2 * k + 1
[PROOFSTEP]
linarith [Nat.one_le_iff_ne_zero.mpr hk]
[GOAL]
case h.e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x)) = fun n =>
    1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x + (-1) ^ (2 * k + 1) * ↑(fourier (-↑n)) ↑x)
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_5.h
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x) =
    1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x + (-1) ^ (2 * k + 1) * ↑(fourier (-↑n)) ↑x)
[PROOFSTEP]
rw [pow_add (-1 : ℂ), pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul, pow_one, ← neg_eq_neg_one_mul, ← sub_eq_add_neg]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) =
    -(2 * ↑π * I) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x)
[PROOFSTEP]
congr
[GOAL]
case h.e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) = -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
rw [pow_add, pow_one]
[GOAL]
case h.e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * I * (2 * ↑π) ^ (2 * k + 1) = -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
conv_rhs =>
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
rw [mul_pow]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -((2 * ↑π) ^ (2 * k + 1) * I ^ (2 * k + 1))
[PROOFSTEP]
congr
[GOAL]
case a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1) * I ^ (2 * k + 1)
[PROOFSTEP]
congr
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1)
case a.a k : ℕ hk : k ≠ 0 x : ℝ hx : x ∈ Icc 0 1 | I ^ (2 * k + 1)
[PROOFSTEP]
·skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)
[PROOFSTEP]
·rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)
[PROOFSTEP]
rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)
[PROOFSTEP]
rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)
[PROOFSTEP]
rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
case h.e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * I * (2 * ↑π) ^ (2 * k + 1) = -((2 * ↑π) ^ (2 * k + 1) * ((-1) ^ k * I))
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
have ofReal_two : ((2 : ℝ) : ℂ) = 2 := by norm_cast
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
⊢ ↑2 = 2
[PROOFSTEP]
norm_cast
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
convert ((hasSum_iff _ _).mp (this.div_const (2 * I))).1
[GOAL]
case h.e'_5.h
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * Real.sin (2 * π * ↑x✝ * x) =
    (1 / ↑x✝ ^ (2 * k + 1) * (↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I)).re
[PROOFSTEP]
convert (ofReal_re _).symm
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * (↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I) =
    ↑(1 / ↑x✝ ^ (2 * k + 1) * Real.sin (2 * π * ↑x✝ * x))
[PROOFSTEP]
rw [ofReal_mul]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * (↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I) =
    ↑(1 / ↑x✝ ^ (2 * k + 1)) * ↑(Real.sin (2 * π * ↑x✝ * x))
[PROOFSTEP]
rw [← mul_div]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * ((↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I)) =
    ↑(1 / ↑x✝ ^ (2 * k + 1)) * ↑(Real.sin (2 * π * ↑x✝ * x))
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) = ↑(1 / ↑x✝ ^ (2 * k + 1))
[PROOFSTEP]
rw [ofReal_div, ofReal_one, ofReal_pow]
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) = 1 / ↑↑x✝ ^ (2 * k + 1)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I) = ↑(Real.sin (2 * π * ↑x✝ * x))
[PROOFSTEP]
rw [ofReal_sin, ofReal_mul, fourier_coe_apply, fourier_coe_apply, sin, ofReal_one, div_one, div_one, ofReal_mul,
  ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_ofNat, ofReal_nat_cast, ← div_div, div_I, div_mul_eq_mul_div₀, ←
  neg_div, ← neg_mul, neg_sub]
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (exp (2 * ↑π * I * -↑x✝ * ↑x) - exp (2 * ↑π * I * ↑x✝ * ↑x)) * I / 2 =
    (exp (-(2 * ↑π * ↑x✝ * ↑x) * I) - exp (2 * ↑π * ↑x✝ * ↑x * I)) * I / 2
[PROOFSTEP]
congr 4
[GOAL]
case h.e'_3.h.e'_1.e_a.e_a.e_a.e_a.e_z
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 2 * ↑π * I * -↑x✝ * ↑x = -(2 * ↑π * ↑x✝ * ↑x) * I
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.e'_1.e_a.e_a.e_a.e_a.e_z
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 2 * ↑π * I * ↑x✝ * ↑x = 2 * ↑π * ↑x✝ * ↑x * I
[PROOFSTEP]
ring
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))) =
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / (2 * I)).re
[PROOFSTEP]
convert (ofReal_re _).symm
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / (2 * I) =
    ↑((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg, ofReal_nat_cast, ofReal_mul,
  ofReal_two, ofReal_one, ← div_div, div_I, div_mul_eq_mul_div₀]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ -((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) * I / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
have : ∀ α β γ δ : ℂ, α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ := by intros; ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
[PROOFSTEP]
intros
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
α✝ β✝ γ✝ δ✝ : ℂ
⊢ α✝ * I * β✝ / γ✝ * δ✝ * I = I ^ 2 * α✝ * β✝ / γ✝ * δ✝
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this✝ :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
⊢ -((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) * I / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
rw [this, I_sq]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this✝ :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
⊢ -(-1 * (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
rw [bernoulliFun]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this✝ :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
⊢ -(-1 * (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! *
          ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) /
        2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k)) ((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!)
[PROOFSTEP]
convert hasSum_one_div_nat_pow_mul_cos hk (left_mem_Icc.mpr zero_le_one) using 1
[GOAL]
case h.e'_5
k : ℕ
hk : k ≠ 0
⊢ (fun n => 1 / ↑n ^ (2 * k)) = fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_5.h
k : ℕ
hk : k ≠ 0
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)
[PROOFSTEP]
rw [mul_zero, Real.cos_zero, mul_one]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))
[PROOFSTEP]
rw [Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
[PROOFSTEP]
have : (2 : ℝ) ^ (2 * k - 1) = (2 : ℝ) ^ (2 * k) / 2 :=
  by
  rw [eq_div_iff (two_ne_zero' ℝ)]
  conv_lhs =>
    congr
    ·skip
    ·rw [← pow_one (2 : ℝ)]
  rw [← pow_add, Nat.sub_add_cancel]
  linarith [Nat.one_le_iff_ne_zero.mpr hk]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2
[PROOFSTEP]
rw [eq_div_iff (two_ne_zero' ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) * 2 = 2 ^ (2 * k)
[PROOFSTEP]
conv_lhs =>
  congr
  ·skip
  ·rw [← pow_one (2 : ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1) * 2
[PROOFSTEP]
  congr
  ·skip
  ·rw [← pow_one (2 : ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1) * 2
[PROOFSTEP]
  congr
  ·skip
  ·rw [← pow_one (2 : ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1) * 2
[PROOFSTEP]
congr
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)
case a k : ℕ hk : k ≠ 0 | 2
[PROOFSTEP]
·skip
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)
[PROOFSTEP]
skip
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)
[PROOFSTEP]
skip
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)
[PROOFSTEP]
skip
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2
[PROOFSTEP]
·rw [← pow_one (2 : ℝ)]
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2
[PROOFSTEP]
rw [← pow_one (2 : ℝ)]
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2
[PROOFSTEP]
rw [← pow_one (2 : ℝ)]
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2
[PROOFSTEP]
rw [← pow_one (2 : ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) * 2 ^ 1 = 2 ^ (2 * k)
[PROOFSTEP]
rw [← pow_add, Nat.sub_add_cancel]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ 1 ≤ 2 * k
[PROOFSTEP]
linarith [Nat.one_le_iff_ne_zero.mpr hk]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
this : 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
[PROOFSTEP]
rw [this, mul_pow]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
this : 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2
⊢ (-1) ^ (k + 1) * (2 ^ (2 * k) / 2) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 ^ (2 * k) * π ^ (2 * k)) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
[PROOFSTEP]
ring
[GOAL]
⊢ HasSum (fun n => 1 / ↑n ^ 2) (π ^ 2 / 6)
[PROOFSTEP]
convert hasSum_zeta_nat one_ne_zero using 1
[GOAL]
case h.e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 * 1 - 1) * π ^ (2 * 1) * ↑(bernoulli (2 * 1)) / ↑(2 * 1)!
[PROOFSTEP]
rw [mul_one]
[GOAL]
case h.e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(bernoulli 2) / ↑2!
[PROOFSTEP]
rw [bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two]
[GOAL]
⊢ 2 ≠ 1
[PROOFSTEP]
decide
[GOAL]
case h.e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(1 / 6) / ↑2!
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_6
⊢ π ^ 2 / 6 = 2 * π ^ 2 * (1 / 6) / 2
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_6
⊢ π ^ 2 * (6 * 2) = 2 * π ^ 2 * 6
[PROOFSTEP]
ring
[GOAL]
⊢ HasSum (fun n => 1 / ↑n ^ 4) (π ^ 4 / 90)
[PROOFSTEP]
convert hasSum_zeta_nat two_ne_zero using 1
[GOAL]
case h.e'_6
⊢ π ^ 4 / 90 = (-1) ^ (2 + 1) * 2 ^ (2 * 2 - 1) * π ^ (2 * 2) * ↑(bernoulli (2 * 2)) / ↑(2 * 2)!
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_6
⊢ π ^ 4 / 90 = -(8 * π ^ 4 * ↑(bernoulli 4)) / 24
[PROOFSTEP]
rw [bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_four]
[GOAL]
case h.e'_6
⊢ π ^ 4 / 90 = -(8 * π ^ 4 * ↑(-1 / 30)) / 24
case h.e'_6 ⊢ 4 ≠ 1
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_6
⊢ π ^ 4 / 90 = 8 * π ^ 4 * (1 / 30) / 24
case h.e'_6 ⊢ 4 ≠ 1
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_6
⊢ π ^ 4 * (30 * 24) = 8 * π ^ 4 * 90
case h.e'_6 ⊢ 4 ≠ 1
[PROOFSTEP]
ring
[GOAL]
case h.e'_6
⊢ 4 ≠ 1
[PROOFSTEP]
decide
[GOAL]
⊢ eval (1 / 4) (bernoulli 3) = 3 / 64
[PROOFSTEP]
simp_rw [Polynomial.bernoulli, Finset.sum_range_succ, Polynomial.eval_add, Polynomial.eval_monomial]
[GOAL]
⊢ eval (1 / 4) (Finset.sum (Finset.range 0) fun x => ↑(monomial (3 - x)) (_root_.bernoulli x * ↑(Nat.choose 3 x))) +
            _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) +
          _root_.bernoulli 1 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
[PROOFSTEP]
rw [Finset.sum_range_zero, Polynomial.eval_zero, zero_add, bernoulli_one]
[GOAL]
⊢ _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
[PROOFSTEP]
rw [bernoulli_eq_bernoulli'_of_ne_one zero_ne_one, bernoulli'_zero,
  bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two,
  bernoulli_eq_bernoulli'_of_ne_one (by decide : 3 ≠ 1), bernoulli'_three]
[GOAL]
⊢ 2 ≠ 1
[PROOFSTEP]
decide
[GOAL]
⊢ 3 ≠ 1
[PROOFSTEP]
decide
[GOAL]
⊢ 1 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        1 / 6 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      0 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
[PROOFSTEP]
norm_num
[GOAL]
⊢ HasSum (fun n => 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)) (π ^ 3 / 32)
[PROOFSTEP]
apply (congr_arg₂ HasSum ?_ ?_).to_iff.mp <| hasSum_one_div_nat_pow_mul_sin one_ne_zero (?_ : 1 / 4 ∈ Icc (0 : ℝ) 1)
[GOAL]
⊢ (fun n => 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4))) = fun n => 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)
[PROOFSTEP]
ext1 n
[GOAL]
case h
n : ℕ
⊢ 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4)) = 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)
[PROOFSTEP]
norm_num
[GOAL]
case h
n : ℕ
⊢ Real.sin (2 * π * ↑n * (1 / 4)) = Real.sin (π * ↑n / 2) ∨ n = 0
[PROOFSTEP]
left
[GOAL]
case h.h
n : ℕ
⊢ Real.sin (2 * π * ↑n * (1 / 4)) = Real.sin (π * ↑n / 2)
[PROOFSTEP]
congr 1
[GOAL]
case h.h.e_x
n : ℕ
⊢ 2 * π * ↑n * (1 / 4) = π * ↑n / 2
[PROOFSTEP]
ring
[GOAL]
⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32
[PROOFSTEP]
have : (1 / 4 : ℝ) = (algebraMap ℚ ℝ) (1 / 4 : ℚ) := by norm_num
[GOAL]
⊢ 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
[PROOFSTEP]
norm_num
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32
[PROOFSTEP]
rw [this, mul_pow, Polynomial.eval_map, Polynomial.eval₂_at_apply, (by decide : 2 * 1 + 1 = 3),
  Polynomial.bernoulli_three_eval_one_quarter]
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ 2 * 1 + 1 = 3
[PROOFSTEP]
decide
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 ^ 3 * π ^ 3) / 2 / ↑3! * ↑(algebraMap ℚ ℝ) (3 / 64) = π ^ 3 / 32
[PROOFSTEP]
norm_num
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ 8 * π ^ 3 / 2 / 6 * (3 / 64) = π ^ 3 / 32
[PROOFSTEP]
field_simp
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ 8 * π ^ 3 * 3 * 32 = π ^ 3 * (2 * 6 * 64)
[PROOFSTEP]
ring
[GOAL]
⊢ 1 / 4 ∈ Icc 0 1
[PROOFSTEP]
rw [mem_Icc]
[GOAL]
⊢ 0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case left
⊢ 0 ≤ 1 / 4
case right ⊢ 1 / 4 ≤ 1
[PROOFSTEP]
linarith
[GOAL]
case right
⊢ 1 / 4 ≤ 1
[PROOFSTEP]
linarith
