(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat.
Require Import boolp reals ereal nsatz_realtype classical_sets posnum functions.
Require Import topology normedtype landau sequences derive realfun.

Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Lemma normr_nneg (R : numDomainType) (x : R) : `|x| \is Num.nneg.
#[global] Hint Resolve normr_nneg : core.

Section PseriesDiff.

Variable R : realType.

Definition pseries f (x : R) := [series f i × x ^+ i]_i.

Fact is_cvg_pseries_inside_norm f (x z : R) :
  cvg (pseries f x) → `|z| < `|x| → cvg (pseries (fun i ⇒ `|f i|) z).

Fact is_cvg_pseries_inside f (x z : R) :
  cvg (pseries f x) → `|z| < `|x| → cvg (pseries f z).

Definition pseries_diffs (f : nat → R) i := i.+1%:R × f i.+1.

Lemma pseries_diffsN (f : nat → R) : pseries_diffs (- f) = -(pseries_diffs f).

Lemma pseries_diffs_inv_fact :
  pseries_diffs (fun n ⇒ (n`!%:R)^-1) = (fun n ⇒ (n`!%:R)^-1 : R).

Lemma pseries_diffs_sumE n f x :
  \sum_(0 ≤ i < n) pseries_diffs f i × x ^+ i =
  (\sum_(0 ≤ i < n) i%:R × f i × x ^+ i.-1) + n%:R × f n × x ^+ n.-1.

Lemma pseries_diffs_equiv f x :
  let s i := i%:R × f i × x ^+ i.-1 in
  cvg (pseries (pseries_diffs f) x) → series s -->
  lim (pseries (pseries_diffs f) x).

Lemma is_cvg_pseries_diffs_equiv f x :
  cvg (pseries (pseries_diffs f) x) → cvg [series i%:R × f i × x ^+ i.-1]_i.

Let pseries_diffs_P1 m (z h : R) :
  \sum_(0 ≤ i < m) ((h + z) ^+ (m - i) × z ^+ i - z ^+ m) =
  \sum_(0 ≤ i < m) z ^+ i × ((h + z) ^+ (m - i) - z ^+ (m - i)).

Let pseries_diffs_P2 n (z h : R) :
  h != 0 →
  ((h + z) ^+ n - (z ^+ n)) / h - n%:R × z ^+ n.-1 =
  h × \sum_(0 ≤ i < n.-1) z ^+ i ×
      \sum_(0 ≤ j < n.-1 - i) (h + z) ^+ j × z ^+ (n.-2 - i - j).

Let pseries_diffs_P3 (z h : R) n K :
  h != 0 → `|z| ≤ K → `|h + z| ≤ K →
    `|((h +z) ^+ n - z ^+ n) / h - n%:R × z ^+ n.-1|
      ≤ n%:R × n.-1%:R × K ^+ n.-2 × `|h|.

Lemma pseries_snd_diffs (c : R^nat) K x :
  cvg (pseries c K) →
  cvg (pseries (pseries_diffs c) K) →
  cvg (pseries (pseries_diffs (pseries_diffs c)) K) →
  `|x| < `|K| →
  is_derive x 1
    (fun x ⇒ lim (pseries c x))
    (lim (pseries (pseries_diffs c) x)).

End PseriesDiff.

Section expR.
Variable R : realType.
Implicit Types x : R.

Lemma expR0 : expR 0 = 1 :> R.

Lemma expR_ge1Dx x : 0 ≤ x → 1 + x ≤ expR x.

Lemma exp_coeffE x : exp_coeff x = (fun n ⇒ (fun n ⇒ (n`!%:R)^-1) n × x ^+ n).

Import GRing.Theory.
Local Open Scope ring_scope.

Lemma expRE :
  expR = fun x ⇒ lim (pseries (fun n ⇒ (fun n ⇒ (n`!%:R)^-1) n) x).

Global Instance is_derive_expR x : is_derive x 1 expR (expR x).

Lemma derivable_expR x : derivable expR x 1.

Lemma continuous_expR : continuous (@expR R).

Lemma expRxDyMexpx x y : expR (x + y) × expR (- x) = expR y.

Lemma expRxMexpNx_1 x : expR x × expR (- x) = 1.

Lemma pexpR_gt1 x : 0 < x → 1 < expR x.

Lemma expR_gt0 x : 0 < expR x.

Lemma expRN x : expR (- x) = (expR x)^-1.

Lemma expRD x y : expR (x + y) = expR x × expR y.

Lemma expRMm n x : expR (n%:R × x) = expR x ^+ n.

Lemma expR_gt1 x: (1 < expR x) = (0 < x).

Lemma expR_lt1 x: (expR x < 1) = (x < 0).

Lemma expRB x y : expR (x - y) = expR x / expR y.

Lemma ltr_expR : {mono (@expR R) : x y / x < y}.

Lemma ler_expR : {mono (@expR R) : x y / x ≤ y}.

Lemma expR_inj : injective (@expR R).

Lemma expR_total_gt1 x :
  1 ≤ x → ∃ y, [/\ 0 ≤ y, 1 + y ≤ x & expR y = x].

Lemma expR_total x : 0 < x → ∃ y, expR y = x.

End expR.

Section Ln.
Variable R : realType.
Implicit Types x : R.

Notation exp := (@expR R).

Definition ln x : R := xget 0 [set y | exp y == x ].

Fact ln0 x : x ≤ 0 → ln x = 0.

Lemma expK : cancel exp ln.

Lemma lnK : {in Num.pos, cancel ln exp}.

Lemma lnK_eq x : (exp (ln x) == x) = (0 < x).

Lemma ln1 : ln 1 = 0.

Lemma lnM : {in Num.pos &, {morph ln : x y / x × y >-> x + y}}.

Lemma ln_inj : {in Num.pos &, injective ln}.

Lemma lnV : {in Num.pos, {morph ln : x / x ^-1 >-> - x}}.

Lemma ln_div : {in Num.pos &, {morph ln : x y / x / y >-> x - y}}.

Lemma ltr_ln : {in Num.pos &, {mono ln : x y / x < y}}.

Lemma ler_ln : {in Num.pos &, {mono ln : x y / x ≤ y}}.

Lemma lnX n x : 0 < x → ln(x ^+ n) = ln x *+ n.

Lemma le_ln1Dx x : 0 ≤ x → ln (1 + x) ≤ x.

Lemma ln_sublinear x : 0 < x → ln x < x.

Lemma ln_ge0 x : 1 ≤ x → 0 ≤ ln x.

Lemma ln_gt0 x : 1 < x → 0 < ln x.

Lemma continuous_ln x : 0 < x → {for x, continuous ln}.

Global Instance is_derive1_ln (x : R) : 0 < x → is_derive x 1 ln x^-1.

End Ln.

Section ExpFun.
Variable R : realType.
Implicit Types a x : R.

Definition exp_fun a x := expR (x × ln a).


Lemma exp_fun_gt0 a x : 0 < a `^ x.

Lemma exp_funr1 a : 0 < a → a `^ 1 = a.

Lemma exp_funr0 a : 0 < a → a `^ 0 = 1.

Lemma exp_fun1 : exp_fun 1 = fun⇒ 1.

Lemma ler_exp_fun a : 1 < a → {homo exp_fun a : x y / x ≤ y}.

Lemma exp_funD a : 0 < a → {morph exp_fun a : x y / x + y >-> x × y}.

Lemma exp_fun_inv a : 0 < a → a `^ (-1) = a ^-1.

Lemma exp_fun_mulrn a n : 0 < a → exp_fun a n%:R = a ^+ n.

End ExpFun.
Notation "a `^ x" := (exp_fun a x).

Section riemannR_series.
Variable R : realType.
Implicit Types a : R.
Local Open Scope ring_scope.

Definition riemannR a : R ^nat := fun n ⇒ (n.+1%:R `^ a)^-1.
Arguments riemannR a n /.

Lemma riemannR_gt0 a i : 0 < a → 0 < riemannR a i.

Lemma dvg_riemannR a : 0 < a ≤ 1 → ¬ cvg (series (riemannR a)).

End riemannR_series.