pith. machine review for the scientific record. sign in
theorem proved term proof

completedRiemannZeta0_hadamard_product

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  85theorem completedRiemannZeta0_hadamard_product
  86    (data : CompletedZetaHadamardProduct) (s : ℂ) :
  87    completedRiemannZeta₀ s =
  88      Complex.exp (data.A + data.B * s) * data.productLimit s :=

proof body

Term-mode proof.

  89  data.completedZeta0_eq_hadamard s
  90
  91/-! ## 4. Track D attack surface -/
  92
  93/-- Practical Track D bundle: the proved Mathlib inputs plus the open Hadamard
  94product data type. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.