Files

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.

# Topology for natural numbers Natural numbers `nat` are endowed with the structure of topology.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code hasNbhsSource code.Build nat principal_filter.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Discrete_ofNbhsSource code.Build nat erefl.

Local Lemma nat_nbhs_itvSource code (nSource code : nat) :
  nbhs n = filter_from
    (fun iSource code => itv_open_ends i /\ n \in i)
    (fun iSource 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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Order_isNbhsSource code.Build _ nat nat_nbhs_itv.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code DiscreteUniform_ofNbhsSource code.Build nat.
HBSource code.instanceSource code DefinitionSource code _Source code {RSource code :Source code numDomainType}Source code :=
  @DiscretePseudoMetric_ofUniform.Build R nat.

Lemma nbhs_infty_gtUsed by
  • mathcomp.analysis.sequences
  • mathcomp.analysis.normedtype_theory.ereal_normedtype
Source code NSource code : \forall nSource code \near \oo, (N < n)%N.
Proof.
by exists N.+1. Qed.
#[global] Hint Resolve nbhs_infty_gt : core.

Lemma nbhs_infty_geUsed by
  • mathcomp.analysis.sequences
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code NSource code : \forall nSource code \near \oo, (N <= n)%N.
Proof.
by exists N. Qed.

Lemma nbhs_infty_gerUsed by
  • mathcomp.analysis.probability_theory.random_variable
  • mathcomp.analysis.realfun
  • mathcomp.analysis.ftc
  • mathcomp.analysis.sequences
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
  • mathcomp.analysis.normedtype_theory.ereal_normedtype
  • mathcomp.analysis.normedtype_theory.num_normedtype
  • mathcomp.analysis.exp
Source code {RSource code : realType} (rSource code : R) :
  \forall nSource 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_addnlSource code NSource code : addn N @ \oo --> \oo.
Proof.
by move=> P [n _ Pn]; exists (n - N)%N => // m; rewrite /= leq_subLR => /Pn.
Qed.

Lemma cvg_addnrUsed by
  • mathcomp.analysis.sequences
  • mathcomp.analysis.lebesgue_integral_theory.radon_nikodym
Source code NSource code : addn^~ N @ \oo --> \oo.
Proof.
by under [addn^~ N]funext => n do rewrite addnC; apply: cvg_addnl. Qed.

Lemma cvg_subnrUsed by
  • mathcomp.analysis.sequences
Source code NSource 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_mulnlSource code NSource 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_mulnrSource code NSource 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_divnrSource code NSource 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_inftySUsed by
  • mathcomp.analysis.sequences
Source code (PSource code : set nat) :
  (\forall xSource code \near \oo, P x.+1) -> (\forall xSource code \near \oo, P x).
Proof.
by case=> N _ NPS; exists N.+1 => // [[]]; rewrite ?ltn0. Qed.

Lemma near_infty_leqUsed by
  • mathcomp.analysis.sequences
Source code (PSource code : set nat) :
  (\forall nSource code \near \oo, P n) <->
  (\forall NSource code \near \oo, forall nSource code, (n >= N)%N -> P n).
Proof.
split => [[N _ /= NP]|].
  by exists N => // n/= Nn m /(leq_trans Nn); exact: NP.
by apply: filterS => N; exact.
Qed.

Section infty_nat.
Local Open Scope nat_scope.

Let cvgnyPSource code {FSource code : set_system nat} {FFSource code : Filter F} : [<->
F --> \oo;
forall ASource code, \forall xSource code \near F, A <= x;
forall ASource code, \forall xSource code \near F, A < x;
\forall ASource code \near \oo, \forall xSource code \near F, A < x;
\forall ASource code \near \oo, \forall xSource 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 {ISource code : Type} {FSource code : set_system I} {FFSource code : Filter F} (fSource code : I -> nat).

Lemma cvgnyPgeUsed by
  • mathcomp.analysis.normedtype_theory.num_normedtype
Source code :
  f @ F --> \oo <-> forall ASource code, \forall xSource code \near F, A <= f x.
Proof.
exact: (cvgnyP 0%N 1%N). Qed.

Lemma cvgnyPgtUsed by
  • mathcomp.analysis.sequences
Source code :
  f @ F --> \oo <-> forall ASource code, \forall xSource code \near F, A < f x.
Proof.
exact: (cvgnyP 0%N 2%N). Qed.

Lemma cvgnyPgtySource code :
  f @ F --> \oo <-> \forall ASource code \near \oo, \forall xSource code \near F, A < f x.
Proof.
exact: (cvgnyP 0%N 3%N). Qed.

Lemma cvgnyPgeySource code :
  f @ F --> \oo <-> \forall ASource code \near \oo, \forall xSource code \near F, A <= f x.
Proof.
exact: (cvgnyP 0%N 4%N). Qed.

End map.

End infty_nat.
Generated by rocqnavi
Source
Uses
Used By