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

LogicComplexAnalyticSubstrateCert

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)

  67structure LogicComplexAnalyticSubstrateCert where
  68  carrier_equiv : LogicComplex ≃ ℂ
  69  zeta_transport : ∀ s : LogicComplex,
  70    logicRiemannZeta s = riemannZeta (toComplex s)
  71  completed_zeta_transport : ∀ s : LogicComplex,
  72    logicCompletedRiemannZeta s = completedRiemannZeta (toComplex s)
  73  euler_product :
  74    ∀ s : LogicComplex, 1 < (toComplex s).re →
  75      Tendsto (fun n : ℕ ↦
  76        NumberTheory.finitePrimeLedgerPartition (toComplex s) (Nat.primesBelow n))
  77        atTop (𝓝 (logicRiemannZeta s))
  78  completed_functional_equation :
  79    ∀ s : LogicComplex,
  80      logicCompletedRiemannZeta (fromComplex (1 - toComplex s)) =
  81        logicCompletedRiemannZeta s
  82
  83/-- The analytic substrate compatibility certificate for Phase 2. -/

used by (3)

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

depends on (9)

Lean names referenced from this declaration's body.