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.
# Theory of exponential/logarithm functions
This file defines exponential and logarithm functions and develops their
theory.
## Differentiability of series (Section PseriesDiff)
This formalization is inspired by HOL-Light (transc.ml). This part is
temporary: it should be subsumed by a proper theory of power series.
```
pseries f x == [series f n * x ^ n]_n
pseries_diffs f i == (i + 1) * f (i + 1)
expeR x == extended real number-valued exponential function
ln x == the natural logarithm
s `^ r == power function, in ring_scope (assumes s >= 0)
e `^ r == power function, in ereal_scope (assumes e >= 0)
riemannR a == sequence n |-> 1 / (n.+1) `^ a where a has a type
of type realType
e `^?(r +? s) == validity condition for the distributivity of
the power of the addition, in ereal_scope
```
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.
Proof.
#[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).
Proof.
Fact
is_cvg_pseries_inside
f
(
x
z
: R)
:
cvg (
pseries f x)
-> `|z| < `|x| -> cvg (
pseries f z).
Proof.
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).
Proof.
by apply/funext => i; rewrite /pseries_diffs /= -mulrN. Qed.
Lemma
pseries_diffs_inv_fact
:
pseries_diffs (
fun
n
=> (
n`!%:R)
^-1)
= (
fun
n
=> (
n`!%:R)
^-1 : R).
Proof.
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.
Proof.
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).
Proof.
Lemma
is_cvg_pseries_diffs_equiv
f
x
:
cvg (
pseries (
pseries_diffs f)
x)
-> cvg [series i%:R * f i * x ^+ i.
-1]_i.
Proof.
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)).
Proof.
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).
Proof.
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|.
Proof.
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)).
Proof.
End PseriesDiff.
Section
expR
.
Variable
R
: realType.
Implicit Types x : R.
Lemma
expR0
: expR 0 = 1 :> R.
Proof.
Lemma
expR_ge1Dx
x
: 0 <= x -> 1 + x <= expR x.
Proof.
Lemma
exp_coeffE
x
: exp_coeff x = (
fun
n
=> (
fun
n
=> (
n`!%:R)
^-1)
n * x ^+ n).
Proof.
by apply/funext => i; rewrite /exp_coeff /= mulrC. Qed.
Import GRing.Theory.
Local Open Scope ring_scope.
Lemma
expRE
:
expR = fun
x
=> lim (
pseries (
fun
n
=> (
fun
n
=> (
n`!%:R)
^-1)
n)
x).
Proof.
by apply/funext => x; rewrite /pseries -exp_coeffE. Qed.
Global Instance
is_derive_expR
x
: is_derive x 1 expR (
expR x).
Proof.
Lemma
derivable_expR
x
: derivable expR x 1.
Proof.
Lemma
derive_expR
: 'D_1 expR = expR :> (
R -> R).
Proof.
Lemma
continuous_expR
: continuous (
@expR R).
Proof.
by move=> x; exact/differentiable_continuous/derivable1_diffP/derivable_expR.
Qed.
Lemma
expRxDyMexpx
x
y
: expR (
x + y)
* expR (
- x)
= expR y.
Proof.
Lemma
expRxMexpNx_1
x
: expR x * expR (
- x)
= 1.
Proof.
Lemma
pexpR_gt1
x
: 0 < x -> 1 < expR x.
Proof.
Lemma
expR_gt0
x
: 0 < expR x.
Proof.
Lemma
expR_ge0
x
: 0 <= expR x
Proof.
Lemma
expR_eq0
x
: (
expR x == 0)
= false.
Proof.
by rewrite gt_eqF ?expR_gt0. Qed.
Lemma
expRN
x
: expR (
- x)
= (
expR x)
^-1.
Proof.
Lemma
expRD
x
y
: expR (
x + y)
= expR x * expR y.
Proof.
Lemma
expRMm
n
x
: expR (
n%:R * x)
= expR x ^+ n.
Proof.
Lemma
expR_gt1
x
: (
1 < expR x)
= (
0 < x).
Proof.
Lemma
expR_lt1
x
: (
expR x < 1)
= (
x < 0).
Proof.
Lemma
expRB
x
y
: expR (
x - y)
= expR x / expR y.
Proof.
Lemma
ltr_expR
: {mono (
@expR R)
:
x
y
/ x < y}.
Proof.
Lemma
ler_expR
: {mono (
@expR R)
:
x
y
/ x <= y}.
Proof.
Lemma
expR_inj
: injective (
@expR R).
Proof.
Lemma
expR_total_gt1
x
:
1 <= x -> exists
y,
[/\ 0 <= y, 1 + y <= x & expR y = x].
Proof.
Lemma
expR_total
x
: 0 < x -> exists
y,
expR y = x.
Proof.
case: (
lerP 1 x)
=> [/expR_total_gt1[y [_ _ Hy]]|x_lt1 x_gt0].
by exists y.
have /expR_total_gt1[y [H1y H2y H3y]] : 1 <= x^-1 by rewrite ltW // !invf_cp1.
by exists (
-y)
; rewrite expRN H3y invrK.
Qed.
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).
Proof.
Local Close Scope convex_scope.
End expR.
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. Qed.
Lemma
expeR_ge0
x
: 0 <= expeR x.
Proof.
Lemma
expeR_gt0
x
: -oo < x -> 0 < expeR x.
Proof.
Lemma
expeR_eq0
x
: (
expeR x == 0)
= (
x == -oo).
Proof.
by case: x => //= [r|]; rewrite ?eqxx// eqe expR_eq0. Qed.
Lemma
expeRD
x
y
: expeR (
x + y)
= expeR x * expeR y.
Proof.
Lemma
expeR_ge1Dx
x
: 0 <= x -> 1 + x <= expeR x.
Proof.
by case: x => //= r; rewrite -EFinD !lee_fin; exact: expR_ge1Dx. Qed.
Lemma
ltr_expeR
: {mono expeR :
x
y
/ x < y}.
Proof.
Lemma
ler_expeR
: {mono expeR :
x
y
/ x <= y}.
Proof.
Lemma
expeR_inj
: injective expeR.
Proof.
move=> [r| |] [s| |] => //=.
- by move=> [] /expR_inj ->.
- by case => /eqP; rewrite expR_eq0.
- by case => /esym/eqP; rewrite expR_eq0.
Qed.
Lemma
expeR_total
x
: 0 <= x -> exists
y,
expeR y = x.
Proof.
move: x => [r|_|//]; last by exists +oo.
rewrite le_eqVlt => /predU1P[<-|]; first by exists -oo.
by rewrite lte_fin => /expR_total[y <-]; exists y%:E.
Qed.
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.
Proof.
Lemma
expRK
: cancel exp ln.
Proof.
by move=> x; rewrite /ln; case: xgetP => [x1 _ /eqP/expR_inj //|/(
_ x)
[]/=].
Qed.
Lemma
lnK
: {in Num.pos, cancel ln exp}.
Proof.
move=> x; rewrite qualifE => x_gt0.
rewrite /ln; case: xgetP=> [x1 _ /eqP// |H].
by case: (
expR_total x_gt0)
=> y /eqP Hy; case: (
H y).
Qed.
Lemma
lnK_eq
x
: (
exp (
ln x)
== x)
= (
0 < x).
Proof.
Lemma
ln1
: ln 1 = 0.
Proof.
Lemma
lnM
: {in Num.pos &, {morph ln :
x
y
/ x * y >-> x + y}}.
Proof.
move=> x y x0 y0; apply: expR_inj; rewrite expRD !lnK//.
by move: x0 y0; rewrite !qualifE; exact: mulr_gt0.
Qed.
Lemma
ln_inj
: {in Num.pos &, injective ln}.
Proof.
by move=> x y /lnK {2}<- /lnK {2}<- ->. Qed.
Lemma
lnV
: {in Num.pos, {morph ln :
x
/ x ^-1 >-> - x}}.
Proof.
Lemma
ln_div
: {in Num.pos &, {morph ln :
x
y
/ x / y >-> x - y}}.
Proof.
move=> x y x0 y0; rewrite (
lnM x0)
?lnV//.
by move: y0; rewrite !qualifE/= invr_gt0.
Qed.
Lemma
ltr_ln
: {in Num.pos &, {mono ln :
x
y
/ x < y}}.
Proof.
by move=> x y x_gt0 y_gt0; rewrite -ltr_expR !lnK. Qed.
Lemma
ler_ln
: {in Num.pos &, {mono ln :
x
y
/ x <= y}}.
Proof.
by move=> x y x_gt0 y_gt0; rewrite -ler_expR !lnK. Qed.
Lemma
lnXn
n
x
: 0 < x -> ln (
x ^+ n)
= ln x *+ n.
Proof.
move=> x_gt0; elim: n => [|n ih] /=; first by rewrite expr0 ln1 mulr0n.
by rewrite !exprS lnM ?qualifE// ?exprn_gt0// mulrS ih.
Qed.
Lemma
le_ln1Dx
x
: 0 <= x -> ln (
1 + x)
<= x.
Proof.
Lemma
ln_sublinear
x
: 0 < x -> ln x < x.
Proof.
Lemma
ln_ge0
x
: 1 <= x -> 0 <= ln x.
Proof.
Lemma
ln_gt0
x
: 1 < x -> 0 < ln x.
Proof.
Lemma
ln_le0
(
x
: R)
: x <= 1 -> ln x <= 0.
Proof.
have [x0|x0 x1] := leP x 0; first by rewrite ln0.
by rewrite -ler_expR expR0 lnK.
Qed.
Lemma
continuous_ln
x
: 0 < x -> {for x, continuous ln}.
Proof.
Global Instance
is_derive1_ln
(
x
: R)
: 0 < x -> is_derive x 1 ln x^-1.
Proof.
move=> x_gt0; rewrite -[x]lnK//.
apply: (
@is_derive_inverse R expR)
; first by near=> z; apply: expRK.
by near=>z; apply: continuous_expR.
by rewrite lnK // lt0r_neq0.
Unshelve.
all: by end_near. Qed.
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).
Proof.
move=> a0 b0; have := convex_expR t (
ln a) (
ln b).
by rewrite !lnK// -(
@ler_ln)
?posrE ?expR_gt0 ?conv_gt0// expRK.
Qed.
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.
Proof.
Lemma
powR_ge0
a
x
: 0 <= a `^ x.
Proof.
Lemma
powR_gt0
a
x
: 0 < a -> 0 < a `^ x.
Proof.
Lemma
gt0_powR
a
x
: 0 < x -> 0 <= a -> 0 < a `^ x -> 0 < a.
Proof.
Lemma
powR0
x
: x != 0 -> 0 `^ x = 0.
Proof.
by move=> x0; rewrite /powR eqxx (
negbTE x0). Qed.
Lemma
powRr1
a
: 0 <= a -> a `^ 1 = a.
Proof.
Lemma
powRr0
a
: a `^ 0 = 1.
Proof.
Lemma
powR1
: powR 1 = fun=> 1.
Proof.
Lemma
powR_eq0
x
p
: (
x `^ p == 0)
= (
x == 0)
&& (
p != 0).
Proof.
Lemma
powR_eq0_eq0
x
p
: x `^ p = 0 -> x = 0.
Proof.
by move=> /eqP; rewrite powR_eq0 => /andP[/eqP]. Qed.
Lemma
ger_powR
a
: 0 < a <= 1 -> {homo powR a :
x
y
/~ y <= x}.
Proof.
Lemma
ler_powR
a
: 1 <= a -> {homo powR a :
x
y
/ x <= y}.
Proof.
Lemma
powR_injective
r
: 0 < r -> {in Num.nneg &, injective (
powR ^~ r)
}.
Proof.
Lemma
ler1_powR
a
r
: 1 <= a -> r <= 1 -> a >= a `^ r.
Proof.
Lemma
le1r_powR
a
r
: 1 <= a -> 1 <= r -> a <= a `^ r.
Proof.
Lemma
ger1_powR
a
r
: 0 < a <= 1 -> r <= 1 -> a <= a `^ r.
Proof.
Lemma
ge1r_powR
a
r
: 0 < a <= 1 -> 1 <= r -> a >= a `^ r.
Proof.
Lemma
ge0_ler_powR
r
: 0 <= r ->
{in Num.nneg &, {homo powR ^~ r :
x
y
/ x <= y >-> x <= y}}.
Proof.
rewrite le_eqVlt => /predU1P[<- x y _ _ _|]; first by rewrite !powRr0.
move=> a0 x y; rewrite 2!nnegrE !le_eqVlt => /predU1P[<-|x0].
move=> /predU1P[<- _|y0 _]; first by rewrite eqxx.
by rewrite !powR0 ?(
gt_eqF a0)
// powR_gt0 ?orbT.
move=> /predU1P[<-|y0]; first by rewrite gt_eqF//= ltNge (
ltW x0).
move=> /predU1P[->//|xy]; first by rewrite eqxx.
by apply/orP; right; rewrite /powR !gt_eqF// ltr_expR ltr_pmul2l// ltr_ln.
Qed.
Lemma
gt0_ltr_powR
r
: 0 < r ->
{in Num.nneg &, {homo powR ^~ r :
x
y
/ x < y >-> x < y}}.
Proof.
Lemma
powRM
x
y
r
: 0 <= x -> 0 <= y -> (
x * y)
`^ r = x `^ r * y `^ r.
Proof.
Lemma
ge1r_powRZ
x
y
r
: 0 < x <= 1 -> 0 <= y -> 1 <= r ->
(
x * y)
`^ r <= x * (
y `^ r).
Proof.
Lemma
le1r_powRZ
x
y
r
: x >= 1 -> 0 <= y -> 1 <= r ->
(
x * y)
`^ r >= x * (
y `^ r).
Proof.
Lemma
powRrM
x
y
z
: x `^ (
y * z)
= (
x `^ y)
`^ z.
Proof.
Lemma
powRAC
x
y
z
: (
x `^ y)
`^ z = (
x `^ z)
`^ y.
Proof.
by rewrite -!powRrM mulrC. Qed.
Lemma
powRD
x
r
s
: (
r + s == 0)
==> (
x != 0)
-> x `^ (
r + s)
= x `^ r * x `^ s.
Proof.
Lemma
mulr_powRB1
x
p
: 0 <= x -> 0 < p -> x * x `^ (
p - 1)
= x `^ p.
Proof.
Lemma
powRN
x
r
: x `^ (
- r)
= (
x `^ r)
^-1.
Proof.
Lemma
powRB
x
r
s
: (
r == s)
==> (
x != 0)
-> x `^ (
r - s)
= x `^ r / x `^ s.
Proof.
by move=> ?; rewrite powRD ?subr_eq0// powRN. Qed.
Lemma
powR_mulrn
a
n
: 0 <= a -> a `^ n%:R = a ^+ n.
Proof.
Lemma
powR_inv1
a
: 0 <= a -> a `^ (
-1)
= a ^-1.
Proof.
Lemma
powR_invn
a
n
: 0 <= a -> a `^ (
- n%:R)
= a ^- n.
Proof.
Lemma
powR_intmul
a
(
z
: int)
: 0 <= a -> a `^ z%:~R = a ^ z.
Proof.
Lemma
ln_powR
a
x
: ln (
a `^ x)
= x * ln a.
Proof.
Lemma
powR12_sqrt
a
: 0 <= a -> a `^ (
2^-1)
= Num.sqrt a.
Proof.
Lemma
norm_powR
a
x
: 0 <= a -> `|a `^ x| = `|a| `^ x.
Proof.
Lemma
lt0_norm_powR
a
x
: a < 0 -> `|a `^ x| = 1.
Proof.
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.
Proof.
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.
Proof.
by []. Qed.
Lemma
poweRyr
r
: r != 0%R -> +oo `^ r = +oo.
Proof.
by move/negbTE => /= ->. Qed.
Lemma
poweRe0
x
: x `^ 0 = 1.
Proof.
by move: x => [x'| |]/=; rewrite ?powRr0// eqxx. Qed.
Lemma
poweRe1
x
: 0 <= x -> x `^ 1 = x.
Proof.
by move: x => [x'| |]//= x0; rewrite ?powRr1// (
negbTE (
oner_neq0 _)).
Qed.
Lemma
poweRN
x
r
: x \is a fin_num -> x `^ (
- r)
= (
fine x `^ r)
^-1%:E.
Proof.
Lemma
poweRNyr
r
: r != 0%R -> -oo `^ r = 0.
Proof.
by move=> r0 /=; rewrite (
negbTE r0). Qed.
Lemma
poweR_eqy
x
r
: x `^ r = +oo -> x = +oo.
Proof.
by case: x => [x| |] //=; case: ifP. Qed.
Lemma
eqy_poweR
x
r
: (
0 < r)
%R -> x = +oo -> x `^ r = +oo.
Proof.
by move: x => [| |]//= r0 _; rewrite gt_eqF. Qed.
Lemma
poweR_lty
x
r
: x < +oo -> x `^ r < +oo.
Proof.
by move: x => [x| |]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry.
Qed.
Lemma
lty_poweRy
x
r
: r != 0%R -> x `^ r < +oo -> x < +oo.
Proof.
by move=> r0; move: x => [x| | _]//=; rewrite ?ltry// (
negbTE r0).
Qed.
Lemma
poweR0r
r
: r != 0%R -> 0 `^ r = 0.
Proof.
Lemma
poweR1r
r
: 1 `^ r = 1
Proof.
Lemma
fine_poweR
x
r
: fine (
x `^ r)
= ((
fine x)
`^ r)
%R.
Proof.
by move: x => [x| |]//=; case: ifPn => [/eqP ->|?]; rewrite ?powRr0 ?powR0.
Qed.
Lemma
poweR_ge0
x
r
: 0 <= x `^ r.
Proof.
by move: x => [x| |]/=; rewrite ?lee_fin ?powR_ge0//; case: ifPn. Qed.
Lemma
poweR_gt0
x
r
: 0 < x -> 0 < x `^ r.
Proof.
Lemma
gt0_poweR
x
r
: (
0 < r)
%R -> 0 <= x -> 0 < x `^ r -> 0 < x.
Proof.
move=> r0; move: x => [x|//|]; rewrite ?leeNe_eq// lee_fin !lte_fin.
exact: gt0_powR.
Qed.
Lemma
poweR_eq0
x
r
: 0 <= x -> (
x `^ r == 0)
= ((
x == 0)
&& (
r != 0%R)).
Proof.
Lemma
poweR_eq0_eq0
x
r
: 0 <= x -> x `^ r = 0 -> x = 0.
Proof.
by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed.
Lemma
gt0_ler_poweR
r
: (
0 <= r)
%R ->
{in `[0, +oo] &, {homo poweR ^~ r :
x
y
/ x <= y >-> x <= y}}.
Proof.
move=> r0 + y; case=> //= [x /[1!in_itv]/= /andP[xint _]| _ _].
- case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _].
+ by rewrite !lee_fin ge0_ler_powR.
+ by case: eqP => [->|]; rewrite ?powRr0 ?leey.
- by rewrite leye_eq => /eqP ->.
Qed.
Lemma
fin_num_poweR
x
r
: x \is a fin_num -> x `^ r \is a fin_num.
Proof.
Lemma
poweRM
x
y
r
: 0 <= x -> 0 <= y -> (
x * y)
`^ r = x `^ r * y `^ r.
Proof.
Lemma
poweRrM
x
r
s
: x `^ (
r * s)
= (
x `^ r)
`^ s.
Proof.
Lemma
poweRAC
x
r
s
: (
x `^ r)
`^ s = (
x `^ s)
`^ r.
Proof.
by rewrite -!poweRrM mulrC. Qed.
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)))).
Proof.
by []. Qed.
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)))).
Proof.
Lemma
add_neq0_poweRD_def
x
r
s
: (
r + s != 0)
%R -> x `^?(
r +? s).
Proof.
Lemma
add_neq0_poweRB_def
x
r
s
: (
r != s)
%R -> x `^?(
r +? - s).
Proof.
Lemma
nneg_neq0_poweRD_def
x
r
s
: x != 0 -> (
r >= 0)
%R -> (
s >= 0)
%R ->
x `^?(
r +? s).
Proof.
move=> xN0 rge0 sge0; rewrite /poweRD_def xN0/=.
by case: ltgtP rge0 => // [r_gt0|<-]; case: ltgtP sge0 => // [s_gt0|<-]//=;
rewrite ?addr0 ?add0r ?implybT// gt_eqF//= ?addr_gt0.
Qed.
Lemma
nneg_neq0_poweRB_def
x
r
s
: x != 0 -> (
r >= 0)
%R -> (
s <= 0)
%R ->
x `^?(
r +? - s).
Proof.
Lemma
poweRD
x
r
s
: x `^?(
r +? s)
-> x `^ (
r + s)
= x `^ r * x `^ s.
Proof.
Lemma
poweRB
x
r
s
: x `^?(
r +? - s)
-> x `^ (
r - s)
= x `^ r * x `^ (
- s).
Proof.
by move=> rs; rewrite poweRD. Qed.
Lemma
poweR12_sqrt
x
: 0 <= x -> x `^ 2^-1 = sqrte x.
Proof.
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.
Proof.
Lemma
dvg_riemannR
a
: 0 <= a <= 1 -> ~ cvg (
series (
riemannR a)).
Proof.
End riemannR_series.