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

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

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ ∑ x : ZMod N, Φ x * sinZeta (toAddCircle x) s =
    (∑ x : ZMod N, Φ x * expZeta (toAddCircle x) s) / (2 * I) -
      (∑ x : ZMod N, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I)

Tactic:
simp only [sinZeta_eq, ← mul_div_assoc, mul_sub, sub_div, sum_sub_distrib, sum_div, map_neg]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x : ZMod N, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s
⊢ 0 < (s + 1).re

Tactic:
simp only [add_re, one_re]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x : ZMod N, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s
⊢ 0 < s.re + 1

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

Tactic:
suffices ∑ x, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s by
  simp only [completedLFunction_def_odd hΦ, neg_sub, completedHurwitzZetaOdd_one_sub, this,
    mul_assoc]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ ∑ x : ZMod N, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ -I⁻¹ * LFunction (𝓕 Φ) s = I * LFunction (𝓕 Φ) s

Tactic:
rw [inv_I, neg_neg]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x : ZMod N, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s
⊢ ∑ x : ZMod N, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s

Tactic:
have hs' : 0 < re (s + 1) := by simp only [add_re, one_re]; linarith

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x : ZMod N, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s
hs' : 0 < (s + 1).re
⊢ ∑ x : ZMod N, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s

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

Tactic:
exact (Fintype.sum_equiv (.neg _) _ _ fun x ↦ by rfl).symm

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (-∑ x : ZMod N, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) -
      (∑ x : ZMod N, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    -(I⁻¹ * ∑ x : ZMod N, Φ x * expZeta (toAddCircle (-x)) s)

Tactic:
ring

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
x : ZMod N
⊢ Φ (-x) * expZeta (toAddCircle (-x)) s = Φ ((Equiv.neg (ZMod N)) x) * expZeta (toAddCircle ((Equiv.neg (ZMod N)) x)) s

Tactic:
rfl

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x : ZMod N, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s
⊢ 0 < s.re + 1

Tactic:
linarith

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (∑ x : ZMod N, Φ (-x) * expZeta (toAddCircle (-x)) s) / (2 * I) -
      (∑ x : ZMod N, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    -I⁻¹ * LFunction (𝓕 Φ) s

Tactic:
simp only [hΦ _, neg_mul, sum_neg_distrib, LFunction_dft Φ (.inl hΦ.map_zero)]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (-∑ x : ZMod N, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) -
      (∑ x : ZMod N, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    -(I⁻¹ * ∑ x : ZMod N, Φ x * expZeta (toAddCircle (-x)) s)

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ ∑ x : ZMod N, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s

Tactic:
suffices ∑ x, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s by
  have hs' : 0 < re (s + 1) := by simp only [add_re, one_re]; linarith
  simpa only [sinZeta, ← mul_div_assoc, ← sum_div, div_left_inj' (Gammaℝ_ne_zero_of_re_pos hs'),
    LFunction_eq_completed_div_gammaFactor_odd (dft_odd_iff.mpr hΦ)]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ ∑ x : ZMod N, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ ∑ x : ZMod N, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s

Tactic:
calc ∑ x, Φ x * sinZeta (toAddCircle x) s
_ = (∑ x, Φ x * expZeta (toAddCircle x) s) / (2 * I)
    - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) := by
  simp only [sinZeta_eq, ← mul_div_assoc, mul_sub, sub_div, sum_sub_distrib, sum_div, map_neg]
_ = (∑ x, Φ (-x) * expZeta (toAddCircle (-x)) s) / (_) - (_) := by
  congrm ?_ / _ - _
  exact (Fintype.sum_equiv (.neg _) _ _ fun x ↦ by rfl).symm
_ = -I⁻¹ * LFunction (𝓕 Φ) s := by
  simp only [hΦ _, neg_mul, sum_neg_distrib, LFunction_dft Φ (.inl hΦ.map_zero)]
  ring
_ = I * LFunction (𝓕 Φ) s := by rw [inv_I, neg_neg]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x : ZMod N, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
simp only [completedLFunction_def_odd hΦ, neg_sub, completedHurwitzZetaOdd_one_sub, this,
  mul_assoc]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (∑ x : ZMod N, Φ x * expZeta (toAddCircle x) s) / (2 * I) -
      (∑ x : ZMod N, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    (∑ x : ZMod N, Φ (-x) * expZeta (toAddCircle (-x)) s) / ?m.233669 - ?m.233672

Tactic:
congrm ?_ / _ - _

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ ∑ 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.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x : ZMod N, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s
hs' : 0 < (s + 1).re
⊢ ∑ x : ZMod N, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s

Tactic:
simpa only [sinZeta, ← mul_div_assoc, ← sum_div, div_left_inj' (Gammaℝ_ne_zero_of_re_pos hs'),
  LFunction_eq_completed_div_gammaFactor_odd (dft_odd_iff.mpr hΦ)]

Result:
no goals