(* 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.classical Require Import boolp classical_sets functions.
From mathcomp.classical 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.

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 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) : a ≤ b →
  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 := 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 PowerPos.
Variable R : realType.
Implicit Types a x : R.

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


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

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

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

Lemma power_posr0 a : a `^ 0 = 1.

Lemma power_pos0 x : power_pos 0 x = (x == 0)%:R.

Lemma power_pos1 : power_pos 1 = fun⇒ 1.

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

Lemma ler_power_pos a : 1 < a → {homo power_pos a : x y / x ≤ y}.

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

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

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

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

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

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

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

Lemma ln_power_pos s r : s != 0 → ln (s `^ r) = r × ln s.

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

End PowerPos.
Notation "a `^ x" := (power_pos a x) : ring_scope.

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

Definition powere_pos 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 powere_pos_EFin (s : R) r : s%:E `^ r = (s `^ r)%:E.

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

Lemma powere_pose0 x : x `^ 0 = 1.

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

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

Lemma powere_pos0r r : 0 `^ r = (r == 0)%:R%:E.

Lemma powere_pos1r r : 1 `^ r = 1.

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

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

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

Lemma powere_pos_eq0 x r : -oo < x → x `^ r = 0 → x = 0.

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

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

End powere_pos.
Notation "a `^ x" := (powere_pos 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.