Library Coq.Reals.Sqrt_reg


Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Require Import R_sqrt.
Require Import Lra.
Local Open Scope R_scope.

Lemma sqrt_var_maj :
  forall h:R, Rabs h <= 1 -> Rabs (sqrt (1 + h) - 1) <= Rabs h.

sqrt is continuous in 1
Lemma sqrt_continuity_pt_R1 : continuity_pt sqrt 1.

sqrt is continuous forall x>0
Lemma sqrt_continuity_pt : forall x:R, 0 < x -> continuity_pt sqrt x.

sqrt is derivable for all x>0
Lemma derivable_pt_lim_sqrt :
  forall x:R, 0 < x -> derivable_pt_lim sqrt x (/ (2 * sqrt x)).

Lemma derivable_pt_sqrt : forall x:R, 0 < x -> derivable_pt sqrt x.

Lemma derive_pt_sqrt :
  forall (x:R) (pr:0 < x),
    derive_pt sqrt x (derivable_pt_sqrt _ pr) = / (2 * sqrt x).

We show that sqrt is continuous for all x>=0 Remark : by definition of sqrt (as extension of Rsqrt on |R), we could also show that sqrt is continuous for all x
Lemma continuity_pt_sqrt : forall x:R, 0 <= x -> continuity_pt sqrt x.