pith. machine review for the scientific record. sign in
structure definition def or abbrev

CompletedZetaHadamardProduct

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)

  66structure CompletedZetaHadamardProduct where
  67  zeros : ℕ → ℂ
  68  zero_ne_zero : ∀ n : ℕ, zeros n ≠ 0
  69  A : ℂ
  70  B : ℂ
  71  productLimit : ℂ → ℂ
  72  partial_products_converge :
  73    ∀ s : ℂ,
  74      Filter.Tendsto
  75        (fun N : ℕ => hadamardPartialProduct zeros s N)
  76        Filter.atTop
  77        (nhds (productLimit s))
  78  completedZeta0_eq_hadamard :
  79    ∀ s : ℂ,
  80      completedRiemannZeta₀ s =
  81        Complex.exp (A + B * s) * productLimit s
  82
  83/-- Once Hadamard product data is supplied, the pole-removed completed zeta has
  84the expected genus-one factorization. -/

used by (2)

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

depends on (14)

Lean names referenced from this declaration's body.