module
module
IndisputableMonolith.Cost.AczelClassification
show as:
view Lean formalization →
used by (1)
depends on (3)
declarations in this module (10)
-
structure
AczelRegularityKernel -
def
aczelRegularityKernel -
theorem
aczel_kernel_smooth -
theorem
aczel_kernel_ode -
structure
PrimitiveCostHypotheses -
theorem
H_one_of_normalized -
theorem
H_continuous_of_positive_continuous -
theorem
H_dAlembert_of_composition -
theorem
primitive_to_uniqueness_of_kernel -
theorem
primitive_to_uniqueness_aczel