`cost_operator_regularity_certificate`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.CostOperatorRegularity
domain: NumberTheory
line: 206 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.CostOperatorRegularity on GitHub at line 206.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 203/-! ## Master certificate -/
 204
 205/-- The structural facts established in this module. -/
 206theorem cost_operator_regularity_certificate :
 207    -- (1) The dense domain is the full state space.
 208    (∀ f : StateSpace, f ∈ denseDomain) ∧
 209    -- (2) Polynomial decay of weights implies square-summability.
 210    (∀ {lamP : Nat.Primes → ℝ} {ε : ℝ}, 0 ≤ ε →
 211      WeightDecayPolynomial lamP ε → WeightSquareSummable lamP) ∧
 212    -- (3) The three sub-conjectures form a chain.
 213    (∀ {lamP : Nat.Primes → ℝ},
 214      EssentialSelfAdjointness lamP →
 215      CompactResolvent lamP →
 216      TraceClassHeatKernel lamP) :=
 217  ⟨denseDomain_mem,
 218   @weight_polynomial_decay_summable,
 219   @regularity_chain⟩
 220
 221end
 222
 223end CostOperatorRegularity
 224end NumberTheory
 225end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.