Library Stdlib.Reals.Ranalysis4

From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import SeqSeries.
From Stdlib Require Import Rtrigo1.
From Stdlib Require Import Ranalysis1.
From Stdlib Require Import Ranalysis3.
From Stdlib Require Import Exp_prop.
From Stdlib Require Import MVT.
From Stdlib Require Import Lra Lia.
Local Open Scope R_scope.

Lemma derivable_pt_inv :
  forall (f:R -> R) (x:R),
    f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x.

Lemma pr_nu_var :
  forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x),
    f = g -> derive_pt f x pr1 = derive_pt g x pr2.

Lemma pr_nu_var2 :
  forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x),
    (forall h:R, f h = g h ) -> derive_pt f x pr1 = derive_pt g x pr2.

Lemma derivable_inv :
  forall f:R -> R, (forall x:R, f x <> 0) -> derivable f -> derivable (/ f).

Lemma derive_pt_inv :
  forall (f:R -> R) (x:R) (pr:derivable_pt f x) (na:f x <> 0),
    derive_pt (/ f) x (derivable_pt_inv f x na pr) =
    - derive_pt f x pr / Rsqr (f x).

Rabsolu

Lemma Rabs_derive_1 : forall x:R, 0 < x -> derivable_pt_lim Rabs x 1.

Lemma Rabs_derive_2 : forall x:R, x < 0 -> derivable_pt_lim Rabs x (-1).

Rabsolu is derivable for all x <> 0

Lemma Rderivable_pt_abs : forall x:R, x <> 0 -> derivable_pt Rabs x.

Rabsolu is continuous for all x

Lemma Rcontinuity_abs : continuity Rabs.

Finite sums : Sum a_k x^k

Lemma continuity_finite_sum :
  forall (An:nat -> R) (N:nat),
    continuity (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N).

Lemma derivable_pt_lim_fs :
  forall (An:nat -> R) (x:R) (N:nat),
    (0 < N)%nat ->
    derivable_pt_lim (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x
    (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N)).

Lemma derivable_pt_lim_finite_sum :
  forall (An:nat -> R) (x:R) (N:nat),
    derivable_pt_lim (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x
    match N with
      | O => 0
      | _ => sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N)
    end.

Lemma derivable_pt_finite_sum :
  forall (An:nat -> R) (N:nat) (x:R),
    derivable_pt (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x.

Lemma derivable_finite_sum :
  forall (An:nat -> R) (N:nat),
    derivable (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N).

Regularity of hyperbolic functions

Lemma derivable_pt_lim_cosh : forall x:R, derivable_pt_lim cosh x (sinh x).

Lemma derivable_pt_lim_sinh : forall x:R, derivable_pt_lim sinh x (cosh x).

Lemma derivable_pt_exp : forall x:R, derivable_pt exp x.

Lemma derivable_pt_cosh : forall x:R, derivable_pt cosh x.

Lemma derivable_pt_sinh : forall x:R, derivable_pt sinh x.

Lemma derivable_exp : derivable exp.

Lemma derivable_cosh : derivable cosh.

Lemma derivable_sinh : derivable sinh.

Lemma derive_pt_exp :
  forall x:R, derive_pt exp x (derivable_pt_exp x) = exp x.

Lemma derive_pt_cosh :
  forall x:R, derive_pt cosh x (derivable_pt_cosh x) = sinh x.

Lemma derive_pt_sinh :
  forall x:R, derive_pt sinh x (derivable_pt_sinh x) = cosh x.

Lemma sinh_lt : forall x y, x < y -> sinh x < sinh y.