EssentialSelfAdjointness

formal source

 165/-- Sub-conjecture C.1: essential self-adjointness of the cost
 166    operator on the dense domain `denseDomain`, given the bandwidth
 167    constraint. -/
 168structure EssentialSelfAdjointness (lamP : Nat.Primes → ℝ) : Prop where
 169  weights_summable : WeightSquareSummable lamP
 170  -- The actual statement: T_J on D is essentially self-adjoint.
 171  -- We state this as a Prop awaiting the analytic discharge.
 172  selfadjoint_extension : True
 173
 174/-- Sub-conjecture C.2: compact resolvent for $T_J$ on $\mathcal{H}_-$,
 175    given polynomial decay of weights and linear growth of cost. -/
 176structure CompactResolvent (lamP : Nat.Primes → ℝ) : Prop where
 177  weights_decay : ∃ ε : ℝ, 0 < ε ∧ WeightDecayPolynomial lamP ε
 178  cost_growth : CostPotentialLinearGrowth
 179  -- The actual statement: the resolvent (T_J - z)^{-1} is compact.
 180  -- Stated as a Prop awaiting the analytic discharge.
 181  compact_resolvent_holds : True
 182
 183/-- Sub-conjecture C.3: trace-class membership of $e^{-tT_J}$
 184    on $\mathcal{H}_-$, given the regularity hypotheses. -/
 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. -/
 197theorem regularity_chain {lamP : Nat.Primes → ℝ}
 198    (h_self : EssentialSelfAdjointness lamP)