IndisputableMonolith.Numerics.Interval.Trig

declarations in this module (17)

• def g_upper L42
• theorem g_upper_continuous L44
• theorem g_upper_differentiable L45
• theorem g_upper_deriv L47
• theorem inv_one_add_sq_le_upper L56
• theorem arctan_le_upper_poly L63
• def h_lower L81
• theorem h_lower_continuous L83
• theorem h_lower_differentiable L84
• theorem h_lower_deriv L86
• theorem lower_le_inv_one_add_sq L95
• theorem lower_poly_le_arctan L102
• def arctanOneThirdInterval L122
• theorem arctan_one_third_in_interval L130
• theorem arctan_two_eq L151
• def arctanTwoInterval L161
• theorem arctan_two_in_interval L166