IndisputableMonolith.Foundation.GeneralizedDAlembert

declarations in this module (38)

• theorem aczel_kannappan_continuous_dAlembert L90
• def ContinuousRouteIndependence L110
• structure SatisfiesLawsOfLogicContinuous L121
• structure LogAczelData L131
• theorem continuous_log_cost_of_continuousOn_positive L141
• theorem log_aczel_data_of_laws L158
• def mollified L212
• theorem mollified_continuous L218
• theorem mollified_pointwise_tendsto L233
• def MollifierCkRoute L247
• theorem mollifierCkRoute_exists L253
• theorem polynomial_continuous L277
• theorem polynomial_implies_continuous L285
• theorem laws_polynomial_implies_continuous L300
• def LogBilinearIdentity L322
• def ClassifiedLogCost L329
• theorem log_zero_bilinear_identity L336
• theorem log_parabolic_bilinear_identity L342
• theorem log_cosh_sub_one_bilinear_identity L348
• theorem log_one_sub_cos_bilinear_identity L358
• theorem classified_log_cost_bilinear L368
• theorem classified_positive_cost_bilinear L392
• theorem log_bilinear_affine_lift_dAlembert L422
• theorem log_bilinear_affine_lift_classification L434
• theorem log_bilinear_positive_cost_bilinear L452
• def ContinuousCombinerMollifierFiniteSmoothness L493
• theorem continuous_combiner_finite_smoothness_to_top L505
• theorem continuous_combiner_log_smoothness_bootstrap L517
• def AczelSecondDerivativeIdentity L527
• def PsiAffineOnImage L532
• def ContinuousCombinerSecondDerivativeInput L544
• def ContinuousCombinerPsiAffineCompletion L557
• structure ContinuousCombinerAnalysisInputs L569
• theorem continuous_combiner_psi_affine_forcing L583
• theorem continuous_combiner_bilinear_classification L598
• theorem continuous_combiner_bilinear L617
• theorem RCL_is_unique_functional_form_of_logic_continuous L638
• theorem laws_continuous_subsumes_polynomial L653