From Coq Require Import Reals Lia ssreflect.

Require Import Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis.

Lemma continuous_abs {K : AbsRing} (x : K) :
  continuous abs x.

Lemma filterlim_abs_0 {K : AbsRing} :
  (∀ x : K, abs x = 0 → x = zero) →
  filterlim (abs (K := K)) (locally' (zero (G := K))) (at_right 0).

Lemma continuous_Rabs (x : R) :
  continuous Rabs x.

Lemma continuous_Rabs_comp f (x : R) :
  continuous f x → continuous (fun x0 ⇒ Rabs (f x0)) x.

Lemma filterlim_Rabs (x : Rbar) :
  filterlim Rabs (Rbar_locally' x) (Rbar_locally (Rbar_abs x)).

Lemma is_lim_Rabs (f : R → R) (x l : Rbar) :
  is_lim f x l → is_lim (fun x ⇒ Rabs (f x)) x (Rbar_abs l).

Lemma filterlim_Rabs_0 :
  filterlim Rabs (Rbar_locally' 0) (at_right 0).

Lemma is_lim_Rabs_0 (f : R → R) (x : Rbar) :
  is_lim f x 0 → Rbar_locally' x (fun x ⇒ f x ≠ 0)
    → filterlim (fun x ⇒ Rabs (f x)) (Rbar_locally' x) (at_right 0).

Lemma filterdiff_Rabs (x : R) :
  x ≠ 0 → filterdiff Rabs (locally x) (fun y : R ⇒ scal y (sign x)).

Lemma is_derive_Rabs (f : R → R) (x df : R) :
  is_derive f x df → f x ≠ 0
    → is_derive (fun x ⇒ Rabs (f x)) x (sign (f x) × df).

Lemma filterlim_Rinv_0_right :
  filterlim Rinv (at_right 0) (Rbar_locally p_infty).

Lemma is_lim_Rinv_0_right (f : R → R) (x : Rbar) :
  is_lim f x 0 → Rbar_locally' x (fun x ⇒ 0 < f x) →
  is_lim (fun x ⇒ / (f x)) x p_infty.

Lemma filterlim_Rinv_0_left :
  filterlim Rinv (at_left 0) (Rbar_locally m_infty).

Lemma is_lim_Rinv_0_left (f : R → R) (x : Rbar) :
  is_lim f x 0 → Rbar_locally' x (fun x ⇒ f x < 0) →
  is_lim (fun x ⇒ / (f x)) x m_infty.

Lemma continuous_Rinv x :
  x ≠ 0 →
  continuous (fun x ⇒ / x) x.

Lemma continuous_Rinv_comp (f : R → R) x:
  continuous f x →
  f x ≠ 0 →
  continuous (fun x ⇒ / (f x)) x.

Lemma filterlim_sqrt_p : filterlim sqrt (Rbar_locally' p_infty) (Rbar_locally p_infty).

Lemma is_lim_sqrt_p (f : R → R) (x : Rbar) :
  is_lim f x p_infty
  → is_lim (fun x ⇒ sqrt (f x)) x p_infty.

Lemma filterdiff_sqrt (x : R) :
  0 < x → filterdiff sqrt (locally x) (fun y ⇒ scal y (/ (2 × sqrt x))).

Lemma is_derive_sqrt (f : R → R) (x df : R) :
  is_derive f x df → 0 < f x
  → is_derive (fun x ⇒ sqrt (f x)) x (df / (2 × sqrt (f x))).

Lemma continuous_sqrt (x : R) : continuous sqrt x.

Lemma continuous_sqrt_comp (f : R → R) x:
  continuous f x →
  continuous (fun x ⇒ sqrt (f x)) x.

Section nat_to_ring.

Context {K : Ring}.

Definition nat_to_ring (n : nat) : K :=
  sum_n_m (fun _ ⇒ one) 1 n.

Lemma nat_to_ring_O :
  nat_to_ring O = zero.

Lemma nat_to_ring_Sn (n : nat) :
  nat_to_ring (S n) = plus (nat_to_ring n) one.

End nat_to_ring.

Section is_derive_mult.

Context {K : AbsRing}.

Lemma is_derive_mult (f g : K → K) x (df dg : K) :
  is_derive f x df → is_derive g x dg
  → (∀ n m : K, mult n m = mult m n)
  → is_derive (fun x : K ⇒ mult (f x) (g x)) x (plus (mult df (g x)) (mult (f x) dg)).

End is_derive_mult.

Lemma filterdiff_pow_n {K : AbsRing} (x : K) (n : nat) :
  (∀ a b : K, mult a b = mult b a)
  → filterdiff (fun y : K ⇒ pow_n y n) (locally x)
    (fun y : K ⇒ scal y (mult (nat_to_ring n) (pow_n x (pred n)))).

Lemma is_derive_n_pow_smalli: ∀ i p x, (i ≤ p)%nat →
  is_derive_n (fun x : R ⇒ x ^ p) i x
    (INR (fact p) / INR (fact (p - i)%nat) × x ^ (p - i)%nat).

Lemma Derive_n_pow_smalli: ∀ i p x, (i ≤ p)%nat →
  Derive_n (fun x : R ⇒ x ^ p) i x
    = INR (fact p) / INR (fact (p - i)%nat) × x ^ (p - i)%nat.

Lemma is_derive_n_pow_bigi: ∀ i p x, (p < i) %nat →
                         is_derive_n (fun x : R ⇒ x ^ p) i x 0.

Lemma Derive_n_pow_bigi: ∀ i p x, (p < i) %nat →
                         Derive_n (fun x : R ⇒ x ^ p) i x = 0.

Lemma Derive_n_pow i p x:
  Derive_n (fun x : R ⇒ x ^ p) i x =
    match (le_dec i p) with
    | left _ ⇒ INR (fact p) / INR (fact (p -i)%nat) × x ^ (p - i)%nat
    | right _ ⇒ 0
    end.

Lemma ex_derive_n_pow i p x: ex_derive_n (fun x : R ⇒ x ^ p) i x.

Lemma is_RInt_pow :
  ∀ a b n,
  is_RInt (fun x ⇒ pow x n) a b (pow b (S n) / INR (S n) - pow a (S n) / INR (S n)).

Lemma exp_ge_taylor (x : R) (n : nat) :
  0 ≤ x → sum_f_R0 (fun k ⇒ x^k / INR (fact k)) n ≤ exp x.

Lemma is_exp_Reals (x : R) :
  is_pseries (fun n ⇒ / INR (fact n)) x (exp x).

Lemma exp_Reals (x : R) :
  exp x = PSeries (fun n ⇒ / INR (fact n)) x.

Lemma is_lim_exp_p : is_lim (fun y ⇒ exp y) p_infty p_infty.

Lemma is_lim_exp_m : is_lim (fun y ⇒ exp y) m_infty 0.

Lemma ex_lim_exp (x : Rbar) : ex_lim (fun y ⇒ exp y) x.

Lemma Lim_exp (x : Rbar) :
  Lim (fun y ⇒ exp y) x =
    match x with
      | Finite x ⇒ exp x
      | p_infty ⇒ p_infty
      | m_infty ⇒ 0
    end.

Lemma is_lim_div_exp_p : is_lim (fun y ⇒ exp y / y) p_infty p_infty.

Lemma is_lim_mul_exp_m : is_lim (fun y ⇒ y × exp y) m_infty 0.

Lemma is_lim_div_expm1_0 : is_lim (fun y ⇒ (exp y - 1) / y) 0 1.

Lemma is_RInt_exp :
  ∀ a b,
  is_RInt exp a b (exp b - exp a).

Lemma continuous_exp x : continuous exp x.

Lemma continuous_exp_comp (f : R → R) x:
  continuous f x →
  continuous (fun x ⇒ exp (f x)) x.

Lemma is_derive_exp : ∀ x, is_derive exp x (exp x).

Lemma is_derive_n_exp : ∀ n x, is_derive_n exp n x (exp x).

Lemma is_lim_ln_p : is_lim (fun y ⇒ ln y) p_infty p_infty.

Lemma is_lim_ln_0 :
  filterlim ln (at_right 0) (Rbar_locally m_infty).

Lemma is_lim_div_ln_p : is_lim (fun y ⇒ ln y / y) p_infty 0.

Lemma is_lim_div_ln1p_0 : is_lim (fun y ⇒ ln (1+y) / y) 0 1.

Lemma continuous_ln x : (0 < x) → continuous ln x.

Lemma is_derive_ln x :
  0 < x → is_derive ln x (/ x)%R.

Lemma is_lim_sinc_0 : is_lim (fun x ⇒ sin x / x) 0 1.

Lemma CV_radius_atan : CV_radius (fun n ⇒ (-1)^n / (INR (S (n + n)))) = 1.

Lemma atan_Reals (x : R) : Rabs x < 1
  → atan x = x × PSeries (fun n ⇒ (-1)^n / (INR (S (n + n)))) (x ^ 2).

Lemma continuous_atan x : continuous atan x.

Lemma continuous_atan_comp (f : R → R) x:
  continuous f x →
  continuous (fun x ⇒ atan (f x)) x.

Lemma is_derive_atan x :
  is_derive atan x (/ (1 + x²)).

Lemma continuous_cos x : continuous cos x.

Lemma continuous_cos_comp (f : R → R) x:
  continuous f x →
  continuous (fun x ⇒ cos (f x)) x.

Lemma is_derive_cos x : is_derive cos x (- sin x).

Lemma continuous_sin x : continuous sin x.

Lemma continuous_sin_comp (f : R → R) x:
  continuous f x →
  continuous (fun x ⇒ sin (f x)) x.

Lemma is_derive_sin x : is_derive sin x (cos x).

Lemma continuous_tan x : cos x ≠ 0 → continuous tan x.

Lemma is_derive_tan x :
  cos x ≠ 0%R → is_derive tan x (tan x ^ 2 + 1)%R.