Top

Module mathcomp.analysis.exp

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.
Require Import signed topology normedtype landau sequences derive realfun.
Require Import itv convex.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
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 Extern 0 (is_true (@Num.norm _ _ _ \is Num.nneg)) =>
  solve [apply: 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) :
    cvgn (pseries f x) -> `|z| < `|x| ->
  cvgn (pseries (fun i => `|f i|) z).

Fact is_cvg_pseries_inside f (x z : R) :
  cvgn (pseries f x) -> `|z| < `|x| -> cvgn (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
  cvgn (pseries (pseries_diffs f) x) ->
  series s @ \oo --> limn (pseries (pseries_diffs f) x).

Lemma is_cvg_pseries_diffs_equiv f x :
    cvgn (pseries (pseries_diffs f) x) ->
  cvgn ([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 :
  cvgn (pseries c K) ->
  cvgn (pseries (pseries_diffs c) K) ->
  cvgn (pseries (pseries_diffs (pseries_diffs c)) K) ->
  `|x| < `|K| ->
  is_derive x (1 : R)
    (fun x => limn (pseries c x))
    (limn (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 => limn (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. Proof. by rewrite ltW// expR_gt0.
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 expRM_natl n x : expR (n%:R * x) = expR x ^+ n.

Lemma expRM_natr n x : expR (x * n%:R) = 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 -> exists y, [/\ 0 <= y, 1 + y <= x & expR y = x].

Lemma expR_total x : 0 < x -> exists 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.

#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `expRM_natl`")]
Notation expRMm := expRM_natl (only parsing).

Section expeR.
Context {R : realType}.
Implicit Types (x y : \bar R) (r s : R).

Local Open Scope ereal_scope.

Definition expeR x :=
  match x with | r%:E => (expR r)%:E | +oo => +oo | -oo => 0 end.

Lemma expeR0 : expeR 0 = 1. Proof. by rewrite /= expR0.
Lemma expeR_ge0 x : 0 <= expeR x.

Lemma expeR_gt0 x : -oo < x -> 0 < expeR x.

Lemma expeR_eq0 x : (expeR x == 0) = (x == -oo).

Lemma expeRD x y : expeR (x + y) = expeR x * expeR y.

Lemma expeR_ge1Dx x : 0 <= x -> 1 + x <= expeR x.

Lemma ltr_expeR : {mono expeR : x y / x < y}.

Lemma ler_expeR : {mono expeR : x y / x <= y}.

Lemma expeR_inj : injective expeR.

Lemma expeR_total x : 0 <= x -> exists y, expeR y = x.

End expeR.

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 lnXn 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_lt0 x : 0 < x < 1 -> ln x < 0.

Lemma ln_gt0 x : 1 < x -> 0 < ln x.

Lemma ln_le0 (x : R) : x <= 1 -> ln x <= 0.

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.

Local Open Scope convex_scope.
Lemma concave_ln (t : {i01 R}) (a b : R^o) : 0 < a -> 0 < b ->
  (ln a : R^o) <| t |> (ln b : R^o) <= ln (a <| t |> b).
Local Close Scope convex_scope.

End Ln.

Section PowR.
Variable R : realType.
Implicit Types a x y z r : R.

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

Local Notation "a `^ x" := (powR a x).

Lemma expRM x y : expR (x * y) = (expR x) `^ y.

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 ger_powR a : 0 < a <= 1 -> {homo powR a : x y /~ y <= x}.

Lemma ler_powR a : 1 <= a -> {homo powR a : x y / x <= y}.

Lemma powR_injective r : 0 < r -> {in Num.nneg &, injective (powR ^~ r)}.

Lemma ler1_powR a r : 1 <= a -> r <= 1 -> a >= a `^ r.

Lemma le1r_powR a r : 1 <= a -> 1 <= r -> a <= a `^ r.

Lemma ger1_powR a r : 0 < a <= 1 -> r <= 1 -> a <= a `^ r.

Lemma ge1r_powR a r : 0 < a <= 1 -> 1 <= r -> a >= a `^ r.

Lemma ge0_ler_powR r : 0 <= r ->
  {in Num.nneg &, {homo powR ^~ r : x y / x <= y >-> x <= y}}.

Lemma gt0_ltr_powR r : 0 < r ->
  {in Num.nneg &, {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 ge1r_powRZ x y r : 0 < x <= 1 -> 0 <= y -> 1 <= r ->
  (x * y) `^ r <= x * (y `^ r).

Lemma le1r_powRZ x y r : x >= 1 -> 0 <= y -> 1 <= r ->
  (x * y) `^ r >= x * (y `^ r).

Lemma powRrM x y z : 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 mulr_powRB1 x p : 0 <= x -> 0 < p -> x * x `^ (p - 1) = x `^ p.

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.

Lemma conjugate_powR a b p q : 0 <= a -> 0 <= b ->
  0 < p -> 0 < q -> p^-1 + q^-1 = 1 ->
  a * b <= a `^ p / p + b `^ q / q.

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

#[deprecated(since="mathcomp-analysis 0.6.5", note="renamed `ge0_ler_powR`")]
Notation gt0_ler_powR := ge0_ler_powR.

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.

Local Notation "x `^ r" := (poweR x r).

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 poweRN x r : x \is a fin_num -> x `^ (- r) = (fine x `^ r)^-1%:E.

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 poweR_lty x r : x < +oo -> x `^ r < +oo.

Lemma lty_poweRy x r : r != 0%R -> x `^ r < +oo -> x < +oo.

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

Lemma poweR1r r : 1 `^ r = 1. Proof. by rewrite poweR_EFin powR1.
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 gt0_ler_poweR r : (0 <= r)%R ->
  {in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}.

Lemma fin_num_poweR x r : x \is a fin_num -> x `^ r \is a fin_num.

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 -> ~ cvgn (series (riemannR a)).

End riemannR_series.