def definition def or abbrev

`det2Factor`

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

formal statement (Lean)

  94noncomputable def det2Factor (p : ℕ) (σ : ℝ) : ℝ :=

proof body

Definition body.

  95  (1 - (p : ℝ) ^ (-σ)) * Real.exp ((p : ℝ) ^ (-σ))
  96
  97/-- The log of the per-prime factor:
  98    log det₂_factor = log(1 − p^{−σ}) + p^{−σ}.
  99    For |z| < 1: log(1−z) + z = −∑_{m≥2} z^m/m,
 100    so |log det₂_factor| ≤ p^{−2σ}/(1 − p^{−σ}). -/

depends on (5)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use