185structure TraceClassHeatKernel (lamP : Nat.Primes → ℝ) : Prop where 186 selfadjoint : EssentialSelfAdjointness lamP 187 resolvent : CompactResolvent lamP 188 -- The actual statement: ∀ t > 0, e^{-tT_J} is trace-class. 189 -- Stated as a Prop awaiting the analytic discharge. 190 trace_class_holds : True 191 192/-! ## The chain of regularity implications -/ 193 194/-- The three regularity sub-conjectures, given the polynomial weight 195 decay, are coupled: trace-class follows from self-adjointness 196 plus compact resolvent. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.