 194/-- The three regularity sub-conjectures, given the polynomial weight
 195    decay, are coupled: trace-class follows from self-adjointness
 196    plus compact resolvent. -/
 197theorem regularity_chain {lamP : Nat.Primes → ℝ}
 198    (h_self : EssentialSelfAdjointness lamP)
 199    (h_res : CompactResolvent lamP) :
 200    TraceClassHeatKernel lamP :=
 201  ⟨h_self, h_res, trivial⟩
 202
 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.