proposition: Lemma ln1p_fast0_correct : forall prec xi x, (0 <= x <= /2)%R -> contains (I.convert xi) (Xreal x) -> contains (I.convert (ln1p_fast0 prec xi)) (Xreal (ln (1 + x))).
proof: Proof. intros prec xi x Bx Ix. unfold ln1p_fast0. rewrite ln1p_ln1pc. replace (ln1pc x) with (1 - (1 - ln1pc x))%R by ring. rewrite Rmult_comm. apply J.mul_correct with (2 := Ix). apply J.sub_correct. now apply I.fromZ_small_correct. pose (Ai := fun x => sum_f_R0 (fun n : nat => ((-1) ^ n / INR (n + 1) * x ^ n)%R)). assert (Hexit : forall k powi divi, contains (I.convert powi) (Xreal (x ^ k)) -> contains (I.convert divi) (Xreal (INR ((k + 1) + 1))) -> contains (I.convert (I.bnd F.zero (I.upper (I.div prec (I.mul prec powi xi) divi)))) (Xreal ((-1) ^ (k + 1) * (ln1pc x - Ai x k)))). intros k powi divi Hpow Hdiv. rewrite I.bnd_correct. 2: { now apply I.valid_lb_real; rewrite F.zero_correct. } 2: { apply I.valid_ub_upper. exists (x ^ k * x / INR (k + 1 + 1))%R. now apply J.div_correct; [apply J.mul_correct|]. } rewrite F.zero_correct, I.upper_correct. 2: { exists (x ^ k * x / INR (k + 1 + 1))%R. now apply J.div_correct; [apply J.mul_correct|]. } assert (A: (0 <= (-1) ^ (k + 1) * (ln1pc x - Ai x k) <= x ^ (k + 1) / INR ((k + 1) + 1))%R). replace (Ai x k) with (sum_f_R0 (tg_alt (fun n => / INR (n + 1) * x ^ n)%R) k). unfold Rdiv. rewrite (Rmult_comm (x ^ _)). replace (k + 1) with (S k) by ring. apply alternated_series_ineq'. apply Un_decreasing_ln1pc. lra. apply Un_cv_ln1pc. rewrite Rabs_pos_eq ; lra. unfold ln1pc. case ln1pc_in_int ; intros Hx. case ln1pc_exists ; simpl projT1 ; intros l C. exact C. elim Hx. lra. apply sum_eq. intros n _. unfold tg_alt. apply sym_eq, Rmult_assoc. apply (conj (proj1 A)). assert (H1 := J.mul_correct prec _ _ _ _ Hpow Ix). assert (H2 := J.div_correct prec _ _ _ _ H1 Hdiv). destruct (I.convert (I.div _ _ _)) as [|l [|u]] ; try easy. apply Rle_trans with (1 := proj2 A). apply Rle_trans with (2 := proj2 H2). apply Req_le, Rmult_eq_compat_r. rewrite pow_add. simpl. now rewrite Rmult_1_r. generalize (F.scale c1 (F.ZtoS (Z.neg (F.prec prec)))) (Pos.to_nat (F.prec prec)). intros thre n. replace 1%R with (Ai x 0) by (unfold Ai ; simpl ; field). refine (_ (I.fromZ_small_correct 1 _) (I.fromZ_small_correct 2 _)) ; [|easy..]. fold i1 i2. generalize i1 i2. intros powi divi. change 1%R with (pow x 0). change 2%Z with (Z_of_nat ((0 + 1) + 1)). rewrite <- INR_IZR_INZ. replace (Ai x 0%nat - ln1pc x)%R with ((-1) * 1 * (ln1pc x - Ai x 0%nat))%R by ring. change (-1 * 1)%R with (pow (-1) (0 + 1)). rewrite <- (Nat.sub_diag n) at 1 2 5 7. generalize (Nat.le_refl n). generalize n at 1 4 6 7 9 11. intros m. revert powi divi. induction m as [|m IHm] ; intros powi divi Hm Hpow Hdiv. simpl. cut (contains (I.convert (I.bnd F.zero (I.upper (I.div prec (I.mul prec powi xi) divi)))) (Xreal ((-1) ^ (n - 0 + 1) * (ln1pc x - Ai x (n - 0))))). now destruct F'.cmp. now apply Hexit. simpl ln1p_fast0_aux. set (powi' := I.mul prec powi xi). set (divi' := I.add prec divi i1). specialize (IHm powi' divi'). assert (H: forall p, n - S m + S p = n - m + p). intros p. clear -Hm ; lia. cut (contains (I.convert (I.sub prec (I.div prec powi' divi) (ln1p_fast0_aux prec thre powi' xi divi' m))) (Xreal ((-1) ^ (n - S m + 1) * (ln1pc x - Ai x (n - S m))))). case F'.cmp ; try easy. intros H'. now apply Hexit. replace ((-1) ^ (n - S m + 1) * (ln1pc x - Ai x (n - S m)%nat))%R with ((-1) ^ (n - S m + 1) * (-1) ^ S (n - S m) * x ^ (S (n - S m)) * / INR (S (n - S m) + 1) - (((-1) * (-1) ^ (n - S m + 1)) * (ln1pc x - (Ai x (n - S m)%nat + ((-1) ^ S (n - S m) * / INR (S (n - S m) + 1) * x ^ (S (n - S m)))))))%R by ring. apply J.sub_correct. rewrite <- pow_add. replace (n - S m + 1 + S (n - S m)) with (2 * (n - S m + 1)) by (clear -Hm ; lia). replace (S (n - S m)) with (n - S m + 1) by now rewrite Nat.add_comm. apply J.div_correct with (2 := Hdiv). rewrite pow_1_even, Rmult_1_l. rewrite pow_add, pow_1. now apply J.mul_correct. evar_last. apply IHm. clear -Hm ; lia. rewrite <- (Nat.add_0_r (n - m)), <- H. rewrite pow_add, pow_1. now apply J.mul_correct. rewrite <- H. replace (_ + 2 + 1) with (n - S m + 1 + 1 + 1) by ring. rewrite plus_INR. apply J.add_correct with (1 := Hdiv). now apply I.fromZ_small_correct. change (Ai x (n - S m)%nat + (-1) ^ S (n - S m) * / INR (S (n - S m) + 1) * x ^ (S (n - S m)))%R with (Ai x (S (n - S m))). change (-1 * (-1) ^ (n - S m + 1))%R with ((-1) ^ (S (n - S m + 1)))%R. rewrite <- plus_Sn_m. now rewrite <-Nat.sub_succ_l. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float