module module

`IndisputableMonolith.NumberTheory.CostOperatorRegularity`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.NumberTheory.HilbertPolyaCandidate module_import

declarations in this module (13)

def denseDomain L51
theorem denseDomain_nonempty L54
theorem denseDomain_mem L57
structure CostPotentialBound L70
def CostPotentialLinearGrowth L84
def WeightSquareSummable L93
def WeightDecayPolynomial L98
theorem weight_polynomial_decay_summable L104
structure EssentialSelfAdjointness L168
structure CompactResolvent L176
structure TraceClassHeatKernel L185
theorem regularity_chain L197
theorem cost_operator_regularity_certificate L206