def definition def or abbrev

`primeLog`

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

formal statement (Lean)

 342noncomputable def primeLog (p : Nat.Primes) : ℝ :=

proof body

Definition body.

 343  Real.log (p : ℝ)
 344
 345/-- The actual complex per-prime Euler eigenvalue `p^{-s}` on the strip, written
 346as an exponential so it is available uniformly on `ℂ`. -/

used by (8)

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

eulerPrimeLogDerivTermComplex in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
eulerPrimePowerComplex in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
norm_eulerPrimeLogDerivTermComplex_le in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
norm_eulerPrimePowerComplex in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
norm_eulerPrimePowerComplex_eq_rpow in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
norm_eulerPrimePowerComplex_lt_one in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
norm_form_eq_carrierDerivTerm in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use

depends on (6)

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Primes in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use