IndisputableMonolith.Numerics.Interval.AlphaBounds

declarations in this module (31)

• theorem alpha_seed_gt L20
• theorem alpha_seed_lt L26
• def exp_taylor_10_at_048 L33
• def exp_error_10_at_048 L37
• lemma exp_048_taylor_ceiling L41
• lemma exp_048_lt L45
• def exp_taylor_10_at_0481 L78
• def exp_error_10_at_0481 L82
• lemma exp_0481_taylor_ceiling L86
• lemma exp_0481_lt L90
• def exp_taylor_10_at_0483 L123
• def exp_error_10_at_0483 L127
• lemma exp_0483_taylor_floor L131
• lemma exp_0483_gt L135
• lemma log_phi_gt_048 L169
• lemma log_phi_gt_0481 L176
• lemma log_phi_lt_0483 L183
• theorem f_gap_gt L190
• theorem f_gap_gt_strong L204
• theorem f_gap_lt L216
• def exp_taylor_10_at_neg_00871 L232
• def exp_error_10_at_neg_00871 L236
• lemma exp_neg_00871_taylor_floor L240
• lemma exp_neg_00871_gt L244
• def exp_taylor_10_at_neg_00866 L268
• def exp_error_10_at_neg_00866 L272
• lemma exp_neg_00866_taylor_ceiling L276
• lemma exp_neg_00866_lt L280
• theorem alphaInv_gt L307
• theorem alphaInv_lt L335
• theorem alphaInv_lt_strong L365