IndisputableMonolith.Cost

declarations in this module (61)

• def Jcost L6
• structure CostRequirements L8
• lemma Jcost_unit0 L12
• lemma Jcost_eq_sq L16
• lemma Jcost_symm L22
• lemma Jcost_nonneg L29
• def AgreesOnExp L34
• lemma Jcost_exp L36
• class SymmUnit L42
• class AveragingAgree L46
• class AveragingDerivation L49
• lemma even_on_log_of_symm L52
• class AveragingBounds L57
• theorem agrees_on_exp_of_bounds L61
• theorem F_eq_J_on_pos_alt L69
• def mkAveragingBounds L81
• class JensenSketch L88
• def F_ofLog L107
• class LogModel L109
• theorem agree_on_exp_extends L141
• theorem F_eq_J_on_pos L148
• theorem F_eq_J_on_pos_of_averaging L153
• theorem agrees_on_exp_of_symm_unit L157
• theorem F_eq_J_on_pos_of_derivation L160
• theorem T5_cost_uniqueness_on_pos L164
• def Jlog L173
• lemma Jlog_as_cosh L175
• lemma hasDerivAt_Jlog L180
• lemma hasDerivAt_Jlog_zero L191
• lemma deriv_Jlog_zero L194
• theorem hasDerivAt_Jcost L198
• theorem deriv_Jcost_one L216
• lemma Jlog_zero L231
• lemma Jlog_nonneg L234
• lemma Jcost_pos_of_ne_one L238
• lemma Jcost_eq_zero_iff L248
• theorem Jcost_surjective_on_nonneg L258
• lemma Jlog_eq_zero_iff L296
• theorem EL_stationary_at_zero L322
• theorem EL_global_min L325
• lemma Jcost_zero_iff_one L329
• lemma Jcost_exp_cosh L335
• def Jmetric L339
• lemma Jmetric_one L342
• lemma Jmetric_symm L346
• lemma Jmetric_nonneg L350
• lemma cosh_minus_one_eq L357
• theorem cosh_quadratic_lower_bound L383
• lemma Jmetric_exp_sinh L414
• theorem Jmetric_val_6 L435
• theorem Jmetric_val_2 L439
• theorem Jmetric_val_3 L443
• theorem sqrt_triangle_violation L447
• theorem Jmetric_triangle_FALSE L471
• theorem Jcost_weak_triangle_FALSE L492
• theorem dalembert_identity L508
• lemma Jcost_submult L519
• lemma Jcost_prod_bound L527
• lemma Jcost_one_plus_eps_quadratic L538
• lemma Jcost_small_strain_bound L572
• lemma Jcost_reciprocal L645