awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
inl : bernoulliFourierCoeff k 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
inr : ∀ (hn : n ≠ 0), bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
⊢ bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
inl : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
inl₁ : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * 0) ^ k
inl₂ : 0 = -(↑k ! : ℂ) / HPow.hPow (α := ℂ) 0 k
inl₃ : 0 = HDiv.hDiv (α := ℂ) (-(↑k ! : ℂ)) 0
inl₄ inl₅ : Eq (α := ℂ) 0 0
⊢ bernoulliFourierCoeff k 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k

Tactic:
rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow hk,
      div_zero]

Premises used: bernoulliFourierCoeff_zero, Int.cast_zero, MulZeroClass.mul_zero, div_zero, zero_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k

Tactic:
Nat.le_induction ?_ (fun k hk h'k => ?_) k (Nat.one_le_iff_ne_zero.mpr hk)

Premises used: Iff.mpr, Nat.le_induction, Nat.one_le_iff_ne_zero
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
inr : bernoulliFourierCoeff 1 n = -(↑1! : ℂ) / HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1
inr₁ :
  ∀ (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)
⊢ bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k

Tactic:
refine Nat.le_induction ?_ (fun k hk h'k => ?_) k (Nat.one_le_iff_ne_zero.mpr hk)
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
inr :
  1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if Eq (α := ℕ) 1 1 then 1 else 0) - (↑1 : ℂ) * bernoulliFourierCoeff (HSub.hSub (α := ℕ) 1 1) n) =
    -(↑1! : ℂ) / HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1
⊢ bernoulliFourierCoeff 1 n = -(↑1! : ℂ) / HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1

Tactic:
rw [bernoulliFourierCoeff_recurrence 1 hn]

Premises used: bernoulliFourierCoeff_recurrence, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
inr : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
⊢ 1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if Eq (α := ℕ) 1 1 then 1 else 0) - (↑1 : ℂ) * bernoulliFourierCoeff (HSub.hSub (α := ℕ) 1 1) n) =
    -(↑1! : ℂ) / HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1

Tactic:
simp only [Nat.cast_one, tsub_self, neg_mul, one_mul, if_true,
      Nat.factorial_one, pow_one]

Premises used: if_true, tsub_self, pow_one, neg_mul, Nat.cast_one, one_mul, Nat.factorial_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
inr : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * HSub.hSub (α := ℂ) 1 0 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₁ : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * 1 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₂ : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₃ : -(1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₄ inr₅ : -(1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))) = -(1 / (2 * (↑π : ℂ) * I * (↑n : ℂ)))
⊢ 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))

Tactic:
rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]

Premises used: neg_div, sub_zero, bernoulli_zero_fourier_coeff, div_neg, mul_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k_1 : ℕ
hk_1 : k_1 ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
⊢ ¬k + 1 = 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k_1 : ℕ
hk_1 : k_1 ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
inr :
  1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) * -((↑(k + 1) : ℂ) * (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k)) =
    -HMul.hMul (α := ℂ) (↑(k + 1) : ℂ) (↑k ! : ℂ) /
      ((2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1)
⊢ bernoulliFourierCoeff (k + 1) n = -(↑(k + 1)! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ (k + 1)

Tactic:
rw [bernoulliFourierCoeff_recurrence (k + 1) hn, if_neg (by grind), Nat.add_sub_cancel k 1, h'k,
      Nat.factorial_succ, zero_sub, Nat.cast_mul, pow_add]

Premises used: Nat.factorial_succ, pow_add, Nat.cast_mul, HAdd.hAdd, Nat.add_sub_cancel, bernoulliFourierCoeff_recurrence, OfNat.ofNat, if_neg, zero_sub
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k_1 : ℕ
hk_1 : k_1 ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
⊢ 1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) * -((↑(k + 1) : ℂ) * (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k)) =
    -HMul.hMul (α := ℂ) (↑(k + 1) : ℂ) (↑k ! : ℂ) /
      ((2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 1
⊢ Continuous (periodizedBernoulli k)

Tactic:
AddCircle.liftIco_zero_continuous
    (mod_cast (bernoulliFun_endpoints_eq_of_ne_one hk).symm)
    (Polynomial.continuous _).continuousOn

Premises used: Polynomial.continuous, Continuous.continuousOn, congrArg, cast, bernoulliFun_endpoints_eq_of_ne_one, bernoulliFun, periodizedBernoulli, congr, Nat.cast_zero, AddCircle.liftIco_zero_continuous, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
h : ∀ (x : 𝕌), (ofReal ∘ periodizedBernoulli k) x = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k) x
⊢ ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)

Tactic:
ext1 x
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
x : 𝕌
⊢ (ofReal ∘ periodizedBernoulli k) x = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k) x

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)

Tactic:
have : ((↑) ∘ periodizedBernoulli k : 𝕌 → ℂ) = AddCircle.liftIco 1 0 ((↑) ∘ bernoulliFun k) := by
    ext1 x; rfl
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
rw :
  fourierCoeffOn (a := 0) (b := HAdd.hAdd (α := ℝ) 0 1) ⋯ (ofReal ∘ bernoulliFun k) n =
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
⊢ fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k

Tactic:
rw [this, fourierCoeff_liftIco_eq]

Premises used: fourierCoeff_liftIco_eq
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
⊢ fourierCoeffOn (a := 0) (b := HAdd.hAdd (α := ℝ) 0 1) ⋯ (ofReal ∘ bernoulliFun k) n =
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k

Tactic:
simpa only [zero_add] using bernoulliFourierCoeff_eq hk n

Premises used: zero_add, bernoulliFourierCoeff_eq
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
n : ℤ
rw :
  -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k / HPow.hPow (α := ℂ) (↑n : ℂ) k
rw₁ :
  -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
    -(↑k ! : ℂ) / ((2 * (↑π : ℂ) * I) ^ k * HPow.hPow (α := ℂ) (↑n : ℂ) k)
rw₂ rw₃ : -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
⊢ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)

Tactic:
rw [mul_one_div, div_div, ← mul_pow]

Premises used: mul_one_div, div_div, mul_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
⊢ ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)

Tactic:
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]
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
this :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
simp_rw : Summable (α := ℂ) fun (n : ℤ) ↦ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k

Tactic:
simp_rw [this]
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
this :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)

Tactic:
Summable.mul_left _ <| .of_norm ?_

Premises used: Summable.of_norm, Summable.mul_left
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
this :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
refine : Summable (α := ℝ) fun (a : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑a : ℂ) k‖
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)

Tactic:
refine Summable.mul_left _ <| .of_norm ?_

Premises used: Summable.mul_left
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
this :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
h : ∀ (x : ℤ), ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖ = |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
⊢ Eq (α := (x : ℤ) → ℝ) (fun (x : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖) fun (x : ℤ) ↦
    |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|

Tactic:
ext1 x
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
this :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
x : ℤ
⊢ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖ = |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|

Tactic:
simp only [one_div, norm_inv, norm_pow, norm_intCast, pow_abs, abs_inv]

Premises used: norm_pow, abs_inv, norm_inv, one_div, pow_abs, Complex.norm_intCast
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
this :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
⊢ Eq (α := (x : ℤ) → ℝ) (fun (x : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖) fun (x : ℤ) ↦
    |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|

Tactic:
have : (fun x : ℤ => ‖1 / (x : ℂ) ^ k‖) = fun x : ℤ => |1 / (x : ℝ) ^ k| := by
    ext1 x
    simp only [one_div, norm_inv, norm_pow, norm_intCast, pow_abs, abs_inv]
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
this_1 :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
this :
  Eq (α := (x : ℤ) → ℝ) (fun (x : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖) fun (x : ℤ) ↦
    |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
simp_rw : Summable (α := ℝ) fun (x : ℤ) ↦ |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
⊢ Summable (α := ℝ) fun (a : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑a : ℂ) k‖

Tactic:
simp_rw [this]
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
this_1 :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
this :
  Eq (α := (x : ℤ) → ℝ) (fun (x : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖) fun (x : ℤ) ↦
    |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
rwa : Summable (α := ℝ) fun (x : ℤ) ↦ 1 / HPow.hPow (α := ℝ) (↑x : ℝ) k
rwa₁ rwa₂ rwa₃ rwa₄ : 1 < k
⊢ Summable (α := ℝ) fun (x : ℤ) ↦ |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|

Tactic:
rwa [summable_abs_iff, Real.summable_one_div_int_pow]

Premises used: Real.summable_one_div_int_pow, summable_abs_iff
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
⊢ Membership.mem (γ := Set ℝ) (Ico 0 1) x ∨ x = 1

Tactic:
rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx

Premises used: Real, zero_le_one', Set.Ico_insert_right, Set.mem_insert_iff, or_comm
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
hx₁ : Membership.mem (γ := Set ℝ) (Ico 0 1) x ∨ x = 1
⊢ ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))

Tactic:
rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx

Premises used: Real, zero_le_one', Set.Ico_insert_right, Set.mem_insert_iff, or_comm
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx_1 : Membership.mem (γ := Set ℝ) (Icc 0 1) x
hx : Membership.mem (γ := Set ℝ) (Ico 0 1) x ∨ x = 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
inl :
  ∀ (hx : Membership.mem (γ := Set ℝ) (Ico 0 1) x),
    HasSum
      (fun (n : ℤ) ↦
        HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
          ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
      (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))
inr :
  ∀ (hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1)
    (this :
      ∀ {y : ℝ},
        Membership.mem (γ := Set ℝ) (Ico 0 1) y →
          HasSum
            (fun (n : ℤ) ↦
              HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
                ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
            (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))),
    HasSum
      (fun (n : ℤ) ↦
        HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
          ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
      (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 1) : ℂ))
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))

Tactic:
rcases hx with (hx | rfl)

Premises used: rfl
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx_1 : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
hx : Membership.mem (γ := Set ℝ) (Ico 0 1) x
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))

Tactic:
this hx
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx_1 : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
hx : Membership.mem (γ := Set ℝ) (Ico 0 1) x
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))

Tactic:
exact this hx
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 0) : ℂ))

Tactic:
this (left_mem_Ico.mpr zero_lt_one)

Premises used: Iff.mpr, Set.left_mem_Ico, zero_lt_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
h :
  Eq (α := ℤ → ℂ)
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    fun (n : ℤ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
h₁ :
  -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 1) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 0) : ℂ)
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 1) : ℂ))

Tactic:
convert! this (left_mem_Ico.mpr zero_lt_one) using 1

Premises used: Iff.mpr, Set.left_mem_Ico, zero_lt_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
h :
  Eq (α := ℤ → ℂ)
    (fun (n : ℤ) ↦ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k) ((fourier n : (a : AddCircle 1) → ℂ) 0 : ℂ))
    fun (n : ℤ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
h₁ h₂ :
  Eq (α := ℤ → ℂ)
    (fun (n : ℤ) ↦ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k) ((fourier n : (a : AddCircle 1) → ℂ) 0 : ℂ))
    fun (n : ℤ) ↦ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k) ((fourier n : (a : AddCircle 1) → ℂ) 0 : ℂ)
⊢ Eq (α := ℤ → ℂ)
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    fun (n : ℤ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]

Premises used: QuotientAddGroup.mk_zero, AddCircle.coe_period
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
⊢ k ≠ 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
h h₁ :
  -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 0) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 0) : ℂ)
⊢ -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 1) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 0) : ℂ)

Tactic:
rw [bernoulliFun_endpoints_eq_of_ne_one (by lia : k ≠ 1)]

Premises used: bernoulliFun_endpoints_eq_of_ne_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
suffices :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))

Tactic:
suffices ∀ {y : ℝ}, y ∈ Ico (0 : ℝ) 1 →
      HasSum (fun (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 lia : k ≠ 1)]
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
⊢ k ≠ 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
rw : ∀ (n : ℤ), fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
⊢ ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k

Tactic:
rw [ContinuousMap.coe_mk]

Premises used: ContinuousMap.coe_mk