# An axiomatization of real numbers $\mathbb{R}$
This file provides a classical axiomatization of real numbers as a
discrete real archimedean field with in particular a theory of floor and
ceil.
```
realType == type of real numbers
sup A == where A : set R with R : realType, the supremum of A when
it exists, 0 otherwise
inf A := - sup (- A)
```
The mixin corresponding to realType extends an archiFieldType with two
properties:
- when sup A exists, it is an upper bound of A (lemma sup_upper_bound)
- when sup A exists, there exists an element x in A such that
sup A - eps < x for any 0 < eps (lemma sup_adherent)
```
Rint == the set of real numbers that can be written as z%:~R,
i.e., as an integer
Rtoint r == r when r is an integer, 0 otherwise
floor_set x := [set y | Rtoint y /\ y <= x]
Rfloor x == the floor of x as a real number
floor x == the floor of x as an integer (type int)
range1 x := [set y |x <= y < x + 1]
Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x)
ceil x := - floor (- x)
```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
Require Import Setoid.
Declare Scope real_scope.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Unset SsrOldRewriteGoalsOrder.
Import Order.TTheory Order.Syntax GRing.Theory Num.Def Num.Theory.
Delimit Scope real_scope with real.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Section
subr_image
.
Variable
R
: numDomainType.
Implicit Types (
E : set R) (
x : R).
Lemma
has_ub_lbN
E
: has_ubound E <-> has_lbound (
-%R @` E).
Proof.
Lemma
has_lbound0
: has_lbound (
@set0 R)
Proof.
by exists 0. Qed.
Lemma
has_ubound0
: has_ubound (
@set0 R)
Proof.
by exists 0. Qed.
Lemma
ubound0
: ubound (
@set0 R)
= setT.
Proof.
by rewrite predeqE => r; split => // _. Qed.
Lemma
lboundT
: lbound [set: R] = set0.
Proof.
End subr_image.
Section
has_bound_lemmas
.
Variable
R
: realDomainType.
Implicit Types E : set R.
Implicit Types x : R.
Lemma
has_ub_image_norm
E
: has_ubound (
normr @` E)
-> has_ubound E.
Proof.
case => M /ubP uM; exists `|M|; apply/ubP => r rS.
rewrite (
le_trans (
real_ler_norm _))
?num_real //.
rewrite (
le_trans (
uM _ _))
?real_ler_norm ?num_real //.
by exists r.
Qed.
Lemma
has_inf_supN
E
: has_sup (
-%R @` E)
<-> has_inf E.
Proof.
split=> [ [NEn0 [x /ub_lbN xubE]] | [En0 [x /lb_ubN xlbe]] ].
by split; [apply/nonemptyN|rewrite -[E]setNK; exists (
- x)
].
by split; [apply/nonemptyN|exists (
- x)
].
Qed.
Lemma
has_supPn
{E} : E !=set0 ->
~ has_sup E <-> (
forall
x,
exists2
y,
E y & x < y).
Proof.
move=> nzE; split=> [/asboolPn|/has_ubPn h [_]] //.
by rewrite asbool_and (
asboolT nzE)
/= => /asboolP/has_ubPn.
Qed.
End has_bound_lemmas.
Module
Real
.
Section
Mixin
.
Variable (
R
: archiFieldType).
Record
mixin_of
: Type := Mixin {
_ :
forall
E
: set (
Num.ArchimedeanField.sort R)
,
has_sup E -> ubound E (
supremum 0 E)
;
_ :
forall (
E
: set (
Num.ArchimedeanField.sort R)) (
eps
: R)
, 0 < eps ->
has_sup E -> exists2
e
: R, E e & (
supremum 0 E - eps)
< e ;
}.
End Mixin.
Definition
EtaMixin
R
sup_upper_bound
sup_adherent
:=
let _ := @Mixin R sup_upper_bound sup_adherent in
@Mixin (
Num.ArchimedeanField.Pack (
Num.ArchimedeanField.class R))
sup_upper_bound sup_adherent.
Section
ClassDef
.
Record
class_of
(
R
: Type)
: Type := Class {
base
: Num.ArchimedeanField.class_of R;
mixin_rcf
: Num.real_closed_axiom (
Num.NumDomain.Pack base)
;
mixin
: mixin_of (
Num.ArchimedeanField.Pack base)
}.
Local Coercion base : class_of >-> Num.ArchimedeanField.class_of.
Local Coercion
base_rcf
R
(
c
: class_of R)
: Num.RealClosedField.class_of R :=
@Num.
RealClosedField.Class _ c (
@mixin_rcf _ c).
Structure
type
:= Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (
T
: Type) (
cT
: type).
Definition
class
:= let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition
clone
c
of phant_id class c := @Pack T c T.
Let
xT
:= let: Pack T _ _ := cT in T.
Notation
xclass
:= (
class : class_of xT).
Definition
rcf_axiom
{R} (
cR
: Num.RealClosedField.class_of R)
:
Num.real_closed_axiom (
Num.NumDomain.Pack cR)
:=
match cR with Num.RealClosedField.Class _ ax => ax end.
Coercion rcf_axiom : Num.RealClosedField.class_of >-> Num.real_closed_axiom.
Definition
pack
b0
(
m0
: mixin_of (
@Num.
ArchimedeanField.Pack T b0))
:=
fun
bT
b
& phant_id (
Num.ArchimedeanField.class bT)
b =>
fun (
bTr
: rcfType) (
br
: Num.RealClosedField.class_of bTr)
&
phant_id (
Num.RealClosedField.class bTr)
br =>
fun
cra
& phant_id (
@rcf_axiom bTr br)
cra =>
fun
m
& phant_id m0 m => Pack (
@Class T b cra m)
T.
Definition
eqType
:= @Equality.
Pack cT xclass.
Definition
choiceType
:= @Choice.
Pack cT xclass.
Definition
porderType
:= @Order.
POrder.Pack ring_display cT xclass.
Definition
latticeType
:= @Order.
Lattice.Pack ring_display cT xclass.
Definition
distrLatticeType
:= @Order.
DistrLattice.Pack ring_display cT xclass.
Definition
orderType
:= @Order.
Total.Pack ring_display cT xclass.
Definition
zmodType
:= @GRing.
Zmodule.Pack cT xclass.
Definition
ringType
:= @GRing.
Ring.Pack cT xclass.
Definition
comRingType
:= @GRing.
ComRing.Pack cT xclass.
Definition
unitRingType
:= @GRing.
UnitRing.Pack cT xclass.
Definition
comUnitRingType
:= @GRing.
ComUnitRing.Pack cT xclass.
Definition
idomainType
:= @GRing.
IntegralDomain.Pack cT xclass.
Definition
numDomainType
:= @Num.
NumDomain.Pack cT xclass.
Definition
normedZmodType
:= NormedZmodType numDomainType cT xclass.
Definition
fieldType
:= @GRing.
Field.Pack cT xclass.
Definition
realDomainType
:= @Num.
RealDomain.Pack cT xclass.
Definition
numFieldType
:= @Num.
NumField.Pack cT xclass.
Definition
realFieldType
:= @Num.
RealField.Pack cT xclass.
Definition
archimedeanFieldType
:= @Num.
ArchimedeanField.Pack cT xclass.
Definition
rcfType
:= @Num.
RealClosedField.Pack cT xclass.
Definition
join_rcfType
:= @Num.
RealClosedField.Pack archimedeanFieldType xclass.
End ClassDef.
Module
Exports
.
Coercion base : class_of >-> Num.ArchimedeanField.class_of.
Coercion base_rcf : class_of >-> Num.RealClosedField.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion porderType : type >-> Order.POrder.type.
Canonical porderType.
Coercion latticeType : type >-> Order.Lattice.type.
Canonical latticeType.
Coercion distrLatticeType : type >-> Order.DistrLattice.type.
Canonical distrLatticeType.
Coercion orderType : type >-> Order.Total.type.
Canonical orderType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> Num.NumDomain.type.
Canonical numDomainType.
Coercion normedZmodType : type >-> Num.NormedZmodule.type.
Canonical normedZmodType.
Coercion realDomainType : type >-> Num.RealDomain.type.
Canonical realDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion numFieldType : type >-> Num.NumField.type.
Canonical numFieldType.
Coercion realFieldType : type >-> Num.RealField.type.
Canonical realFieldType.
Coercion archimedeanFieldType : type >-> Num.ArchimedeanField.type.
Canonical archimedeanFieldType.
Coercion rcfType : type >-> Num.RealClosedField.type.
Canonical rcfType.
Canonical join_rcfType.
Notation
realType
:= type.
Notation
RealType
T m := (
@pack T _ m _ _ id _ _ id _ id _ id).
Notation
RealMixin
:= EtaMixin.
Notation
"[ 'realType' 'of' T 'for' cT ]"
:= (
@clone T cT _ idfun)
(
at level 0, format "[ 'realType' 'of' T 'for' cT ]")
: form_scope.
Notation
"[ 'realType' 'of' T ]"
:= (
@clone T _ _ id)
(
at level 0, format "[ 'realType' 'of' T ]")
: form_scope.
End Exports.
End Real.
Export Real.Exports.
Definition
sup
{R : realType} := @supremum _ R 0.
Definition
inf
{R : realType} (
E
: set R)
:= - sup (
-%R @` E).
Lemma
sup_upper_bound
{R : realType} (
E
: set R)
:
has_sup E -> ubound E (
sup E).
Proof.
by move=> supE; case: R E supE=> ? [? ? []]. Qed.
Lemma
sup_adherent
{R : realType} (
E
: set R) (
eps
: R)
: 0 < eps ->
has_sup E -> exists2
e
: R, E e & (
sup E - eps)
< e.
Proof.
by case: R E eps=> ? [? ? []]. Qed.
Section
IsInt
.
Context {R : realFieldType}.
Definition
Rint
:= [qualify a
x
: R | `[< exists
z,
x == z%:~R >]].
Fact
Rint_key
: pred_key Rint
Proof.
by []. Qed.
Canonical
Rint_keyed
:= KeyedQualifier Rint_key.
Lemma
Rint_def
x
: (
x \is a Rint)
= (
`[< exists
z,
x == z%:~R >]).
Proof.
by []. Qed.
Lemma
RintP
x
: reflect (
exists
z,
x = z%:~R) (
x \in Rint).
Proof.
by apply/(
iffP idP)
=> [/asboolP[z /eqP]|[z]] ->; [|apply/asboolP]; exists z.
Qed.
Lemma
RintC
z
: z%:~R \is a Rint.
Proof.
by apply/RintP; exists z. Qed.
Lemma
Rint0
: 0 \is a Rint.
Proof.
Lemma
Rint1
: 1 \is a Rint.
Proof.
by rewrite -[1]mulr1z RintC. Qed.
Hint Resolve Rint0 Rint1 RintC : core.
Lemma
Rint_subring_closed
: subring_closed Rint.
Proof.
split=> // _ _ /RintP[x ->] /RintP[y ->]; apply/RintP.
by exists (
x - y)
; rewrite rmorphB.
by exists (
x * y)
; rewrite rmorphM.
Qed.
Canonical
Rint_opprPred
:= OpprPred Rint_subring_closed.
Canonical
Rint_addrPred
:= AddrPred Rint_subring_closed.
Canonical
Rint_mulrPred
:= MulrPred Rint_subring_closed.
Canonical
Rint_zmodPred
:= ZmodPred Rint_subring_closed.
Canonical
Rint_semiringPred
:= SemiringPred Rint_subring_closed.
Canonical
Rint_smulrPred
:= SmulrPred Rint_subring_closed.
Canonical
Rint_subringPred
:= SubringPred Rint_subring_closed.
Lemma
Rint_ler_addr1
(
x
y
: R)
: x \is a Rint -> y \is a Rint ->
(
x + 1 <= y)
= (
x < y).
Proof.
Lemma
Rint_ltr_addr1
(
x
y
: R)
: x \is a Rint -> y \is a Rint ->
(
x < y + 1)
= (
x <= y).
Proof.
End IsInt.
Section
ToInt
.
Context {R : realType}.
Implicit Types x y : R.
Definition
Rtoint
(
x
: R)
: int :=
if insub x : {?
x
| x \is a Rint} is Some Px then
xchoose (
asboolP _ (
tagged Px))
else 0.
Lemma
RtointK
(
x
: R)
: x \is a Rint -> (
Rtoint x)
%:~R = x.
Proof.
Lemma
Rtointz
(
z
: int)
: Rtoint z%:~R = z.
Proof.
by apply/eqP; rewrite -(
@eqr_int R)
RtointK ?rpred_int. Qed.
Lemma
Rtointn
(
n
: nat)
: Rtoint n%:R = n%:~R.
Proof.
by rewrite -{1}mulrz_nat Rtointz. Qed.
Lemma
inj_Rtoint
: {in Rint &, injective Rtoint}.
Proof.
by move=> x y Ix Iy /= /(
congr1 (
@intmul R 1))
; rewrite !RtointK. Qed.
Lemma
RtointN
x
: x \is a Rint -> Rtoint (
- x)
= - Rtoint x.
Proof.
End ToInt.
Section
RealDerivedOps
.
Variable
R
: realType.
Implicit Types x y : R.
Definition
floor_set
x
:= [set
y
: R | (
y \is a Rint)
&& (
y <= x)
].
Definition
Rfloor
x
: R := sup (
floor_set x).
Definition
floor
x
: int := Rtoint (
Rfloor x).
Definition
range1
(
x
: R)
:= [set
y
| x <= y < x + 1].
Definition
Rceil
x
:= - Rfloor (
- x).
Definition
ceil
x
:= - floor (
- x).
End RealDerivedOps.
Section
RealLemmas
.
Variables (
R
: realType).
Implicit Types E : set R.
Implicit Types x : R.
Lemma
sup_out
E
: ~ has_sup E -> sup E = 0
Proof.
Lemma
sup0
: sup (
@set0 R)
= 0
Proof.
Lemma
sup1
x
: sup [set x] = x
Proof.
Lemma
sup_ub
{E} : has_ubound E -> ubound E (
sup E).
Proof.
move=> ubE; apply/ubP=> x x_in_E; move: (x) (x_in_E).
by apply/ubP/sup_upper_bound=> //; split; first by exists x.
Qed.
Lemma
sup_ub_strict
E
: has_ubound E ->
~ E (
sup E)
-> E `<=` [set
r
| r < sup E].
Proof.
move=> ubE EsupE r Er; rewrite /mkset lt_neqAle sup_ub // andbT.
by apply/negP => /eqP supEr; move: EsupE; rewrite -supEr.
Qed.
Lemma
sup_total
{E}
x
: has_sup E -> down E x \/ sup E <= x.
Proof.
move=> has_supE; rewrite orC.
case: (
lerP (
sup E)
x)
=> hx /=; [by left|right].
have /sup_adherent/(
_ has_supE)
: 0 < sup E - x by rewrite subr_gt0.
case=> e Ee hlte; apply/downP; exists e => //; move: hlte.
by rewrite opprB addrCA subrr addr0 => /ltW.
Qed.
Lemma
sup_le_ub
{E}
x
: E !=set0 -> (
ubound E)
x -> sup E <= x.
Proof.
move=> hasE leEx; set y := sup E; pose z := (
x + y)
/ 2%:R.
have Dz: 2%:R * z = x + y.
by rewrite mulrCA divff ?mulr1 // pnatr_eq0.
have ubE : has_sup E by split => //; exists x.
have [/downP [t Et lezt] | leyz] := sup_total z ubE.
rewrite -(
ler_add2l x)
-Dz -mulr2n -[leRHS]mulr_natl.
rewrite ler_pmul2l ?ltr0Sn //; apply/(
le_trans lezt).
by move/ubP : leEx; exact.
rewrite -(
ler_add2r y)
-Dz -mulr2n -[leLHS]mulr_natl.
by rewrite ler_pmul2l ?ltr0Sn.
Qed.
Lemma
sup_setU
(
A
B
: set R)
: has_sup B ->
(
forall
a
b,
A a -> B b -> a <= b)
-> sup (
A `|` B)
= sup B.
Proof.
move=> [B0 [l Bl]] AB; apply/eqP; rewrite eq_le; apply/andP; split.
- apply sup_le_ub => [|x [Ax|]]; first by apply: subset_nonempty B0 => ?; right.
by case: B0 => b Bb; rewrite (
le_trans (
AB _ _ Ax Bb))
// sup_ub //; exists l.
- by move=> Bx; rewrite sup_ub //; exists l.
- apply sup_le_ub => // b Bb; apply sup_ub; last by right.
by exists l => x [Ax|Bx]; [rewrite (
le_trans (
AB _ _ Ax Bb))
// Bl|exact: Bl].
Qed.
Lemma
sup_gt
(
S
: set R) (
x
: R)
: S !=set0 ->
(
x < sup S -> exists2
y,
S y & x < y)
%R.
Proof.
move=> S0; rewrite not_exists2P => + g; apply/negP; rewrite -leNgt.
by apply sup_le_ub => // y Sy; move: (
g y)
=> -[// | /negP]; rewrite leNgt.
Qed.
End RealLemmas.
Section
sup_sum
.
Context {R : realType}.
Lemma
sup_sumE
(
A
B
: set R)
:
has_sup A -> has_sup B -> sup [set x + y |
x
in A &
y
in B] = sup A + sup B.
Proof.
move=> /[dup] supA [[a Aa] ubA] /[dup] supB [[b Bb] ubB].
have ABsup : has_sup [set x + y |
x
in A &
y
in B].
split; first by exists (
a + b)
, a => //; exists b.
case: ubA ubB => p up [q uq]; exists (
p + q)
=> ? [r Ar [s Bs] <-].
by apply: ler_add; [exact: up | exact: uq].
apply: le_anti; apply/andP; split.
apply: sup_le_ub; first by case: ABsup.
by move=> ? [p Ap [q Bq] <-]; apply: ler_add; exact: sup_ub.
rewrite real_leNgt ?num_real// -subr_gt0; apply/negP.
set eps := (
_ + _ - _)
=> epos.
have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n.
have [r Ar supBr] := sup_adherent e2pos supA.
have [s Bs supAs] := sup_adherent e2pos supB.
have := ltr_add supBr supAs.
rewrite -addrA [-_+_]addrC -addrA -opprD -splitr addrA /= opprD opprK addrA.
rewrite subrr add0r; apply/negP; rewrite -real_leNgt ?num_real//.
by apply: sup_upper_bound => //; exists r => //; exists s.
Qed.
Lemma
inf_sumE
(
A
B
: set R)
:
has_inf A -> has_inf B -> inf [set x + y |
x
in A &
y
in B] = inf A + inf B.
Proof.
move/has_inf_supN => ? /has_inf_supN ?; rewrite /inf.
rewrite [X in - sup X = _](
_ : _ =
[set x + y |
x
in [set - x |
x
in A ] &
y
in [set - x |
x
in B]]).
rewrite eqEsubset; split => /= t [] /= x []a Aa.
case => b Bb <- <-; exists (
- a)
; first by exists a.
by exists (
- b)
; [exists b|rewrite opprD].
move=> <- [y] [b Bb] <- <-; exists (
a + b)
; last by rewrite opprD.
by exists a => //; exists b.
by rewrite sup_sumE // -opprD.
Qed.
End sup_sum.
Section
InfTheory
.
Variables (
R
: realType).
Implicit Types E : set R.
Implicit Types x : R.
Lemma
inf_lower_bound
E
: has_inf E -> lbound E (
inf E).
Proof.
move=> /has_inf_supN /sup_upper_bound /ubP inflb; apply/lbP => x.
by rewrite memNE => /inflb; rewrite ler_oppl.
Qed.
Lemma
inf_adherent
E
(
eps
: R)
: 0 < eps ->
has_inf E -> exists2
e,
E e & e < inf E + eps.
Proof.
move=> + /has_inf_supN supNE => /sup_adherent /(
_ supNE)
[e NEx egtsup].
exists (
- e)
; first by case: NEx => x Ex <-{}; rewrite opprK.
by rewrite ltr_oppl -mulN1r mulrDr !mulN1r opprK.
Qed.
Lemma
inf_out
E
: ~ has_inf E -> inf E = 0.
Proof.
move=> ninfE; rewrite -oppr0 -(
@sup_out _ (
-%R @` E))
=> // supNE; apply: ninfE.
exact/has_inf_supN.
Qed.
Lemma
inf0
: inf (
@set0 R)
= 0.
Proof.
Lemma
inf1
x
: inf [set x] = x.
Proof.
Lemma
inf_lb
E
: has_lbound E -> lbound E (
inf E).
Proof.
by move/has_lb_ubN/sup_ub/ub_lbN; rewrite setNK. Qed.
Lemma
inf_lb_strict
E
: has_lbound E ->
~ E (
inf E)
-> E `<=` [set
r
| inf E < r].
Proof.
move=> lE EinfE r Er; rewrite /mkset lt_neqAle inf_lb // andbT.
by apply/negP => /eqP infEr; move: EinfE; rewrite infEr.
Qed.
Lemma
lb_le_inf
E
x
: nonempty E -> (
lbound E)
x -> x <= inf E.
Proof.
Lemma
has_infPn
E
: nonempty E ->
~ has_inf E <-> (
forall
x,
exists2
y,
E y & y < x).
Proof.
move=> nzE; split=> [/asboolPn|/has_lbPn h [_] //].
by rewrite asbool_and (
asboolT nzE)
/= => /asboolP/has_lbPn.
Qed.
Lemma
inf_setU
(
A
B
: set R)
: has_inf A ->
(
forall
a
b,
A a -> B b -> a <= b)
-> inf (
A `|` B)
= inf A.
Proof.
Lemma
inf_lt
(
S
: set R) (
x
: R)
: S !=set0 ->
(
inf S < x -> exists2
y,
S y & y < x)
%R.
Proof.
move=> /nonemptyN S0; rewrite /inf ltr_oppl => /sup_gt => /(
_ S0)
[r [r' Sr']].
by move=> <-; rewrite ltr_oppr opprK => r'x; exists r'.
Qed.
End InfTheory.
Section
FloorTheory
.
Variable
R
: realType.
Implicit Types x y : R.
Lemma
has_sup_floor_set
x
: has_sup (
floor_set x).
Proof.
split; [exists (
- (
Num.bound (
-x))
%:~R)
| exists (
Num.bound x)
%:~R].
rewrite /floor_set/mkset rpredN rpred_int /= ler_oppl.
case: (
ger0P (
-x))
=> [/archi_boundP/ltW//|].
by move/ltW/le_trans; apply; rewrite ler0z.
apply/ubP=> y /andP[_] /le_trans; apply.
case: (
ger0P x)
=> [/archi_boundP/ltW|] //.
by move/ltW/le_trans; apply; rewrite ler0z.
Qed.
Lemma
sup_in_floor_set
x
: (
floor_set x) (
sup (
floor_set x)).
Proof.
Lemma
isint_Rfloor
x
: Rfloor x \is a Rint.
Proof.
Lemma
RfloorE
x
: Rfloor x = (
floor x)
%:~R.
Proof.
by rewrite /floor RtointK ?isint_Rfloor. Qed.
Lemma
mem_rg1_Rfloor
x
: (
range1 (
Rfloor x))
x.
Proof.
Lemma
Rfloor_le
x
: Rfloor x <= x.
Proof.
Lemma
floor_le
x
: (
floor x)
%:~R <= x.
Proof.
Lemma
lt_succ_Rfloor
x
: x < Rfloor x + 1.
Proof.
Lemma
range1z_inj
x
(
m1
m2
: int)
:
(
range1 m1%:~R)
x -> (
range1 m2%:~R)
x -> m1 = m2.
Proof.
move=> /andP[m1x x_m1] /andP[m2x x_m2].
wlog suffices: m1 m2 m1x {x_m1 m2x} x_m2 / (
m1 <= m2).
by move=> ih; apply/eqP; rewrite eq_le !ih.
rewrite -(
ler_add2r 1)
lez_addr1 -(
@ltr_int R)
intrD.
exact/(
le_lt_trans m1x).
Qed.
Lemma
range1rr
x
: (
range1 x)
x.
Proof.
Lemma
range1zP
(
m
: int)
x
: Rfloor x = m%:~R <-> (
range1 m%:~R)
x.
Proof.
split=> [<-|h]; first exact/mem_rg1_Rfloor.
apply/eqP; rewrite RfloorE eqr_int; apply/eqP/(
@range1z_inj x)
=> //.
by rewrite /range1/mkset -RfloorE mem_rg1_Rfloor.
Qed.
Lemma
Rfloor_natz
(
z
: int)
: Rfloor z%:~R = z%:~R :> R.
Proof.
by apply/range1zP/range1rr. Qed.
Lemma
Rfloor0
: Rfloor 0 = 0 :> R.
Proof.
Lemma
Rfloor1
: Rfloor 1 = 1 :> R.
Proof.
Lemma
le_Rfloor
: {homo (
@Rfloor R)
:
x
y
/ x <= y}.
Proof.
Lemma
Rfloor_ge_int
x
(
n
: int)
: (
n%:~R <= x)
= (
n%:~R <= Rfloor x).
Proof.
Lemma
Rfloor_lt_int
x
(
z
: int)
: (
x < z%:~R)
= (
Rfloor x < z%:~R).
Proof.
Lemma
Rfloor_le0
x
: x <= 0 -> Rfloor x <= 0.
Proof.
by move=> ?; rewrite -Rfloor0 le_Rfloor. Qed.
Lemma
Rfloor_lt0
x
: x < 0 -> Rfloor x < 0.
Proof.
Lemma
floor_natz
n
: floor (
n%:R : R)
= n%:~R :> int.
Proof.
Lemma
floor0
: floor (
0 : R)
= 0.
Proof.
Lemma
floor1
: floor (
1 : R)
= 1.
Proof.
Lemma
floor_ge0
x
: (
0 <= floor x)
= (
0 <= x).
Proof.
by rewrite -(
@ler_int R)
-RfloorE -Rfloor_ge_int. Qed.
Lemma
floor_le0
x
: x <= 0 -> floor x <= 0.
Proof.
by move=> ?; rewrite -(
@ler_int R)
-RfloorE Rfloor_le0. Qed.
Lemma
floor_lt0
x
: x < 0 -> floor x < 0.
Proof.
Lemma
le_floor
: {homo @floor R :
x
y
/ x <= y}.
Proof.
by move=>*; rewrite -(
@ler_int R)
!RtointK ?isint_Rfloor ?le_Rfloor. Qed.
Lemma
floor_neq0
x
: (
floor x != 0)
= (
x < 0)
|| (
x >= 1).
Proof.
Lemma
lt_succ_floor
x
: x < (
floor x)
%:~R + 1.
Proof.
Lemma
floor_lt_int
x
(
z
: int)
: (
x < z%:~R)
= (
floor x < z).
Proof.
Lemma
floor_ge_int
x
(
z
: int)
: (
z%:~R <= x)
= (
z <= floor x).
Proof.
Lemma
ltr_add_invr
(
y
x
: R)
: y < x -> exists
k,
y + k.
+1%:R^-1 < x.
Proof.
End FloorTheory.
Section
CeilTheory
.
Variable
R
: realType.
Implicit Types x y : R.
Lemma
isint_Rceil
x
: Rceil x \is a Rint.
Proof.
Lemma
Rceil0
: Rceil 0 = 0 :> R.
Proof.
Lemma
Rceil_ge
x
: x <= Rceil x.
Proof.
Lemma
le_Rceil
: {homo (
@Rceil R)
:
x
y
/ x <= y}.
Proof.
Lemma
Rceil_ge0
x
: 0 <= x -> 0 <= Rceil x.
Proof.
by move=> ?; rewrite -Rceil0 le_Rceil. Qed.
Lemma
RceilE
x
: Rceil x = (
ceil x)
%:~R.
Proof.
Lemma
ceil_ge
x
: x <= (
ceil x)
%:~R.
Proof.
by rewrite -RceilE; exact: Rceil_ge. Qed.
Lemma
ceil_ge0
x
: 0 <= x -> 0 <= ceil x.
Proof.
Lemma
ceil_gt0
x
: 0 < x -> 0 < ceil x.
Proof.
Lemma
ceil_le0
x
: x <= 0 -> ceil x <= 0.
Proof.
Lemma
le_ceil
: {homo @ceil R :
x
y
/ x <= y}.
Proof.
Lemma
ceil_ge_int
x
(
z
: int)
: (
x <= z%:~R)
= (
ceil x <= z).
Proof.
Lemma
ceil_lt_int
x
(
z
: int)
: (
z%:~R < x)
= (
z < ceil x).
Proof.
Lemma
ceilN
x
: ceil (
- x)
= - floor x
Proof.
by rewrite /ceil opprK. Qed.
Lemma
floorN
x
: floor (
- x)
= - ceil x
Proof.
by rewrite /ceil opprK. Qed.
End CeilTheory.
Section
Sup
.
Context {R : realType}.
Implicit Types A B : set R.
Lemma
le_down
A
: A `<=` down A.
Proof.
by move=> x xA; apply/downP; exists x. Qed.
Lemma
downK
A
: down (
down A)
= down A.
Proof.
rewrite predeqE => x; split; last by move=> Ax; apply/downP; exists x.
case/downP => y /downP[z Az yz xy].
by apply/downP; exists z => //; rewrite (
le_trans xy).
Qed.
Lemma
has_sup_down
A
: has_sup (
down A)
<-> has_sup A.
Proof.
split=> -[nzA nzubA].
case: nzA => x /downP[y yS le_xy]; split; first by exists y.
case: nzubA=> u /ubP ubA; exists u; apply/ubP=> z zS.
by apply/ubA; apply/downP; exists z.
case: nzA => x xA; split; first by exists x; apply/le_down.
case: nzubA => u /ubP ubA; exists u; apply/ubP=> y /downP [].
by move=> z zA /le_trans; apply; apply/ubA.
Qed.
Lemma
le_sup
A
B
: A `<=` down B -> nonempty A -> has_sup B ->
sup A <= sup B.
Proof.
move=> le_AB nz_A hs_B; have hs_A: has_sup A.
split=> //; case: hs_B => _ [x ubx].
exists x; apply/ubP=> y /le_AB /downP[z zB le_yz].
by apply/(
le_trans le_yz)
; move/ubP: ubx; apply.
rewrite leNgt -subr_gt0; apply/negP => lt_sup.
case: (
sup_adherent lt_sup hs_A )
=> x /le_AB xdB.
rewrite subKr => lt_Bx; case/downP: xdB => z zB.
move/(
lt_le_trans lt_Bx)
; rewrite ltNge.
by move/ubP : (
sup_upper_bound hs_B)
=> ->.
Qed.
Lemma
le_inf
A
B
: -%R @` B `<=` down (
-%R @` A)
-> nonempty B -> has_inf A ->
inf A <= inf B.
Proof.
Lemma
sup_down
A
: sup (
down A)
= sup A.
Proof.
have [supA|supNA] := pselect (
has_sup A)
; last first.
by rewrite !sup_out // => /has_sup_down.
have supDA : has_sup (
down A)
by apply/has_sup_down.
apply/eqP; rewrite eq_le !le_sup //.
- by case: supA => -[x xA] _; exists x; apply/le_down.
- by rewrite downK; exact: le_down.
- by case: supA.
Qed.
Lemma
lt_sup_imfset
{T : Type} (
F
: T -> R)
l
:
has_sup [set
y
| exists
x,
y = F x] ->
l < sup [set
y
| exists
x,
y = F x] ->
exists2
x,
l < F x & F x <= sup [set
y
| exists
x,
y = F x].
Proof.
set P := [set
y
| _] => hs; rewrite -subr_gt0.
move=> /sup_adherent/(
_ hs)
[_ [x ->]]; rewrite subKr=> lt_lFx.
by exists x => //; move/ubP : (
sup_upper_bound hs)
=> -> //; exists x.
Qed.
Lemma
lt_inf_imfset
{T : Type} (
F
: T -> R)
l
:
has_inf [set
y
| exists
x,
y = F x] ->
inf [set
y
| exists
x,
y = F x] < l ->
exists2
x,
F x < l & inf [set
y
| exists
x,
y = F x] <= F x.
Proof.
set P := [set
y
| _]; move=> hs; rewrite -subr_gt0.
move=> /inf_adherent/(
_ hs)
[_ [x ->]]; rewrite addrCA subrr addr0 => ltFxl.
by exists x=> //; move/lbP : (
inf_lower_bound hs)
=> -> //; exists x.
Qed.
End Sup.
Lemma
int_lbound_has_minimum
(
B
: set int)
i
: B !=set0 -> lbound B i ->
exists
j,
B j /\ forall
k,
B k -> j <= k.
Proof.
move=> [i0 Bi0] lbBi; have [n i0in] : exists
n,
i0 - i = n%:Z.
by exists `|i0 - i|%N; rewrite gez0_abs // subr_ge0; exact: lbBi.
elim: n i lbBi i0in => [i lbBi /eqP|n ih i lbBi i0in1].
by rewrite subr_eq0 => /eqP i0i; exists i0; split =>// k Bk; rewrite i0i lbBi.
have i0i1n : i0 - (
i + 1)
= n by rewrite opprD addrA i0in1 -addn1 PoszD addrK.
have [?|/not_forallP] := pselect (
lbound B (
i + 1))
; first exact: (
ih (
i + 1)).
move=> /contrapT[x /not_implyP[Bx i1x]]; exists x; split => // k Bk.
rewrite (
le_trans _ (
lbBi _ Bk))
//.
by move/negP : i1x; rewrite -ltNge ltz_addr1.
Qed.
Section
rat_in_itvoo
.
Let
bound_div
(
R
: archiFieldType) (
x
y
: R)
: nat :=
if y < 0 then 0%N else Num.bound (
y / x).
Let
archi_bound_divP
(
R
: archiFieldType) (
x
y
: R)
:
0 < x -> y < x *+ bound_div x y.
Proof.
Lemma
rat_in_itvoo
(
R
: realType) (
x
y
: R)
:
x < y -> exists
q,
ratr q \in `]x, y[.
Proof.
End rat_in_itvoo.