smooth

used by (40)

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

• standardLagrangian in IndisputableMonolith.Action.QuadraticLimit decl_use
• alphaInv_linear_rate in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
• aczel_kernel_smooth in IndisputableMonolith.Cost.AczelClassification decl_use
• aczelRegularityKernel in IndisputableMonolith.Cost.AczelClassification decl_use
• AczelRegularityKernel in IndisputableMonolith.Cost.AczelClassification decl_use
• primitive_to_uniqueness_of_kernel in IndisputableMonolith.Cost.AczelClassification decl_use
• dAlembert_classification in IndisputableMonolith.Cost.AczelProof decl_use
• dAlembert_contDiff_smooth in IndisputableMonolith.Cost.AczelProof decl_use
• dAlembert_to_ODE_general in IndisputableMonolith.Cost.AczelProof decl_use
• dAlembert_contDiff_smooth in IndisputableMonolith.Cost.AczelTheorem decl_use
• dAlembert_contDiff_top in IndisputableMonolith.Cost.AczelTheorem decl_use
• dAlembert_to_ODE_general in IndisputableMonolith.Cost.AczelTheorem decl_use
• smooth in IndisputableMonolith.Cost.AczelTheorem decl_use
• dAlembert_continuous_implies_smooth_hypothesis in IndisputableMonolith.Cost.FunctionalEquation decl_use
• ode_cosh_uniqueness in IndisputableMonolith.Cost.FunctionalEquation decl_use
• ode_cosh_uniqueness_contdiff in IndisputableMonolith.Cost.FunctionalEquation decl_use
• Jcost_log_second_deriv_normalized in IndisputableMonolith.CPM.LawOfExistence decl_use
• cosh_rescaling_lemma in IndisputableMonolith.Foundation.AxiomDischargePlan decl_use
• ode_cos_unit_uniqueness in IndisputableMonolith.Foundation.AxiomDischargePlan decl_use
• Composition_Normalization_implies_symmetry in IndisputableMonolith.Foundation.CostAxioms decl_use
• separable_forces_additive in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
• IsEntangling in IndisputableMonolith.Foundation.DAlembert.EntanglementGate decl_use
• H_dAlembert_of_G_RCL in IndisputableMonolith.Foundation.DAlembert.FullUnconditional decl_use
• polynomial_consistency_forces_rcl in IndisputableMonolith.Foundation.DAlembert.RightAffineFromFactorization decl_use
• rcl_without_gate in IndisputableMonolith.Foundation.DAlembert.RightAffineFromFactorization decl_use
• StabilityHypotheses in IndisputableMonolith.Foundation.DAlembert.Stability decl_use
• continuous_combiner_log_smoothness_bootstrap in IndisputableMonolith.Foundation.GeneralizedDAlembert decl_use
• log_aczel_data_of_laws in IndisputableMonolith.Foundation.GeneralizedDAlembert decl_use
• PsiAffineOnImage in IndisputableMonolith.Foundation.GeneralizedDAlembert decl_use
• regge_sum in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use

… and 10 more