theorem FunctionalEquation.jacobiTheta_modular_S_transform (τ : UpperHalfPlane) : jacobiTheta ↑(ModularGroup.S • τ) = (-Complex.I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ

@[reducible, inline]

noncomputable abbrev FunctionalEquation.completedZeta (s : ℂ) : ℂ

@[reducible, inline]

noncomputable abbrev FunctionalEquation.completedZeta₀ (s : ℂ) : ℂ

theorem FunctionalEquation.gamma_ne_zero {s : ℂ} (hs : ∀ (m : ℕ), s ≠ -↑m) : Complex.Gamma s ≠ 0

noncomputable def FunctionalEquation.xi (s : ℂ) : ℂ

theorem FunctionalEquation.xi_differentiable : Differentiable ℂ xi

theorem FunctionalEquation.xi_eq_mul_completedZeta {s : ℂ} (hs0 : s ≠ 0) (hs1 : s ≠ 1) : xi s = s * (s - 1) / 2 * completedRiemannZeta s

theorem FunctionalEquation.xi_functional_equation (s : ℂ) : xi (1 - s) = xi s

theorem FunctionalEquation.completedRiemannZeta_ne_zero_of_one_le_re {s : ℂ} (hs_re : 1 ≤ s.re) (hs0 : s ≠ 0) : completedRiemannZeta s ≠ 0

theorem FunctionalEquation.completedRiemannZeta_zero_re_in_critical_strip (s : ℂ) (hs : completedRiemannZeta s = 0) (hs0 : s ≠ 0) (hs1 : s ≠ 1) : 0 < s.re ∧ s.re < 1

theorem FunctionalEquation.xi_zero_re_in_critical_strip (s : ℂ) (hs : xi s = 0) : 0 < s.re ∧ s.re < 1

theorem FunctionalEquation.xi_entire_functional_equation_and_critical_strip : Differentiable ℂ xi ∧ (∀ (s : ℂ), xi (1 - s) = xi s) ∧ ∀ (s : ℂ), xi s = 0 → 0 < s.re ∧ s.re < 1