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