IndisputableMonolith.Numerics.Interval.Log

declarations in this module (27)

• def logLowerSimple L31
• def logUpperSimple L34
• def logIntervalMono L37
• theorem logIntervalMono_contains_log L46
• def logPhiInterval L69
• lemma phi_minus_one_abs L92
• lemma phi_minus_one_abs_lt_one L96
• lemma complex_norm_ofReal L101
• lemma log_taylor_error_bound L106
• lemma log_one_add_bounds L136
• def exp_taylor_10_at_048 L179
• def exp_error_10_at_048 L184
• lemma exp_048_lt_phi L189
• theorem log_phi_gt_048 L196
• def exp_taylor_10_at_0481 L222
• def exp_error_10_at_0481 L227
• lemma exp_0481_lt_phi L232
• theorem log_phi_gt_0481 L239
• def exp_taylor_10_at_0483 L262
• def exp_error_10_at_0483 L267
• lemma phi_lt_exp_0483 L272
• theorem log_phi_lt_0483 L279
• theorem log_phi_in_interval L312
• def log2Interval L333
• theorem log_2_in_interval L339
• def log10Interval L358
• theorem log_10_in_interval L369