theorem proved term proof

`aczel_kernel_smooth`

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

formal statement (Lean)

  38theorem aczel_kernel_smooth [AczelSmoothnessPackage] (H : ℝ → ℝ) :
  39    dAlembert_continuous_implies_smooth_hypothesis H :=

Term-mode proof.

  40  (aczelRegularityKernel H).smooth
  41
  42/-- Convenience projection: the ODE kernel exported by the classification step. -/

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
step in IndisputableMonolith.Complexity.CellularAutomata decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
AczelSmoothnessPackage in IndisputableMonolith.Cost.AczelClass decl_use
aczelRegularityKernel in IndisputableMonolith.Cost.AczelClassification 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
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use