IndisputableMonolith.Cost.FunctionalEquation

declarations in this module (62)

• def G L23
• def H L26
• def CoshAddIdentity L29
• def DirectCoshAdd L34
• lemma CoshAddIdentity_implies_DirectCoshAdd L38
• lemma G_even_of_reciprocal_symmetry L42
• lemma G_zero_of_unit L51
• theorem Jcost_G_eq_cosh_sub_one L54
• theorem Jcost_cosh_add_identity L60
• theorem even_deriv_at_zero L76
• lemma dAlembert_even L97
• lemma dAlembert_double L106
• lemma dAlembert_product L121
• lemma dAlembert_diff_square L139
• def HasLogCurvature L156
• lemma sub_one_eq_mul_ratio L159
• lemma tendsto_H_one_of_log_curvature L166
• theorem dAlembert_continuous_of_log_curvature L192
• lemma deriv_exp_neg L280
• lemma ode_diagonalization L291
• lemma deriv_neg_self_zero L315
• lemma deriv_pos_self_zero L342
• theorem ode_zero_uniqueness L371
• theorem cosh_second_deriv_eq L400
• theorem cosh_initials L407
• theorem ode_cosh_uniqueness_contdiff L414
• def ode_linear_regularity_bootstrap_hypothesis L460
• def ode_regularity_continuous_hypothesis L467
• def ode_regularity_differentiable_hypothesis L474
• theorem cosh_satisfies_bootstrap L484
• theorem cosh_satisfies_continuous L489
• theorem cosh_satisfies_differentiable L494
• theorem ode_cosh_uniqueness L498
• def dAlembert_continuous_implies_smooth_hypothesis L525
• def dAlembert_to_ODE_hypothesis L535
• theorem cosh_dAlembert_smooth L540
• theorem cosh_dAlembert_to_ODE L545
• theorem dAlembert_cosh_solution L549
• theorem dAlembert_cosh_solution_of_log_curvature L569
• def IsReciprocalCost L593
• def IsNormalized L597
• def IsCalibrated L601
• def IsCalibratedLimit L606
• lemma taylorWithinEval_succ_real L609
• lemma taylorWithinEval_one_univ L616
• lemma taylorWithinEval_two_univ L627
• lemma isCalibratedLimit_of_isCalibrated L656
• lemma isCalibrated_of_isCalibratedLimit L676
• def SatisfiesCompositionLaw L700
• theorem reciprocal_implies_G_even L705
• theorem normalized_implies_G_zero L710
• theorem composition_law_equiv_coshAdd L719
• theorem washburn_uniqueness L761
• def symmetric_second_diff_limit_hypothesis L859
• theorem dAlembert_smooth_of_aczel L874
• theorem dAlembert_to_ODE_general_theorem L882
• theorem dAlembert_to_ODE_theorem L960
• theorem ode_regularity_continuous_of_smooth L1035
• theorem ode_regularity_differentiable_of_smooth L1040
• theorem ode_regularity_bootstrap_of_smooth L1045
• theorem dAlembert_cosh_solution_aczel L1053
• theorem washburn_uniqueness_aczel L1076