mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt (f (k + 1)) (↑m * (↑k + 1) * f k x) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ sinZeta (↑x) (2 * ↑k + 1) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 2 * ↑k = ↑(2 * k - 1) + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 ≤ 2 * k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
⊢ Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
    Φ j *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ k + 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ cosZeta (↑x) (2 * ↑k) =
    (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ normalizedFactors (Ideal.map (algebraMap R S) I) =
    Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ Complex.Gamma (2 * ↑k + 1) = Complex.Gamma (↑(2 * k) + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ Φ 0 = 0 → Φ (-0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
k✝ : ℕ
a✝ : k✝ < m
⊢ Continuous (bernoulliFun (k + 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
i✝ : ℕ
a✝ : i✝ ∈ Finset.range m
⊢ Continuous fun x ↦ bernoulliFun (k + 1) (x + ↑i✝ / ↑m)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ 2 * ↑k + 1 = ↑(2 * k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ sinZeta (↑x) (2 * ↑k + 1) =
    (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ {a | (Equiv.neg (ZMod N)) a ≠ a} ⊆ ↑Finset.univ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ 2 * ↑k ≠ -↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
⊢ 2 * ↑k ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
⊢ (2 * ↑k).Gammaℂ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ Continuous fun x ↦ bernoulliFun (k + 1) (↑m * x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
this : ∃ y, normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
⊢ Irreducible (Ideal.map (algebraMap R S) I)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ Continuous fun x ↦ ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ∫ (x : ℝ) in 0..(↑m)⁻¹, f (k + 1) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZetaEven (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ 2 * ↑k + 1 ≠ -↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
⊢ (2 * ↑k + 1).Gammaℂ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k m : ℕ
m0 : m ≠ 0
x : ℝ
⊢ bernoulliFun k (↑m * x) = ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ -(2 * ↑k) = 1 - (2 * ↑k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ bernoulliFun (2 * k + 1) 2⁻¹ = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ Irreducible (Ideal.map (algebraMap R S) I)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
k1 : ¬k = 1
m : ↑(bernoulli k) = 2 ^ k / 2 * (bernoulliFun k (1 / 2) + ↑(bernoulli k))
⊢ 2 ^ k / 2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
⊢ LFunction Φ (1 - s) =
    ↑N ^ (s - 1) * (2 * ↑π) ^ (-s) * Gamma s *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ LFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * hurwitzZetaEven (toAddCircle j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ LFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * hurwitzZetaOdd (toAddCircle j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
⊢ LFunction Φ 0 = -Φ 0 / 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZetaOdd (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
n : ℕ
⊢ LFunction Φ (-(2 * (↑n + 1))) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
n : ℕ
⊢ LFunction Φ (-(2 * ↑n) - 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
s : ℂ
⊢ completedLFunction 0 s = 0

Tactic:
simp only [completedLFunction, Pi.zero_apply, zero_mul, sum_const_zero, mul_zero, zero_add]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
s : ℂ
⊢ completedLFunction 0 s = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0
⊢ hurwitzZeta (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZeta (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
⊢ completedLFunction (fun j ↦ a * Φ j) s = a * completedLFunction Φ s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 0 n = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0
⊢ hurwitzZeta (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZeta (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n ≠ 0
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n + 1 ≠ 0
⊢ n + 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ ¬k + 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZeta (↑x) (-↑k) =
    -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: Φ : ZMod 1 → ℂ
s : ℂ
⊢ completedLFunction Φ s = Φ 1 * completedRiemannZeta s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ fun s ↦ ↑N ^ (-s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ 1 < 2 * k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ (completedLFunction₀ Φ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ (completedLFunction₀ Φ)

Tactic:
by
  refine .add ?_ ?_ <;>
  refine .mul (by fun_prop) (.fun_sum fun i _ ↦ .const_mul ?_ _)
  exacts [differentiable_completedHurwitzZetaEven₀ _, differentiable_completedHurwitzZetaOdd _]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
⊢ completedLFunction Φ s = completedLFunction₀ Φ s - ↑N ^ (-s) * Φ 0 / s - (↑N ^ (-s) * ∑ j, Φ j) / (1 - s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
n : ℤ
⊢ bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun x ↦ ↑N ^ (-x)) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
n : ℤ
⊢ ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ riemannZeta (2 * ↑k) = (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : Φ 0 = 0
⊢ DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
n : ℤ
⊢ fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
⊢ ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : s ≠ 1
⊢ DifferentiableAt ℂ (fun x ↦ ∑ j, Φ j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
⊢ riemannZeta (2 * ↑k) = (-1) ^ (k + 1) * 2 ^ (2 * ↑k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : s ≠ 1
⊢ DifferentiableAt ℂ (HSub.hSub 1) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: 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|

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: ⊢ riemannZeta 2 = ↑π ^ 2 / 6

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : s ≠ 1
⊢ 1 - s ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: ⊢ 1 < 4

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
⊢ Summable fun n ↦ -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: ⊢ riemannZeta 4 = ↑π ^ 4 / 90

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun x ↦ (∑ j, Φ j) / (1 - x)) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (completedLFunction Φ) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
        ⟨Polynomial.map (Ideal.Quotient.mk I) Q, hQ⟩) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ k + 1 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
⊢ riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
⊢ term (f + g) s = term f s + term g s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f + g) s n = term f s n + term g s n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f + g) s (a + b)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeriesSummable (f + g) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeries (f + g) s = LSeries f s + LSeries g s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
⊢ term (-f) s = -term f s

Tactic:
by

Goal state after: