IndisputableMonolith.Cost.OscillatoryBranchAudit

declarations in this module (12)

• def oscillatoryCost L33
• theorem G_oscillatoryCost L37
• theorem oscillatory_cosh_add_identity L42
• theorem oscillatory_satisfies_composition_law L50
• theorem oscillatory_normalized L56
• theorem oscillatory_reciprocal L60
• theorem oscillatory_second_log_derivative L67
• theorem oscillatory_not_calibrated L91
• theorem oscillatory_negative_at_exp_pi L99
• theorem oscillatory_not_nonnegative_on_positive L105
• structure OscillatoryBranchCert L115
• theorem oscillatory_branch_audit L126