proposition: Lemma maj_term2 : forall (x h eps l1 alp_f2 alp_f2t2:R) (eps_f2:posreal) (f2:R -> R), 0 < eps -> f2 x <> 0 -> f2 (x + h) <> 0 -> (forall a:R, Rabs a < alp_f2t2 -> Rabs (f2 (x + a) - f2 x) < Rabs (eps * Rsqr (f2 x) / (8 * l1))) -> (forall a:R, Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) -> h <> 0 -> Rabs h < alp_f2t2 -> Rabs h < Rmin eps_f2 alp_f2 -> l1 <> 0 -> Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) < eps / 4.
proof: Proof. intros. assert (H8 := H3 h H6). assert (H9 := H2 h H5). apply Rle_lt_trans with (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))). { rewrite Rabs_mult; apply Rmult_le_compat_l. { apply Rabs_pos. } rewrite <- (Rabs_Ropp (f2 x - f2 (x + h))); rewrite Ropp_minus_distr. left; apply H9. } apply Rlt_le_trans with (Rabs (2 * (l1 / (f2 x * f2 x))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))). { apply Rmult_lt_compat_r. { apply Rabs_pos_lt. unfold Rdiv; unfold Rsqr; repeat apply prod_neq_R0; try assumption || discrR. { lra. } apply Rinv_neq_0_compat; apply prod_neq_R0; try assumption || discrR. } unfold Rdiv. repeat rewrite Rinv_mult. repeat rewrite Rabs_mult. replace (Rabs 2) with 2 by (symmetry; apply Rabs_right; left; prove_sup0). rewrite (Rmult_comm 2). replace (Rabs l1 * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with (Rabs l1 * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))) by ring. repeat apply Rmult_lt_compat_l. - apply Rabs_pos_lt; assumption. - apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption. - repeat rewrite Rabs_inv. rewrite <- (Rmult_comm 2). unfold Rdiv in H8; exact H8. } right. unfold Rsqr, Rdiv. rewrite 2!Rinv_mult. repeat rewrite Rabs_mult. repeat rewrite Rabs_inv. replace (Rabs eps) with eps by (symmetry ; apply Rabs_right; left; assumption). replace (Rabs 8) with 8 by (symmetry ; apply Rabs_right; left; prove_sup). replace (Rabs 2) with 2 by (symmetry ; apply Rabs_right; left; prove_sup0). replace 8 with (4 * 2); [ idtac | ring ]. rewrite Rinv_mult. replace (2 * (Rabs l1 * (/ Rabs (f2 x) * / Rabs (f2 x))) * (eps * (Rabs (f2 x) * Rabs (f2 x)) * (/ 4 * / 2 * / Rabs l1))) with (eps * / 4 * (Rabs l1 * / Rabs l1) * (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) * (2 * / 2)); [ idtac | ring ]. repeat rewrite Rinv_r; try (apply Rabs_no_R0; assumption) || discrR. ring. Qed.
imports: Rbase Rfunctions Ranalysis1 Lra