(* 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.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import mathcomp_extra.
Require Import reals ereal nsatz_realtype.
Require Import signed topology normedtype landau sequences derive realfun.
Require Import itv convex.

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.

Reserved Notation "x '`^?' ( r +? s )"
 (format "x '`^?' ( r +? s )", r at next level, at level 11) .

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 derive_expR : 'D_1 expR = expR :> (R → R).

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 expR_ge0 x : 0 ≤ expR x.

Lemma expR_eq0 x : (expR x == 0) = false.

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.

Local Open Scope convex_scope.
Lemma convex_expR (t : {i01 R}) (a b : R^o) :
  expR (a <| t |> b) ≤ (expR a : R^o) <| t |> (expR b : R^o).
Local Close Scope convex_scope.

End expR.

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

Notation exp := (@expR R).

Definition ln x : R := [get y | exp y == x ].

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

Lemma expRK : 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 PowR.
Variable R : realType.
Implicit Types a x : R.

Definition powR a x := if a == 0 then (x == 0)%:R else expR (x × ln a).


Lemma powR_ge0 a x : 0 ≤ a `^ x.

Lemma powR_gt0 a x : 0 < a → 0 < a `^ x.

Lemma gt0_powR a x : 0 < x → 0 ≤ a → 0 < a `^ x → 0 < a.

Lemma powR0 x : x != 0 → 0 `^ x = 0.

Lemma powRr1 a : 0 ≤ a → a `^ 1 = a.

Lemma powRr0 a : a `^ 0 = 1.

Lemma powR1 : powR 1 = fun⇒ 1.

Lemma powR_eq0 x p : (x `^ p == 0) = (x == 0) && (p != 0).

Lemma powR_eq0_eq0 x p : x `^ p = 0 → x = 0.

Lemma ler_powR a : 1 ≤ a → {homo powR a : x y / x ≤ y}.

Lemma gt0_ler_powR (r : R) : 0 ≤ r →
  {in `[0, +oo[ &, {homo powR ^~ r : x y / x ≤ y >-> x ≤ y}}.

Lemma powRM x y r : 0 ≤ x → 0 ≤ y → (x × y) `^ r = x `^ r × y `^ r.

Lemma powRrM (x y z : R) : x `^ (y × z) = (x `^ y) `^ z.

Lemma powRAC x y z : (x `^ y) `^ z = (x `^ z) `^ y.

Lemma powRD x r s : (r + s == 0) ==> (x != 0) → x `^ (r + s) = x `^ r × x `^ s.

Lemma powRN x r : x `^ (- r) = (x `^ r)^-1.

Lemma powRB x r s : (r == s) ==> (x != 0) → x `^ (r - s) = x `^ r / x `^ s.

Lemma powR_mulrn a n : 0 ≤ a → a `^ n%:R = a ^+ n.

Lemma powR_inv1 a : 0 ≤ a → a `^ (-1) = a ^-1.

Lemma powR_invn a n : 0 ≤ a → a `^ (- n%:R) = a ^- n.

Lemma powR_intmul a (z : int) : 0 ≤ a → a `^ z%:~R = a ^ z.

Lemma ln_powR a x : ln (a `^ x) = x × ln a.

Lemma powR12_sqrt a : 0 ≤ a → a `^ (2^-1) = Num.sqrt a.

Lemma norm_powR a x : 0 ≤ a → `|a `^ x| = `|a| `^ x.

Lemma lt0_norm_powR a x : a < 0 → `|a `^ x| = 1.

End PowR.
Notation "a `^ x" := (powR a x) : ring_scope.

Section poweR.
Local Open Scope ereal_scope.
Context {R : realType}.
Implicit Types (s r : R) (x y : \bar R).

Definition poweR x r :=
  match x with
  | x'%:E ⇒ (x' `^ r)%:E
  | +oo ⇒ if r == 0%R then 1%E else +oo
  | -oo ⇒ if r == 0%R then 1%E else 0%E
  end.


Lemma poweR_EFin s r : s%:E `^ r = (s `^ r)%:E.

Lemma poweRyr r : r != 0%R → +oo `^ r = +oo.

Lemma poweRe0 x : x `^ 0 = 1.

Lemma poweRe1 x : 0 ≤ x → x `^ 1 = x.

Lemma poweRNyr r : r != 0%R → -oo `^ r = 0.

Lemma poweR_eqy x r : x `^ r = +oo → x = +oo.

Lemma eqy_poweR x r : (0 < r)%R → x = +oo → x `^ r = +oo.

Lemma poweR0r r : r != 0%R → 0 `^ r = 0.

Lemma poweR1r r : 1 `^ r = 1.

Lemma fine_poweR x r : fine (x `^ r) = ((fine x) `^ r)%R.

Lemma poweR_ge0 x r : 0 ≤ x `^ r.

Lemma poweR_gt0 x r : 0 < x → 0 < x `^ r.

Lemma gt0_poweR x r : (0 < r)%R → 0 ≤ x → 0 < x `^ r → 0 < x.

Lemma poweR_eq0 x r : 0 ≤ x → (x `^ r == 0) = ((x == 0) && (r != 0%R)).

Lemma poweR_eq0_eq0 x r : 0 ≤ x → x `^ r = 0 → x = 0.

Lemma poweRM x y r : 0 ≤ x → 0 ≤ y → (x × y) `^ r = x `^ r × y `^ r.

Lemma poweRrM x r s : x `^ (r × s) = (x `^ r) `^ s.

Lemma poweRAC x r s : (x `^ r) `^ s = (x `^ s) `^ r.

Definition poweRD_def x r s := ((r + s == 0)%R ==>
  ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).
Notation "x '`^?' ( r +? s )" := (poweRD_def x r s) : ereal_scope.

Lemma poweRD_defE x r s :
  x `^?(r +? s) = ((r + s == 0)%R ==>
  ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).

Lemma poweRB_defE x r s :
  x `^?(r +? - s) = ((r == s)%R ==>
  ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).

Lemma add_neq0_poweRD_def x r s : (r + s != 0)%R → x `^?(r +? s).

Lemma add_neq0_poweRB_def x r s : (r != s)%R → x `^?(r +? - s).

Lemma nneg_neq0_poweRD_def x r s : x != 0 → (r ≥ 0)%R → (s ≥ 0)%R →
  x `^?(r +? s).

Lemma nneg_neq0_poweRB_def x r s : x != 0 → (r ≥ 0)%R → (s ≤ 0)%R →
  x `^?(r +? - s).

Lemma poweRD x r s : x `^?(r +? s) → x `^ (r + s) = x `^ r × x `^ s.

Lemma poweRB x r s : x `^?(r +? - s) → x `^ (r - s) = x `^ r × x `^ (- s).

Lemma poweR12_sqrt x : 0 ≤ x → x `^ 2^-1 = sqrte x.

End poweR.
Notation "a `^ x" := (poweR a x) : ereal_scope.

Section riemannR_series.
Variable R : realType.
Implicit Types a : R.
Local Open Scope real_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.