IndisputableMonolith.Numerics.Interval.PhiBounds

declarations in this module (98)

• theorem sq_2236_lt_5 L26
• theorem five_lt_sq_2237 L29
• theorem sqrt5_gt_2236 L32
• theorem sqrt5_lt_2237 L37
• theorem phi_gt_1618 L42
• theorem phi_lt_16185 L48
• theorem sq_22360679_lt_5 L56
• theorem five_lt_sq_22360680 L59
• theorem sqrt5_gt_22360679 L62
• theorem sqrt5_lt_22360680 L67
• theorem phi_gt_161803395 L72
• theorem phi_lt_16180340 L78
• theorem phi_tight_bounds L87
• def phiIntervalTight L91
• theorem phi_in_phiIntervalTight L97
• def phi_quarter_lo L114
• def phi_quarter_hi L117
• lemma phi_quarter_lo_pow4_lt_phi_lo L119
• lemma phi_hi_lt_phi_quarter_hi_pow4 L123
• theorem phi_quarter_gt L128
• theorem phi_quarter_lt L157
• theorem phi_quarter_bounds L185
• theorem phi_neg_quarter_bounds L189
• theorem phi_sq_gt L216
• theorem phi_sq_lt L221
• theorem phi_neg2_gt L229
• theorem phi_neg2_lt L242
• theorem phi_inv_eq L256
• theorem phi_inv_gt L262
• theorem phi_inv_lt L267
• def phi_inv_interval_proven L273
• theorem phi_inv_in_interval_proven L278
• theorem phi_cubed_eq L291
• theorem phi_cubed_gt L299
• theorem phi_cubed_lt L304
• theorem phi_pow4_eq L310
• theorem phi_pow4_gt L319
• theorem phi_pow4_lt L324
• theorem phi_pow5_eq L330
• theorem phi_pow5_gt L339
• theorem phi_pow5_lt L344
• theorem phi_pow6_eq L350
• theorem phi_pow7_eq L360
• theorem phi_pow8_eq L370
• theorem phi_pow8_gt L380
• theorem phi_pow8_lt L385
• def phi_pow8_interval_proven L391
• theorem phi_pow8_in_interval_proven L396
• theorem phi_inv2_gt L409
• theorem phi_inv2_lt L414
• theorem phi_inv3_gt L420
• theorem phi_inv3_lt L427
• def phi_inv3_interval_proven L434
• theorem phi_inv3_in_interval_proven L439
• theorem phi_inv3_zpow_bounds L456
• theorem phi_inv5_gt L492
• theorem phi_inv5_lt L501
• def phi_inv5_interval_proven L511
• theorem phi_inv5_in_interval_proven L516
• theorem phi_pow16_eq L529
• theorem phi_pow16_gt L538
• theorem phi_pow16_lt L543
• theorem phi_pow51_eq L549
• theorem phi_pow51_gt L557
• theorem phi_pow51_lt L562
• def phi_pow51_interval_proven L567
• theorem phi_pow51_in_interval_proven L572
• theorem phi_pow54_eq L579
• theorem phi_pow54_gt L583
• theorem phi_pow54_lt L595
• theorem phi_neg54_gt L609
• theorem phi_neg54_lt L623
• theorem phi_pow58_eq L638
• theorem phi_pow58_gt L642
• theorem phi_pow58_lt L654
• theorem phi_neg58_gt L667
• theorem phi_neg58_lt L680
• lemma qhi_pos L702
• lemma qlo_pos L705
• theorem phi_neg2174_gt L709

… and 18 more