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)
85theorem eigenvalue_pos {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
86 0 < (p : ℝ) ^ (-σ) := by
proof body
Term-mode proof.
87 exact Real.rpow_pos_of_pos (by exact_mod_cast p.prop.pos) _
88
89/-! ### §2. The regularized Fredholm determinant -/
90
91/-- The per-prime factor of det₂:
92 det₂_factor(p, s) = (1 − p^{−s}) · exp(p^{−s}).
93 This is entire in s. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (10)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
Primes
in IndisputableMonolith.NumberTheory.EulerInstantiation
decl_use