toComplex_re_eq

formal source

  42  simp [logicCompletedRiemannZeta]
  43
  44/-- Recovered-complex real part agrees with the real part after transport. -/
  45theorem toComplex_re_eq (s : LogicComplex) :
  46    (toComplex s).re = RealsFromLogic.LogicReal.toReal s.re := rfl
  47
  48/-- The Euler product theorem, read on recovered complex inputs. -/
  49theorem logicRiemannZeta_eulerProduct_tendsto
  50    (s : LogicComplex) (hs : 1 < (toComplex s).re) :
  51    Tendsto (fun n : ℕ ↦
  52        NumberTheory.finitePrimeLedgerPartition (toComplex s) (Nat.primesBelow n))
  53      atTop (𝓝 (logicRiemannZeta s)) := by
  54  simpa [logicRiemannZeta] using
  55    NumberTheory.EulerProductEqualsZeta.ledger_partition_equals_zeta
  56      (toComplex s) hs
  57
  58/-- Completed zeta satisfies the functional equation on recovered complex
  59inputs, by transport to Mathlib's `completedRiemannZeta`. -/
  60theorem logicCompletedRiemannZeta_one_sub (s : LogicComplex) :
  61    logicCompletedRiemannZeta (fromComplex (1 - toComplex s)) =
  62      logicCompletedRiemannZeta s := by
  63  simp [logicCompletedRiemannZeta, completedRiemannZeta_one_sub]
  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 : ℕ ↦