structure definition def or abbrev

`AczelRegularityKernel`

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

formal statement (Lean)

  23structure AczelRegularityKernel (H : ℝ → ℝ) : Prop where
  24  smooth : dAlembert_continuous_implies_smooth_hypothesis H
  25  ode : dAlembert_to_ODE_hypothesis H
  26
  27/-- The default kernel obtained from the current Aczél smoothness package. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

aczelRegularityKernel in IndisputableMonolith.Cost.AczelClassification decl_use
H_dAlembert_of_composition in IndisputableMonolith.Cost.AczelClassification decl_use
primitive_to_uniqueness_of_kernel in IndisputableMonolith.Cost.AczelClassification decl_use
PublicCostLayer in IndisputableMonolith.Foundation.DimensionalConstraints.CostLayer decl_use

depends on (11)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
default in IndisputableMonolith.Chemistry.PeriodicTable decl_use
default in IndisputableMonolith.Config.Flags decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
smooth in IndisputableMonolith.Cost.AczelProof decl_use
smooth in IndisputableMonolith.Cost.AczelTheorem decl_use
dAlembert_continuous_implies_smooth_hypothesis in IndisputableMonolith.Cost.FunctionalEquation decl_use
dAlembert_to_ODE_hypothesis in IndisputableMonolith.Cost.FunctionalEquation decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use