R_compl.v

(**
This file is part of the Elfic library

Copyright (C) Boldo, Clément, Faissole, Leclerc, Martin, Mayero

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

From Coq Require Import Lia Reals Lra.
From Coquelicot Require Import Coquelicot.
From Flocq Require Import Core. (* For Zfloor, Zceil. *)


Section R_ring_compl.

(** Complements on ring operations Rplus and Rmult. **)

Lemma Rplus_not_eq_compat_l : forall r r1 r2, r1 <> r2 -> r + r1 <> r + r2.
Proof.
intros r r1 r2 H H'.
apply Rplus_eq_reg_l in H'.
contradiction.
Qed.

Lemma Rminus_plus_asso : forall a b c, a - (b + c) = a - b - c.
Proof.
intros; ring.
Qed.

Lemma Rmult_lt_pos_pos_pos: forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2.
Proof.
intros r1 r2 H1 H2.
now apply Rmult_lt_0_compat.
Qed.

Lemma Rmult_lt_neg_neg_pos: forall r1 r2, r1 < 0 -> r2 < 0 -> 0 < r1 * r2.
Proof.
intros r1 r2 H1 H2.
generalize (Ropp_gt_lt_0_contravar r1 H1).
generalize (Ropp_gt_lt_0_contravar r2 H2).
clear H1 H2; intros H2 H1.
generalize (Rmult_lt_0_compat (-r1) (-r2) H1 H2).
intro H.
replace (- r1 * - r2) with (r1*r2) in H;[auto|ring].
Qed.

Lemma Rmult_lt_neg_pos_neg: forall r1 r2, r1 < 0 -> 0 < r2 -> r1 * r2 < 0.
Proof.
intros r1 r2 H1 H2.
generalize (Ropp_gt_lt_0_contravar r1 H1).
clear H1; intros H1.
generalize (Rmult_lt_0_compat (-r1) (r2) H1 H2).
intro H.
replace (- r1 * r2) with (-(r1*r2)) in H;try ring.
rewrite <- (Ropp_involutive 0) in H.
apply Ropp_lt_cancel.
rewrite Ropp_0.
now rewrite (Ropp_involutive 0) in H.
Qed.

End R_ring_compl.


Section R_order_compl.

(** Complements on order. **)

Definition R2N : R -> nat := fun x => Z.abs_nat (Zfloor (Rabs x)).

Lemma R2N_INR : forall n, R2N (INR n) = n.
Proof.
intros n; unfold R2N.
rewrite Rabs_right, INR_IZR_INZ, Zfloor_IZR, Zabs2Nat.id; try easy.
apply Rle_ge, pos_INR.
Qed.

Lemma Zfloor_opp : forall x, Zfloor (- x) = (- Zceil x)%Z.
Proof.
intros x; unfold Zceil; lia.
Qed.

Lemma Zceil_opp : forall x, Zceil (- x) = (- Zfloor x)%Z.
Proof.
intros x; unfold Zceil; now rewrite Ropp_involutive.
Qed.

Lemma archimed_floor : forall x, IZR (Zfloor x) <= x < IZR (Zfloor x) + 1.
Proof.
intros x; unfold Zfloor; rewrite minus_IZR.
replace (IZR (up x) - 1 + 1) with (IZR (up x)) by ring.
generalize (archimed x); intros [H1 H2]; lra.
Qed.

Lemma archimed_ceil : forall x, IZR (Zceil x) - 1 < x <= IZR (Zceil x).
Proof.
intros x; generalize (archimed_floor (- x)); intros [H1 H2].
rewrite Zfloor_opp, opp_IZR in H1, H2; lra.
Qed.

Lemma archimed_floor_ex : forall x, exists (n : Z), IZR n <= x < IZR n + 1.
Proof.
intros x; exists (Zfloor x); unfold Zfloor; rewrite minus_IZR.
replace (IZR (up x) - 1 + 1) with (IZR (up x)) by ring.
generalize (archimed x); intros [H1 H2]; lra.
Qed.

Lemma archimed_floor_uniq :
  forall x (n1 n2 : Z),
    IZR n1 <= x < IZR n1 + 1 ->
    IZR n2 <= x < IZR n2 + 1 ->
    n1 = n2.
Proof.
intros x n1 n2 H1 H2.
transitivity (Zfloor x); [symmetry | ];
    now apply Zfloor_imp; rewrite plus_IZR.
Qed.

Lemma archimed_ceil_ex : forall x, exists (n : Z), IZR n - 1 < x <= IZR n.
Proof.
intros x; generalize (archimed_floor_ex (- x)); intros [n [Hn1 Hn2]].
exists (- n)%Z; rewrite opp_IZR; lra.
Qed.

Lemma archimed_ceil_uniq :
  forall x (n1 n2 : Z),
    IZR n1 - 1 < x <= IZR n1 ->
    IZR n2 - 1 < x <= IZR n2 ->
    n1 = n2.
Proof.
intros x n1 n2 H1 H2.
transitivity (Zceil x); [symmetry | ];
    now apply Zceil_imp; rewrite minus_IZR.
Qed.

Lemma Rlt_plus_le_ex : forall a b, a < b <-> exists n, a + / (INR n + 1) <= b.
Proof.
intros a b; split.
(* *)
intros H1.
apply Rminus_lt_0 in H1.
generalize (Rinv_0_lt_compat (b - a) H1); intros H2.
generalize (archimed_floor_ex (/ (b - a))); intros [n [_ Hn]].
exists (Z.abs_nat n).
rewrite INR_IZR_INZ, Zabs2Nat.id_abs, abs_IZR, Rabs_pos_eq.
rewrite Rplus_comm, <- Rle_minus_r, <- (Rinv_involutive (b - a)).
apply Rinv_le_contravar; try easy; now apply Rlt_le.
now apply not_eq_sym, Rlt_not_eq.
apply IZR_le, Z.lt_succ_r, lt_IZR; unfold Z.succ; rewrite plus_IZR.
now apply Rlt_trans with (/ (b - a)).
(* *)
intros [n Hn].
apply Rlt_le_trans with (a + / (INR n + 1)); try easy.
rewrite <- Rplus_0_r at 1.
apply Rplus_lt_compat_l, Rinv_0_lt_compat, INRp1_pos.
Qed.

Lemma Rlt_le_minus_ex : forall a b, a < b <-> exists n, a <= b - / (INR n + 1).
Proof.
intros a b; rewrite Rlt_plus_le_ex; split; intros [n Hn].
exists n; now rewrite Rle_minus_r.
exists n; now rewrite <- Rle_minus_r.
Qed.

Lemma intoo_intco_ex :
  forall a b x, a < x < b <-> exists n, a + / (INR n + 1) <= x < b.
Proof.
intros a b x.
generalize (Rlt_plus_le_ex a x); intros [Ha1 Ha2].
split.
intros [Hx1 Hx2]; apply Ha1 in Hx1; destruct Hx1 as [n Hn]; now exists n.
intros [n [Hx1 Hx2]]; split; [apply Ha2; exists n | ]; easy.
Qed.

Lemma intoo_intoc_ex :
  forall a b x, a < x < b <-> exists n, a < x <= b - / (INR n + 1).
Proof.
intros a b x.
generalize (Rlt_le_minus_ex x b); intros [Hb1 Hb2].
split.
intros [Hx1 Hx2]; apply Hb1 in Hx2; destruct Hx2 as [n Hn]; now exists n.
intros [n [Hx1 Hx2]]; split; [ | apply Hb2; exists n]; easy.
Qed.

Lemma intoo_intcc_ex :
  forall a b x,
    a < x < b <-> exists n, a + / (INR n + 1) <= x <= b - / (INR n + 1).
Proof.
intros a b x.
generalize (Rlt_plus_le_ex a x); intros [Ha1 Ha2].
generalize (Rlt_le_minus_ex x b); intros [Hb1 Hb2].
split.
(* *)
intros [Hx1 Hx2].
apply Ha1 in Hx1; destruct Hx1 as [n1 Hn1].
apply Hb1 in Hx2; destruct Hx2 as [n2 Hn2].
exists (max n1 n2); split.
apply Rle_trans with (a + / (INR n1 + 1)); try easy.
apply Rplus_le_compat_l, Rinv_le_contravar; try apply INRp1_pos.
apply Rplus_le_compat_r, le_INR, Nat.le_max_l.
apply Rle_trans with (b - / (INR n2 + 1)); try easy.
apply Rplus_le_compat_l, Ropp_le_contravar, Rinv_le_contravar.
apply INRp1_pos.
apply Rplus_le_compat_r, le_INR, Nat.le_max_r.
(* *)
intros [n [Hx1 Hx2]]; split; [apply Ha2 | apply Hb2]; now exists n.
Qed.

Lemma Rlt_increasing :
  forall u N,
    (forall i, (i < N)%nat -> u i < u (S i)) ->
    forall i j, (i <= j <= N)%nat -> u i <= u j.
Proof.
intros u N H i j Hij.
replace j with (i + (j - i))%nat by auto with zarith.
cut (j - i <= N)%nat; try auto with zarith.
cut (i + (j - i) <= N)%nat; try auto with zarith.
generalize (j-i)%nat.
induction n; intros M1 M2.
rewrite plus_0_r.
apply Rle_refl.
apply Rle_trans with (u (i + n)%nat).
apply IHn; auto with zarith.
replace (i + S n)%nat with (S (i + n)) by auto with zarith.
apply Rlt_le, H.
auto with zarith.
Qed.

Lemma Rle_0_cont_l :
  forall f a,
    (filterlim f (at_left a) (locally (f a))) ->
    at_left a (fun x => 0 <= f x) ->
    0 <= f a.
Proof.
intros f a Hf Hf'.
apply (@closed_filterlim_loc _ _ (at_left a) _ f); try assumption.
apply closed_ge.
Qed.

Lemma Rlt_0_cont_l :
  forall f a,
    (filterlim f (at_left a) (locally (f a))) ->
    at_left a (fun x => 0 < f x) ->
    0 <= f a.
Proof.
intros f a H [eps Heps].
apply Rle_0_cont_l; try assumption.
exists eps.
intros y H1 H2.
now apply Rlt_le, Heps.
Qed.

End R_order_compl.


Section R_intervals_compl.

(** Operations on rays ond intervals. **)

Lemma interval_sum :
  forall a b c x,
    a <= b <= c ->
    (a <= x < b \/ b <= x < c) <-> a <= x < c.
Proof.
intros a b c x [H H']; split.
intros [[H1 H1'] | [H1 H1']]; split; try easy;
    [apply Rlt_le_trans with b | apply Rle_trans with b]; assumption.
intros [H1 H1']; case (Rle_dec b x); intros; intuition.
Qed.

Lemma interval_difference_l :
  forall a b c x,
    a <= b <= c ->
    (a <= x < c /\ ~ b <= x < c) <-> a <= x < b.
Proof.
intros a b c x [H H']; split; intros [H1 H1']; repeat split; try easy.
case (Rle_dec b x); intros H2; intuition.
apply Rlt_le_trans with b; assumption.
intros [H2 H2']; apply Rle_not_lt in H2; contradiction.
Qed.

Lemma interval_difference_r :
  forall a b c x,
    a <= b <= c ->
    (a <= x < c /\ ~ a <= x < b) <-> b <= x < c.
Proof.
intros a b c x [H H']; split; intros [H1 H1']; repeat split; try easy.
case (Rle_dec b x); intros H2; intuition; now apply Rnot_lt_le.
apply Rle_trans with b; assumption.
intros [H2 H2']; apply Rle_not_lt in H1; contradiction.
Qed.

End R_intervals_compl.


Section R_atan_compl.

(** Atan Lipschitz on R. **)

Lemma Rsqrp1_pos : forall z, 0 < 1 + Rsqr z.
Proof.
intros z; apply Rplus_lt_le_0_compat; [apply Rlt_0_1 | apply Rle_0_sqr].
Qed.

Lemma Rsqrp1_not_0 : forall z, 1 + Rsqr z <> 0.
Proof.
intros z; apply Rgt_not_eq, Rlt_gt, Rsqrp1_pos.
Qed.

Lemma atan_Lipschitz_aux : forall x y, x <= y -> atan y - atan x <= y - x.
Proof.
intros x y Hxy.
apply Rplus_le_reg_r with (atan x), Rplus_le_reg_l with (- y); ring_simplify.
replace (atan x - x) with (- x + atan x).
2: now ring_simplify.
pose (pr1 := fun z => derivable_pt_opp _ z (derivable_pt_id z)).
pose (pr := fun z => derivable_pt_plus _ _ _ (pr1 z) (derivable_pt_atan z)).
(* *)
assert (H : decreasing (fun x => - x + atan x)).
apply nonpos_derivative_1 with pr.
intros z.
replace (derive_pt (- id + atan) z (pr z)) with (- (Rsqr z / (1 + Rsqr z))).
apply Rge_le, Ropp_0_le_ge_contravar, Rdiv_le_0_compat;
    [apply Rle_0_sqr | apply Rsqrp1_pos].
unfold pr; rewrite derive_pt_plus; clear pr.
unfold pr1; rewrite derive_pt_opp; clear pr1.
rewrite derive_pt_id, derive_pt_atan.
replace (- (1) + 1 / (1 + Rsqr z)) with (- (1 - 1 / (1 + Rsqr z))); try now ring_simplify.
apply Ropp_eq_compat, Rmult_eq_reg_r with (1 + Rsqr z);
    try field_simplify; now try apply Rsqrp1_not_0.
(* *)
now apply H.
Qed.

Lemma atan_Lipschitz : forall x y, Rabs (atan x - atan y) <= Rabs (x - y).
(* Reciprocal Rabs (x - y) <= K * Rabs (atan x - atan y) is wrong! *)
Proof.
assert (H : forall x y, x <= y -> Rabs (atan x - atan y) <= Rabs (x - y)).
intros x y Hxy.
replace (Rabs (atan x - atan y)) with (atan y - atan x).
replace (Rabs (x - y)) with (y - x).
now apply atan_Lipschitz_aux.
rewrite Rabs_minus_sym; symmetry; apply Rabs_pos_eq;
    apply Rplus_le_reg_r with x; now ring_simplify.
rewrite Rabs_minus_sym; symmetry; apply Rabs_pos_eq;
    apply Rplus_le_reg_r with (atan x); ring_simplify.
destruct Hxy as [Hxy | Hxy];
    [left; now apply atan_increasing | right; now rewrite Hxy].
(* *)
intros x y; case (Rle_lt_dec x y); intros Hxy.
now apply H.
rewrite Rabs_minus_sym.
replace (Rabs (x - y)) with (Rabs (y - x)).
2: now rewrite Rabs_minus_sym.
now apply H, Rlt_le.
Qed.

End R_atan_compl.

Require Import
  Utf8
.

Section Rpow_def_and_prop.

  (* Une fonction puissance R*₊×R ∪ {0}×R*₊ -> R⁺ *)

  Definition Rpow (x p : R) :=
    match Req_EM_T x 0 with
      | left _ => 0
      | right _ => exp (p * ln x)
    end.

    Lemma Rpow_plus : ∀ x y z : R, Rpow z (x + y) = Rpow z x * Rpow z y.
    Proof.
      intros x y z.
      unfold Rpow; case (Req_EM_T z 0).
      lra.
      intros Hz.
      rewrite Rmult_plus_distr_r.
      rewrite exp_plus.
      reflexivity.
    Qed.

    Lemma Rpow_mult : ∀ x y z : R, Rpow (Rpow x y) z = Rpow x (y * z).
    Proof.
      intros x y z.
      unfold Rpow; case (Req_EM_T z 0).
      intros ->.
      case (Req_EM_T x 0).
      intros _.
      case (Req_EM_T 0 0); easy.
      intros Neq0x.
      case (Req_EM_T (exp (y * ln x))).
      assert (exp (y * ln x) > 0) by apply exp_pos.
      lra.
      intros _.
      rewrite Rmult_0_r; do 2 rewrite Rmult_0_l; try easy.
      intros _.
      case (Req_EM_T x 0).
      case (Req_EM_T 0 0); easy.
      intros _.
      case (Req_EM_T (exp (y * ln x)) 0).
      assert (exp (y * ln x) > 0) by apply exp_pos.
      lra.
      intros _.
      rewrite ln_exp.
      f_equal.
      lra.
    Qed.

    Lemma Rpow_0 : ∀ x : R, 0 < x -> Rpow x 0 = 1.
    Proof.
      intros x Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _; rewrite Rmult_0_l; rewrite exp_0; easy.
    Qed.

    Lemma Rpow_0_alt : ∀ p : R, 0 < p -> Rpow 0 p = 0.
    Proof.
      intros p Hp.
      unfold Rpow.
      case (Req_EM_T 0 0); easy.
    Qed.

    Lemma Rpow_1 : ∀ x : R, 0 <= x -> Rpow x 1 = x.
    Proof.
      intros x Hx.
      unfold Rpow; case (Req_EM_T x 0).
      lra.
      intros H; rewrite Rmult_1_l, exp_ln; try easy.
      lra.
    Qed.

    Lemma Rpow_pow : ∀ (n : nat) (x : R), 0 <= x -> (0 < n)%nat -> Rpow x (INR n) = x ^ n.
    Proof.
      intros n x Hx Hn.
      unfold Rpow.
      case (Req_EM_T x 0).
      intros ->.
      rewrite pow_ne_zero; try easy.
      lia.
      intros Neq0x.
      rewrite <-ln_pow.
      2 : lra.
      rewrite exp_ln; try easy.
      apply pow_lt; lra.
    Qed.

    Lemma Rpow_pos : ∀ (x : R) (y : R), 0 < x -> 0 < Rpow x y.
    Proof.
      intros x n Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _; apply exp_pos.
    Qed.

    Lemma Rpow_nonneg : ∀ (x : R) (y : R), 0 <= x -> 0 <= Rpow x y.
    Proof.
      intros x n Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      apply Rlt_le, exp_pos.
    Qed.

    Lemma Rpow_lt :
      ∀ x y z : R, 1 < x -> y < z -> Rpow x y < Rpow x z.
    Proof.
      intros x y z Hx Hyz.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      apply exp_increasing.
      apply Rmult_lt_compat_r.
      rewrite <-ln_1.
      apply ln_increasing; lra.
      assumption.
    Qed.

    Lemma Rpow_sqrt : ∀ x : R, 0 <= x -> Rpow x (/ 2) = sqrt x.
    Proof.
      intros x Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      intros ->.
      rewrite sqrt_0; try easy.
      intros Neq0x.
      replace x with (sqrt x)².
      2 : rewrite Rsqr_sqrt; try easy.
      unfold Rsqr at 1.
      rewrite ln_mult.
      2, 3 : apply sqrt_lt_R0; lra.
      rewrite <-RIneq.double.
      rewrite <-Rmult_assoc.
      rewrite Rinv_l.
      rewrite Rmult_1_l.
      rewrite exp_ln.
      3 : lra.
      2 : apply sqrt_lt_R0; lra.
      rewrite Rsqr_sqrt; easy.
    Qed.

    Lemma Rpow_Ropp : ∀ x y : R, 0 < x -> Rpow x (- y) = / (Rpow x y).
    Proof.
      intros x y Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      rewrite <-exp_Ropp.
      f_equal; lra.
    Qed.

    Lemma powerRZ_Rpow x z : (0 < x)%R -> powerRZ x z = Rpow x (IZR z).
    Proof.
      intros Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      case z.
      simpl; rewrite Rmult_0_l, exp_0; try easy.
      intros p; simpl.
      rewrite <-Rpow_pow; unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      rewrite INR_IZR_INZ.
      f_equal; f_equal; f_equal.
      apply positive_nat_Z.
      lra.
      lia.
      intros p; simpl.
      rewrite <-Rpow_pow; unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      rewrite INR_IZR_INZ.
      rewrite <-exp_Ropp.
      f_equal.
      rewrite Ropp_mult_distr_l.
      f_equal.
      rewrite <-opp_IZR.
      f_equal.
      apply Z.eq_opp_r.
      rewrite Pos2Z.opp_neg.
      apply positive_nat_Z.
      lra.
      lia.
    Qed.

    Lemma Rle_Rpow :
      ∀ e n m : R, 1 <= e -> n <= m -> Rpow e n <= Rpow e m.
    Proof.
      intros e n m He Hnm.
      unfold Rpow.
      case (Req_EM_T e 0).
      lra.
      intros _.
      apply exp_le.
      apply Rmult_le_compat_r.
      rewrite <-ln_1.
      apply ln_le; lra.
      assumption.
    Qed.

    Lemma ln_Rpow : ∀ x y : R, 0 < x -> ln (Rpow x y) = y * ln x.
    Proof.
      intros x y Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      rewrite ln_exp; easy.
    Qed.

    Lemma Rpow_inv : ∀ x p : R, 0 <= x -> p ≠ 0 -> Rpow (Rpow x p) (/p) = x.
    Proof.
      intros x p Hx Hp.
      rewrite Rpow_mult.
      rewrite Rinv_r; try easy.
      rewrite Rpow_1; easy.
    Qed.

    Lemma Rpow_inv_alt : ∀ x p : R, 0 <= x -> p ≠ 0 -> Rpow (Rpow x (/p)) p = x.
    Proof.
      intros x p Hx Hp.
      rewrite Rpow_mult.
      rewrite Rinv_l; try easy.
      rewrite Rpow_1; easy.
    Qed.

End Rpow_def_and_prop.