Top source

Module mathcomp.analysis.topology_theory.nat_topology

From HB Require Import structures.
From mathcomp Require Import boot order algebra all_classical.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import reals topology_structure uniform_structure.
From mathcomp Require Import pseudometric_structure order_topology.
From mathcomp Require Import discrete_topology.


Unset SsrOldRewriteGoalsOrder.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

:=

---

Source code

hasNbhs

---

Source code

.Build nat principal_filter.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

:=

---

Source code

Discrete_ofNbhs

---

Source code

.Build nat erefl.

Local Lemma

nat_nbhs_itv

---

Source code

(

n

---

Source code

: nat) :
  nbhs n = filter_from
    (fun

i

---

Source code

=> itv_open_ends i /\ n \in i)
    (fun

i

---

Source code

=> [set` i]).

Proof.

rewrite nbhs_principalE eqEsubset; split=> U; first last.
  by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb.
move/principal_filterP; case: n.
  move=> U0; exists `]-oo, 1[; first split => //.
  by move=> r /=; rewrite in_itv /=; case: r.
move=> n USn; exists `]n, n.+2[; first split => //.
  by rewrite in_itv; apply/andP;split => //=; rewrite /Order.lt //=.
move=> r /=; rewrite in_itv /= => nr2; suff: r = n.+1 by move=> ->.
exact/esym/le_anti.
Qed.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

:=

---

Source code

Order_isNbhs

---

Source code

.Build _ nat nat_nbhs_itv.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

:=

---

Source code

DiscreteUniform_ofNbhs

---

Source code

.Build nat.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

{R

---

Source code

:

---

Source code

numDomainType}

---

Source code

:=
  @DiscretePseudoMetric_ofUniform.Build R nat.

Lemma

nbhs_infty_gt

---

Source code

N

---

Source code

: \forall

n

---

Source code

\near \oo, (N < n)%N.

Proof.

by exists N.+1. Qed.

#[global] Hint Resolve nbhs_infty_gt : core.

Lemma

nbhs_infty_ge

---

Source code

N

---

Source code

: \forall

n

---

Source code

\near \oo, (N <= n)%N.

Proof.

by exists N. Qed.

Lemma

nbhs_infty_ger

---

Source code

{

R

---

Source code

: realType} (

r

---

Source code

: R) :
  \forall

n

---

Source code

\near \oo, (r <= n%:R)%R.

Proof.

exists (Num.bound r) => // n /=; rewrite -(ler_nat R).
by apply/le_trans/ltW/ltr_bound.
Qed.

Lemma

cvg_addnl

---

Source code

N

---

Source code

: addn N @ \oo --> \oo.

Proof.

by move=> P [n _ Pn]; exists (n - N)%N => // m; rewrite /= leq_subLR => /Pn.
Qed.

Lemma

cvg_addnr

---

Source code

N

---

Source code

: addn^~ N @ \oo --> \oo.

Proof.

by under [addn^~ N]funext => n do rewrite addnC; apply: cvg_addnl. Qed.

Lemma

cvg_subnr

---

Source code

N

---

Source code

: subn^~ N @ \oo --> \oo.

Proof.

move=> P [n _ Pn]; exists (N + n)%N => //= m le_m.
by apply: Pn; rewrite /= leq_subRL// (leq_trans _ le_m)// leq_addr.
Qed.

Lemma

cvg_mulnl

---

Source code

N

---

Source code

: (N > 0)%N -> muln N @ \oo --> \oo.

Proof.

case: N => N // _ P [n _ Pn]; exists (n %/ N.+1).+1 => // m.
by rewrite /= ltn_divLR// => n_lt; apply: Pn; rewrite mulnC /= ltnW.
Qed.

Lemma

cvg_mulnr

---

Source code

N

---

Source code

:(N > 0)%N -> muln^~ N @ \oo --> \oo.

Proof.

by move=> N_gt0; under [muln^~ N]funext => n do rewrite mulnC; apply: cvg_mulnl.
Qed.

Lemma

cvg_divnr

---

Source code

N

---

Source code

: (N > 0)%N -> divn^~ N @ \oo --> \oo.

Proof.

move=> N_gt0 P [n _ Pn]; exists (n * N)%N => //= m.
by rewrite /= -leq_divRL//; apply: Pn.
Qed.

Lemma

near_inftyS

---

Source code

(

P

---

Source code

: set nat) :
  (\forall

x

---

Source code

\near \oo, P (S x)) -> (\forall

x

---

Source code

\near \oo, P x).

Proof.

case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed.

Section infty_nat.
Local Open Scope nat_scope.

Let

cvgnyP

---

Source code

{

F

---

Source code

: set_system nat} {

FF

---

Source code

: Filter F} : [<->
F --> \oo;
forall

A

---

Source code

, \forall

x

---

Source code

\near F, A <= x;
forall

A

---

Source code

, \forall

x

---

Source code

\near F, A < x;
\forall

A

---

Source code

\near \oo, \forall

x

---

Source code

\near F, A < x;
\forall

A

---

Source code

\near \oo, \forall

x

---

Source code

\near F, A <= x ].

Proof.

tfae; first by move=> Foo A; apply: Foo; apply: nbhs_infty_ge.
- move=> AF A; near \oo => B; near=> x.
  suff : (B <= x)%N by apply: leq_trans; near: B; apply: nbhs_infty_gt.
  by near: x; apply: AF; near: B.
- by move=> Foo; near do apply: Foo.
- by apply: filterS => ?; apply: filterS => ?; apply: ltnW.
case=> [A _ AF] P [n _ Pn]; near \oo => B; near=> m; apply: Pn => /=.
suff: (B <= m)%N by apply: leq_trans; near: B; apply: nbhs_infty_ge.
by near: m; apply: AF; near: B; apply: nbhs_infty_ge.
Unshelve. all: end_near. Qed.

Section map.

Context {

I

---

Source code

: Type} {

F

---

Source code

: set_system I} {

FF

---

Source code

: Filter F} (

f

---

Source code

: I -> nat).

Lemma

cvgnyPge

---

Source code

:
  f @ F --> \oo <-> forall

A

---

Source code

, \forall

x

---

Source code

\near F, A <= f x.

Proof.

exact: (cvgnyP 0%N 1%N). Qed.

Lemma

cvgnyPgt

---

Source code

:
  f @ F --> \oo <-> forall

A

---

Source code

, \forall

x

---

Source code

\near F, A < f x.

Proof.

exact: (cvgnyP 0%N 2%N). Qed.

Lemma

cvgnyPgty

---

Source code

:
  f @ F --> \oo <-> \forall

A

---

Source code

\near \oo, \forall

x

---

Source code

\near F, A < f x.

Proof.

exact: (cvgnyP 0%N 3%N). Qed.

Lemma

cvgnyPgey

---

Source code

:
  f @ F --> \oo <-> \forall

A

---

Source code

\near \oo, \forall

x

---

Source code

\near F, A <= f x.

Proof.

exact: (cvgnyP 0%N 4%N). Qed.

End map.

End infty_nat.