LogicComplexAnalyticSubstrateCert

formal source

  64
  65/-- Certificate that all analytic zeta operations are performed in Mathlib `ℂ`
  66through the recovered-complex equivalence. -/
  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. -/
  84def logicComplexAnalyticSubstrateCert : LogicComplexAnalyticSubstrateCert where
  85  carrier_equiv := equivComplex
  86  zeta_transport := fun _ => rfl
  87  completed_zeta_transport := fun _ => rfl
  88  euler_product := logicRiemannZeta_eulerProduct_tendsto
  89  completed_functional_equation := logicCompletedRiemannZeta_one_sub
  90
  91end
  92
  93end LogicComplexCompat
  94end Foundation
  95end IndisputableMonolith