equal
deleted
inserted
replaced
806 using arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float ?invx\<close> \<open>real_of_float ?invx \<le> 1\<close>] |
806 using arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float ?invx\<close> \<open>real_of_float ?invx \<le> 1\<close>] |
807 by (auto intro!: float_round_up_le) |
807 by (auto intro!: float_round_up_le) |
808 also note float_round_up |
808 also note float_round_up |
809 finally have "pi / 2 - float_round_up prec (?ub_horner ?invx) \<le> arctan x" |
809 finally have "pi / 2 - float_round_up prec (?ub_horner ?invx) \<le> arctan x" |
810 using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>] |
810 using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>] |
811 unfolding real_sgn_pos[OF \<open>0 < 1 / real_of_float x\<close>] le_diff_eq by auto |
811 unfolding sgn_pos[OF \<open>0 < 1 / real_of_float x\<close>] le_diff_eq by auto |
812 moreover |
812 moreover |
813 have "lb_pi prec * Float 1 (- 1) \<le> pi / 2" |
813 have "lb_pi prec * Float 1 (- 1) \<le> pi / 2" |
814 unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp |
814 unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp |
815 ultimately |
815 ultimately |
816 show ?thesis |
816 show ?thesis |
933 by (auto intro!: float_round_down_le) |
933 by (auto intro!: float_round_down_le) |
934 also have "\<dots> \<le> arctan (1 / x)" |
934 also have "\<dots> \<le> arctan (1 / x)" |
935 unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone') (rule float_divl) |
935 unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone') (rule float_divl) |
936 finally have "arctan x \<le> pi / 2 - (?lb_horner ?invx)" |
936 finally have "arctan x \<le> pi / 2 - (?lb_horner ?invx)" |
937 using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>] |
937 using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>] |
938 unfolding real_sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto |
938 unfolding sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto |
939 moreover |
939 moreover |
940 have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)" |
940 have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)" |
941 unfolding Float_num times_divide_eq_right mult_1_right |
941 unfolding Float_num times_divide_eq_right mult_1_right |
942 using pi_boundaries by auto |
942 using pi_boundaries by auto |
943 ultimately |
943 ultimately |