completedZeta0_differentiable

formal source

  27/-! ## 1. Mathlib facts available for the pole-removed completed zeta -/
  28
  29/-- Completed zeta with poles removed is differentiable everywhere in Mathlib. -/
  30theorem completedZeta0_differentiable :
  31    Differentiable ℂ completedRiemannZeta₀ :=
  32  differentiable_completedZeta₀
  33
  34/-- The pole-removed completed zeta has the same functional equation. -/
  35theorem completedZeta0_functional_equation (s : ℂ) :
  36    completedRiemannZeta₀ s = completedRiemannZeta₀ (1 - s) :=
  37  (completedRiemannZeta₀_one_sub s).symm
  38
  39/-! ## 2. Genus-one Hadamard factors -/
  40
  41/-- The genus-one elementary Hadamard factor `E₁(z) = (1-z) exp(z)`. -/
  42def hadamardE1 (z : ℂ) : ℂ :=
  43  (1 - z) * Complex.exp z
  44
  45@[simp] theorem hadamardE1_zero : hadamardE1 0 = 1 := by
  46  simp [hadamardE1]
  47
  48/-- The finite genus-one product over the first `N` listed zeros. -/
  49def hadamardPartialProduct (zeros : ℕ → ℂ) (s : ℂ) (N : ℕ) : ℂ :=
  50  ∏ n ∈ Finset.range N, hadamardE1 (s / zeros n)
  51
  52@[simp] theorem hadamardPartialProduct_zero
  53    (zeros : ℕ → ℂ) (N : ℕ) :
  54    hadamardPartialProduct zeros 0 N = 1 := by
  55  simp [hadamardPartialProduct]
  56
  57/-! ## 3. Exact Hadamard product data needed downstream -/
  58
  59/-- Hadamard product data for the pole-removed completed zeta.
  60