-- Mathlib/NumberTheory/LSeries/ZMod.lean
/--
First form of functional equation for completed L-functions (even case).

Private because it is superseded by `completedLFunction_one_sub_even` below, which is valid for a
much wider range of `s`.
-/
private lemma completedLFunction_one_sub_of_one_lt_even (hΦ : Φ.Even) {s : ℂ} (hs : 1 < re s) :
    completedLFunction Φ (1 - s) = N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ ∑ x : ZMod N, Φ x * cosZeta (toAddCircle x) s = LFunction (𝓕 Φ) s

Tactic:
simp only [cosZeta_eq, ← mul_div_assoc _ _ (2 : ℂ), mul_add, ← sum_div, sum_add_distrib,
  LFunction_dft Φ (.inr hs₁), map_neg, div_eq_iff (two_ne_zero' ℂ), mul_two, add_left_inj]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ ∑ x : ZMod N, Φ x * expZeta (toAddCircle x) s = ∑ x : ZMod N, Φ x * expZeta (-toAddCircle x) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
this : ∑ x : ZMod N, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
simp only [completedLFunction_def_even hΦ, neg_sub, completedHurwitzZetaEven_one_sub, this]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ ∑ x : ZMod N, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s

Tactic:
suffices ∑ x, Φ x * cosZeta (toAddCircle x) s = LFunction (𝓕 Φ) s by
  simpa only [cosZeta, Function.update_of_ne hs₀, ← mul_div_assoc, ← sum_div,
    LFunction_eq_completed_div_gammaFactor_even (dft_even_iff.mpr hΦ) _ (.inl hs₀),
    div_left_inj' (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ ∑ x : ZMod N, Φ x * cosZeta (toAddCircle x) s = LFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
suffices ∑ x, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s by
  simp only [completedLFunction_def_even hΦ, neg_sub, completedHurwitzZetaEven_one_sub, this]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ ∑ x : ZMod N, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ ∀ (x : ZMod N),
    Φ x * expZeta (toAddCircle x) s = Φ ((Equiv.neg (ZMod N)) x) * expZeta (-toAddCircle ((Equiv.neg (ZMod N)) x)) s

Tactic:
simp [hΦ _]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
this : ∑ x : ZMod N, Φ x * cosZeta (toAddCircle x) s = LFunction (𝓕 Φ) s
⊢ ∑ x : ZMod N, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s

Tactic:
simpa only [cosZeta, Function.update_of_ne hs₀, ← mul_div_assoc, ← sum_div,
  LFunction_eq_completed_div_gammaFactor_even (dft_even_iff.mpr hΦ) _ (.inl hs₀),
  div_left_inj' (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
have hs₀ : s ≠ 0 := ne_zero_of_one_lt_re hs

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ ∑ x : ZMod N, Φ x * expZeta (toAddCircle x) s = ∑ x : ZMod N, Φ x * expZeta (-toAddCircle x) s

Tactic:
exact Fintype.sum_equiv (.neg _) _ _ (by simp [hΦ _])

Result:
no goals