-- Mathlib/NumberTheory/LSeries/ZMod.lean
/-- For `1 < re s` the congruence L-function agrees with the sum of the Dirichlet series. -/
lemma LFunction_eq_LSeries (Φ : ZMod N → ℂ) {s : ℂ} (hs : 1 < re s) :
    LFunction Φ s = LSeries (Φ ·) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j * (1 / ↑↑N ^ s * (1 / ↑((↑j.val + ↑N * ↑m) / ↑N) ^ s)) = Φ j / (↑↑N * ↑((↑j.val + ↑N * ↑m) / ↑N)) ^ s

Tactic:
rw [one_div_mul_one_div, mul_one_div, mul_cpow_ofReal_nonneg] <;> positivity

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
⊢ ∑ i : ZMod N, ↑N ^ (-s) * (Φ i * hurwitzZeta (toAddCircle i) s) =
    ∑ j : ZMod N, ∑' (m : ℕ), LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Tactic:
congr 1 with j

Result:
case e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
⊢ ↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s) = ∑' (m : ℕ), LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Proof state:
case e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
⊢ ↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s) = ∑' (m : ℕ), LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Tactic:
have : (j.val / N : ℝ) ∈ Set.Icc 0 1 := mem_Icc.mpr ⟨by positivity,
  (div_le_one (Nat.cast_pos.mpr <| NeZero.pos _)).mpr <| Nat.cast_le.mpr (val_lt j).le⟩

Result:
case e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
⊢ ↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s) = ∑' (m : ℕ), LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ ↑(j.val + N * m) / ↑(j.val + N * m) ^ s = LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Tactic:
rw [LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs)]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑↑N * ↑((↑j.val + ↑N * ↑m) / ↑N)) ^ s = Φ j / (↑N * (↑j.val + ↑N * ↑m) / ↑N) ^ s

Tactic:
simp only [ofReal_natCast, ofReal_div, ofReal_add, ofReal_mul, mul_div_assoc]

Result:
no goals

Proof state:
case e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
⊢ ∑' (x : ℕ), ↑N ^ (-s) * Φ j * (1 / (↑x + ↑(↑j.val / ↑N)) ^ s) =
    ∑' (m : ℕ), LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Tactic:
congr 1 with m

Result:
case e_f.h.e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ ↑N ^ (-s) * Φ j * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s) = LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j * (↑N ^ (-s) * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s)) = Φ j * (1 / ↑↑N ^ s * (1 / ↑((↑j.val + ↑N * ↑m) / ↑N) ^ s))

Tactic:
simp only [cpow_neg, ← one_div, ofReal_div, ofReal_natCast, add_comm, add_div, ofReal_add,
  ofReal_mul, mul_div_cancel_left₀ (m : ℂ) (Nat.cast_ne_zero.mpr (NeZero.ne N))]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
⊢ LFunction Φ s = LSeries (fun x => Φ ↑x) s

Tactic:
rw [LFunction, LSeries, mul_sum, Nat.sumByResidueClasses (LSeriesSummable_of_one_lt_re Φ hs) N]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
⊢ ∑ i : ZMod N, ↑N ^ (-s) * (Φ i * hurwitzZeta (toAddCircle i) s) =
    ∑ j : ZMod N, ∑' (m : ℕ), LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Proof state:
case e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
⊢ ↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s) = ∑' (m : ℕ), LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Tactic:
rw [toAddCircle_apply, ← (hasSum_hurwitzZeta_of_one_lt_re this hs).tsum_eq, ← mul_assoc,
  ← tsum_mul_left]

Result:
case e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
⊢ ∑' (x : ℕ), ↑N ^ (-s) * Φ j * (1 / (↑x + ↑(↑j.val / ↑N)) ^ s) =
    ∑' (m : ℕ), LSeries.term (fun x => Φ ↑x) s (j.val + N * m)

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ ↑N ^ (-s) * Φ j * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s) = Φ j * (↑N ^ (-s) * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s))

Tactic:
rw [← mul_assoc, mul_comm _ (Φ _)]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑j.val + ↑N * ↑m) ^ s = Φ ↑(j.val + N * m) / ↑(j.val + N * m) ^ s

Tactic:
simp only [Nat.cast_add, Nat.cast_mul, natCast_zmod_val, natCast_self, zero_mul, add_zero]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
⊢ 0 ≤ ↑j.val / ↑N

Tactic:
positivity

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑N * (↑j.val + ↑N * ↑m) / ↑N) ^ s = Φ j / (↑j.val + ↑N * ↑m) ^ s

Tactic:
rw [mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr (NeZero.ne N))]

Result:
no goals