Library mathcomp.analysis.normedtype

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
From mathcomp.classical Require Import boolp classical_sets functions.
From mathcomp.classical Require Import cardinality set_interval mathcomp_extra.
Require Import ereal reals signed topology prodnormedzmodule.

This file extends the topological hierarchy with norm-related notions. Note that balls in topology.v are not necessarily open, here they are.

Normed Topological Abelian groups:

pseudoMetricNormedZmodType R == interface type for a normed topological Abelian group equipped with a norm PseudoMetricNormedZmodule.Mixin nb == builds the mixin for a normed topological Abelian group from the compatibility between the norm and balls; the carrier type must have a normed Zmodule over a numDomainType.

Normed modules :

normedModType K == interface type for a normed module structure over the numDomainType K. NormedModMixin normZ == builds the mixin for a normed module from the property of the linearity of the norm; the carrier type must have a pseudoMetricNormedZmodType structure NormedModType K T m == packs the mixin m to build a normedModType K; T must have canonical pseudoMetricNormedZmodType K and pseudoMetricType structures. [normedModType K of T for cT] == T-clone of the normedModType K structure cT. [normedModType K of T] == clone of a canonical normedModType K structure on T. `|x| == the norm of x (notation from ssrnum). ball_norm == balls defined by the norm. nbhs_norm == neighborhoods defined by the norm. closed_ball == closure of a ball. f @`[ a , b ], f @`] a , b [ == notations for images of intervals, intended for continuous, monotonous functions, defined in ring_scope and classical_set_scope respectively as: f @`[ a , b ] := `[minr (f a) (f b), maxr (f a) (f b) ]%O f @`] a , b [ := `]minr (f a) (f b), maxr (f a) (f b) [%O f @`[ a , b ] := `[minr (f a) (f b), maxr (f a) (f b) ]%classic f @`] a , b [ := `]minr (f a) (f b), maxr (f a) (f b) [%classic

Domination notations:

dominated_by h k f F == `|f| <= k * `|h|, near F bounded_near f F == f is bounded near F [bounded f x | x in A] == f is bounded on A, ie F := globally A [locally [bounded f x | x in A] == f is locally bounded on A bounded_set == set of bounded sets. := [set A | [bounded x | x in A] ] bounded_fun == set of functions bounded on their whole domain. := [set f | [bounded f x | x in setT] ] lipschitz_on f F == f is lipschitz near F [lipschitz f x | x in A] == f is lipschitz on A [locally [lipschitz f x | x in A] == f is locally lipschitz on A k.-lipschitz_on f F == f is k.-lipschitz near F k.-lipschitz_A f == f is k.-lipschitz on A [locally k.-lipschitz_A f] == f is locally k.-lipschitz on A contraction q f == f is q.-lipschitz and q < 1 is_contraction f == exists q, f is q.-lipschitz and q < 1 is_interval E == the set E is an interval bigcup_ointsub U q == union of open real interval included in U and that contain the rational number q Rhull A == the real interval hull of a set A shift x y == y + x center c := shift (- c)

Complete normed modules :

completeNormedModType K == interface type for a complete normed module structure over a realFieldType K. [completeNormedModType K of T] == clone of a canonical complete normed module structure over K on T.

Filters :

at_left x, at_right x == filters on real numbers for predicates s.t. nbhs holds on the left/right of x --> We used these definitions to prove the intermediate value theorem and the Heine-Borel theorem, which states that the compact sets of R^n are the closed and bounded sets.

Reserved Notation "f @`[ a , b ]" (at level 20, b at level 9,
  format "f @`[ a , b ]").
Reserved Notation "f @`] a , b [" (at level 20, b at level 9,
  format "f @`] a , b [").
Reserved Notation "x ^'+" (at level 3, format "x ^'+").
Reserved Notation "x ^'-" (at level 3, format "x ^'-").
Reserved Notation "+oo_ R" (at level 3, format "+oo_ R").
Reserved Notation "-oo_ R" (at level 3, format "-oo_ R").
Reserved Notation "[ 'bounded' E | x 'in' A ]"
  (at level 0, x name, format "[ 'bounded' E | x 'in' A ]").
Reserved Notation "k .-lipschitz_on f"
  (at level 2, format "k .-lipschitz_on f").
Reserved Notation "k .-lipschitz_ A f"
  (at level 2, A at level 0, format "k .-lipschitz_ A f").
Reserved Notation "k .-lipschitz f" (at level 2, format "k .-lipschitz f").
Reserved Notation "[ 'lipschitz' E | x 'in' A ]"
  (at level 0, x name, format "[ 'lipschitz' E | x 'in' A ]").

Set Implicit Arguments.

Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Definition pointed_of_zmodule (R : zmodType) : pointedType := PointedType R 0.

Definition filtered_of_normedZmod (K : numDomainType) (R : normedZmodType K)
  : filteredType R := Filtered.Pack (Filtered.Class
    (@Pointed.class (pointed_of_zmodule R))
    (nbhs_ball_ (ball_ (fun x ⇒ `|x|)))).

Section pseudoMetric_of_normedDomain.
Variables (K : numDomainType) (R : normedZmodType K).
Lemma ball_norm_center (x : R) (e : K) : 0 < e → ball_ normr x e x.
Lemma ball_norm_symmetric (x y : R) (e : K) :
  ball_ normr x e y → ball_ normr y e x.
Lemma ball_norm_triangle (x y z : R) (e1 e2 : K) :
  ball_ normr x e1 y → ball_ normr y e2 z → ball_ normr x (e1 + e2) z.
Definition pseudoMetric_of_normedDomain
  : PseudoMetric.mixin_of K (@entourage_ K R R (ball_ (fun x ⇒ `|x|)))
  := PseudoMetricMixin ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.

Lemma nbhs_ball_normE :
  @nbhs_ball_ K R R (ball_ normr) = nbhs_ (entourage_ (ball_ normr)).
End pseudoMetric_of_normedDomain.

Lemma nbhsN (R : numFieldType) (x : R) : nbhs (- x) = -%R @ x.

Lemma nbhsNimage (R : numFieldType) (x : R) :
  nbhs (- x) = [set -%R @` A | A in nbhs x ].

Lemma nearN (R : numFieldType) (x : R) (P : R → Prop) :
  (\∀ y \near - x , P y ) ↔ \near x , P (- x).

Lemma openN (R : numFieldType) (A : set R) :
  open A → open [set - x | x in A ].

Lemma closedN (R : numFieldType) (A : set R) :
  closed A → closed [set - x | x in A ].

Module PseudoMetricNormedZmodule.
Section ClassDef.
Variable R : numDomainType.
Record mixin_of (T : normedZmodType R) (ent : set (set (T × T)))
    (m : PseudoMetric.mixin_of R ent) := Mixin {
  _ : PseudoMetric.ball m = ball_ (fun x ⇒ `| x |) }.

Record class_of (T : Type) := Class {
  base : Num.NormedZmodule.class_of R T;
  pointed_mixin : Pointed.point_of T ;
  nbhs_mixin : Filtered.nbhs_of T T ;
  topological_mixin : @Topological.mixin_of T nbhs_mixin ;
  uniform_mixin : @Uniform.mixin_of T nbhs_mixin ;
  pseudoMetric_mixin :
    @PseudoMetric.mixin_of R T (Uniform.entourage uniform_mixin) ;
  mixin : @mixin_of (Num.NormedZmodule.Pack _ base) _ pseudoMetric_mixin
}.
Definition base2 T c := @PseudoMetric.Class _ _
    (@Uniform.Class _
      (@Topological.Class _
        (Filtered.Class
         (Pointed.Class (@base T c) (pointed_mixin c))
         (nbhs_mixin c))
        (topological_mixin c))
      (uniform_mixin c))
    (pseudoMetric_mixin c).

TODO: base3?

Structure type (phR : phant R) :=
  Pack { sort; _ : class_of sort }.

Variables (phR : phant R) (T : Type) (cT : type phR).

Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack phR T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack (b0 : Num.NormedZmodule.class_of R T) lm0 um0
  (m0 : @mixin_of (@Num.NormedZmodule.Pack R (Phant R) T b0) lm0 um0) :=
  fun bT (b : Num.NormedZmodule.class_of R T)
      & phant_id (@Num.NormedZmodule.class R (Phant R) bT) b ⇒
  fun uT (u : PseudoMetric.class_of R T) & phant_id (@PseudoMetric.class R uT) u ⇒
  fun (m : @mixin_of (Num.NormedZmodule.Pack _ b) _ u) & phant_id m m0 ⇒
  @Pack phR T (@Class T b u u u u u m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition zmodType := @GRing.Zmodule.Pack cT xclass.
Definition normedZmodType := @Num.NormedZmodule.Pack R phR cT xclass.
Definition pointedType := @Pointed.Pack cT xclass.
Definition filteredType := @Filtered.Pack cT cT xclass.
Definition topologicalType := @Topological.Pack cT xclass.
Definition uniformType := @Uniform.Pack cT xclass.
Definition pseudoMetricType := @PseudoMetric.Pack R cT xclass.
Definition pointed_zmodType := @GRing.Zmodule.Pack pointedType xclass.
Definition filtered_zmodType := @GRing.Zmodule.Pack filteredType xclass.
Definition topological_zmodType := @GRing.Zmodule.Pack topologicalType xclass.
Definition uniform_zmodType := @GRing.Zmodule.Pack uniformType xclass.
Definition pseudoMetric_zmodType := @GRing.Zmodule.Pack pseudoMetricType xclass.
Definition pointed_normedZmodType := @Num.NormedZmodule.Pack R phR pointedType xclass.
Definition filtered_normedZmodType := @Num.NormedZmodule.Pack R phR filteredType xclass.
Definition topological_normedZmodType := @Num.NormedZmodule.Pack R phR topologicalType xclass.
Definition uniform_normedZmodType := @Num.NormedZmodule.Pack R phR uniformType xclass.
Definition pseudoMetric_normedZmodType := @Num.NormedZmodule.Pack R phR pseudoMetricType xclass.

End ClassDef.

Definition numDomain_normedDomainType (R : numDomainType) : type (Phant R) := Pack (Phant R) (@Class R _ _ (NumDomain.normed_mixin (NumDomain.class R))).

Module Exports.
Coercion base : class_of >-> Num.NormedZmodule.class_of.
Coercion base2 : class_of >-> PseudoMetric.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion normedZmodType : type >-> Num.NormedZmodule.type.
Canonical normedZmodType.
Coercion pointedType : type >-> Pointed.type.
Canonical pointedType.
Coercion filteredType : type >-> Filtered.type.
Canonical filteredType.
Coercion topologicalType : type >-> Topological.type.
Canonical topologicalType.
Coercion uniformType : type >-> Uniform.type.
Canonical uniformType.
Coercion pseudoMetricType : type >-> PseudoMetric.type.
Canonical pseudoMetricType.
Canonical pointed_zmodType.
Canonical filtered_zmodType.
Canonical topological_zmodType.
Canonical uniform_zmodType.
Canonical pseudoMetric_zmodType.
Canonical pointed_normedZmodType.
Canonical filtered_normedZmodType.
Canonical topological_normedZmodType.
Canonical uniform_normedZmodType.
Canonical pseudoMetric_normedZmodType.
Notation pseudoMetricNormedZmodType R := (type (Phant R)).
Notation PseudoMetricNormedZmodType R T m :=
  (@pack _ (Phant R) T _ _ _ m _ _ idfun _ _ idfun _ idfun).
Notation "[ 'pseudoMetricNormedZmodType' R 'of' T 'for' cT ]" :=
  (@clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'pseudoMetricNormedZmodType' R 'of' T 'for' cT ]") :
  form_scope.
Notation "[ 'pseudoMetricNormedZmodType' R 'of' T ]" :=
  (@clone _ (Phant R) T _ _ idfun)
  (at level 0, format "[ 'pseudoMetricNormedZmodType' R 'of' T ]") : form_scope.
End Exports.

End PseudoMetricNormedZmodule.
Export PseudoMetricNormedZmodule.Exports.

Section pseudoMetricnormedzmodule_lemmas.
Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}.

Lemma ball_normE : ball_norm = ball.

End pseudoMetricnormedzmodule_lemmas.

neighborhoods

Section Nbhs'.
Context {R : numDomainType} {T : pseudoMetricType R}.

Lemma ex_ball_sig (x : T) (P : set T) :
  ¬ (∀ eps : {posnum R }, ¬ (ball x eps %:num `<=` ~` P )) →
    {d : {posnum R } | ball x d %:num `<=` ~` P }.

Lemma nbhsC (x : T) (P : set T) :
  ¬ (∀ eps : {posnum R }, ¬ (ball x eps %:num `<=` ~` P )) →
  nbhs x (~` P).

Lemma nbhsC_ball (x : T) (P : set T) :
  nbhs x (~` P) → {d : {posnum R } | ball x d %:num `<=` ~` P }.

Lemma nbhs_ex (x : T) (P : T → Prop) : nbhs x P →
  {d : {posnum R } | ∀ y, ball x d %:num y → P y }.

End Nbhs'.

Lemma coord_continuous {K : numFieldType} m n i j :
  continuous (fun M : 'M[K]_(m, n) ⇒ M i j).

Global Instance Proper_dnbhs_numFieldType (R : numFieldType) (x : R) :
  ProperFilter x ^'.

#[global] Hint Extern 0 (ProperFilter _^') ⇒
  (apply: Proper_dnbhs_numFieldType) : typeclass_instances.

Some Topology on extended real numbers

Definition pinfty_nbhs (R : numFieldType) : set (set R) :=
  fun P ⇒ ∃ M , M \is Num.real ∧ ∀ x, M < x → P x.
Arguments pinfty_nbhs R : clear implicits.
Definition ninfty_nbhs (R : numFieldType) : set (set R) :=
  fun P ⇒ ∃ M , M \is Num.real ∧ ∀ x, x < M → P x.
Arguments ninfty_nbhs R : clear implicits.

Notation "+oo_ R" := (pinfty_nbhs [numFieldType of R])
  (only parsing) : ring_scope.
Notation "-oo_ R" := (ninfty_nbhs [numFieldType of R])
  (only parsing) : ring_scope.

Notation "+oo" := (pinfty_nbhs _) : ring_scope.
Notation "-oo" := (ninfty_nbhs _) : ring_scope.

Section infty_nbhs_instances.
Context {R : numFieldType}.
Let R_topologicalType := [topologicalType of R ].
Implicit Types r : R.

Global Instance proper_pinfty_nbhs : ProperFilter (pinfty_nbhs R).

Global Instance proper_ninfty_nbhs : ProperFilter (ninfty_nbhs R).

Lemma nbhs_pinfty_gt r : r \is Num.real → \∀ x \near +oo , r < x.

Lemma nbhs_pinfty_ge r : r \is Num.real → \∀ x \near +oo , r ≤ x.

Lemma nbhs_ninfty_lt r : r \is Num.real → \∀ x \near -oo , r > x.

Lemma nbhs_ninfty_le r : r \is Num.real → \∀ x \near -oo , r ≥ x.

Lemma nbhs_pinfty_real : \∀ x \near +oo , x \is @Num.real R.

Lemma nbhs_ninfty_real : \∀ x \near -oo , x \is @Num.real R.

Lemma pinfty_ex_gt (m : R) (A : set R) : m \is Num.real →
  (\∀ k \near +oo , A k ) → exists2 M , m < M & A M.

Lemma pinfty_ex_ge (m : R) (A : set R) : m \is Num.real →
  (\∀ k \near +oo , A k ) → exists2 M , m ≤ M & A M.

Lemma pinfty_ex_gt0 (A : set R) :
  (\∀ k \near +oo , A k ) → exists2 M , M > 0 & A M.

Lemma near_pinfty_div2 (A : set R) :
  (\∀ k \near +oo , A k ) → (\∀ k \near +oo , A (k / 2)).

End infty_nbhs_instances.

#[global] Hint Extern 0 (is_true (_ < ?x)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_pinfty_gt end : core.
#[global] Hint Extern 0 (is_true (_ ≤ ?x)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_pinfty_ge end : core.
#[global] Hint Extern 0 (is_true (_ > ?x)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_ninfty_lt end : core.
#[global] Hint Extern 0 (is_true (_ ≥ ?x)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_ninfty_le end : core.
#[global] Hint Extern 0 (is_true (?x \is Num.real)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_pinfty_real end : core.
#[global] Hint Extern 0 (is_true (?x \is Num.real)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_ninfty_real end : core.

#[global] Hint Extern 0 (is_true (_ < ?x)%E) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: ereal_nbhs_pinfty_gt end : core.
#[global] Hint Extern 0 (is_true (_ ≤ ?x)%E) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: ereal_nbhs_pinfty_ge end : core.
#[global] Hint Extern 0 (is_true (_ > ?x)%E) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: ereal_nbhs_ninfty_lt end : core.
#[global] Hint Extern 0 (is_true (_ ≥ ?x)%E) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: ereal_nbhs_ninfty_le end : core.
#[global] Hint Extern 0 (is_true (fine ?x \is Num.real)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: ereal_nbhs_pinfty_real end : core.
#[global] Hint Extern 0 (is_true (fine ?x \is Num.real)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: ereal_nbhs_ninfty_real end : core.

Section cvg_infty_numField.
Context {R : numFieldType}.

Let cvgryPnum {F : set (set R)} {FF : Filter F} : [<->
(* 0 *) F --> +oo;
(* 1 *) ∀ A, A \is Num.real → \∀ x \near F , A ≤ x;
(* 2 *) ∀ A, A \is Num.real → \∀ x \near F , A < x;
(* 3 *) \∀ A \near +oo , \∀ x \near F , A < x;
(* 4 *) \∀ A \near +oo , \∀ x \near F , A ≤ x ].

Let cvgrNyPnum {F : set (set R)} {FF : Filter F} : [<->
F --> -oo;
∀ A, A \is Num.real → \∀ x \near F , A ≥ x;
∀ A, A \is Num.real → \∀ x \near F , A > x;
\∀ A \near -oo , \∀ x \near F , A > x;
\∀ A \near -oo , \∀ x \near F , A ≥ x ].

Context {T} {F : set (set T)} {FF : Filter F}.
Implicit Types f : T → R.

Lemma cvgryPger f :
  f @ F --> +oo ↔ ∀ A, A \is Num.real → \∀ x \near F , A ≤ f x.

Lemma cvgryPgtr f :
  f @ F --> +oo ↔ ∀ A, A \is Num.real → \∀ x \near F , A < f x.

Lemma cvgryPgty f :
  f @ F --> +oo ↔ \∀ A \near +oo , \∀ x \near F , A < f x.

Lemma cvgryPgey f :
  f @ F --> +oo ↔ \∀ A \near +oo , \∀ x \near F , A ≤ f x.

Lemma cvgrNyPler f :
  f @ F --> -oo ↔ ∀ A, A \is Num.real → \∀ x \near F , A ≥ f x.

Lemma cvgrNyPltr f :
  f @ F --> -oo ↔ ∀ A, A \is Num.real → \∀ x \near F , A > f x.

Lemma cvgrNyPltNy f :
  f @ F --> -oo ↔ \∀ A \near -oo , \∀ x \near F , A > f x.

Lemma cvgrNyPleNy f :
  f @ F --> -oo ↔ \∀ A \near -oo , \∀ x \near F , A ≥ f x.

Lemma cvgry_ger f :
  f @ F --> +oo → ∀ A, A \is Num.real → \∀ x \near F , A ≤ f x.

Lemma cvgry_gtr f :
  f @ F --> +oo → ∀ A, A \is Num.real → \∀ x \near F , A < f x.

Lemma cvgrNy_ler f :
  f @ F --> -oo → ∀ A, A \is Num.real → \∀ x \near F , A ≥ f x.

Lemma cvgrNy_ltr f :
  f @ F --> -oo → ∀ A, A \is Num.real → \∀ x \near F , A > f x.

Lemma cvgNry f : (- f @ F --> +oo ) ↔ (f @ F --> -oo ).

Lemma cvgNrNy f : (- f @ F --> -oo ) ↔ (f @ F --> +oo ).

End cvg_infty_numField.

Section cvg_infty_realField.
Context {R : realFieldType}.
Context {T} {F : set (set T)} {FF : Filter F} (f : T → R).

Lemma cvgryPge : f @ F --> +oo ↔ ∀ A, \∀ x \near F , A ≤ f x.

Lemma cvgryPgt : f @ F --> +oo ↔ ∀ A, \∀ x \near F , A < f x.

Lemma cvgrNyPle : f @ F --> -oo ↔ ∀ A, \∀ x \near F , A ≥ f x.

Lemma cvgrNyPlt : f @ F --> -oo ↔ ∀ A, \∀ x \near F , A > f x.

Lemma cvgry_ge : f @ F --> +oo → ∀ A, \∀ x \near F , A ≤ f x.

Lemma cvgry_gt : f @ F --> +oo → ∀ A, \∀ x \near F , A < f x.

Lemma cvgrNy_le : f @ F --> -oo → ∀ A, \∀ x \near F , A ≥ f x.

Lemma cvgrNy_lt : f @ F --> -oo → ∀ A, \∀ x \near F , A > f x.

End cvg_infty_realField.

Lemma cvgrnyP {R : realType} {T} {F : set (set T)} {FF : Filter F} (f : T → nat) :
   (((f n)%:R : R ) @[n --> F ] --> +oo ) ↔ (f @ F --> \oo ).

Section ecvg_infty_numField.
Local Open Scope ereal_scope.

Context {R : numFieldType}.

Let cvgeyPnum {F : set (set \bar R)} {FF : Filter F} : [<->
F --> +oo;
∀ A, A \is Num.real → \∀ x \near F , A %:E ≤ x;
∀ A, A \is Num.real → \∀ x \near F , A %:E < x;
\∀ A \near +oo%R, \∀ x \near F , A %:E < x;
\∀ A \near +oo%R, \∀ x \near F , A %:E ≤ x ].

Let cvgeNyPnum {F : set (set \bar R)} {FF : Filter F} : [<->
F --> -oo;
∀ A, A \is Num.real → \∀ x \near F , A %:E ≥ x;
∀ A, A \is Num.real → \∀ x \near F , A %:E > x;
\∀ A \near -oo%R, \∀ x \near F , A %:E > x;
\∀ A \near -oo%R, \∀ x \near F , A %:E ≥ x ].

Context {T} {F : set (set T)} {FF : Filter F}.
Implicit Types (f : T → \bar R) (u : T → R).

Lemma cvgeyPger f :
  f @ F --> +oo ↔ ∀ A, A \is Num.real → \∀ x \near F , A %:E ≤ f x.

Lemma cvgeyPgtr f :
  f @ F --> +oo ↔ ∀ A, A \is Num.real → \∀ x \near F , A %:E < f x.

Lemma cvgeyPgty f :
  f @ F --> +oo ↔ \∀ A \near +oo%R, \∀ x \near F , A %:E < f x.

Lemma cvgeyPgey f :
  f @ F --> +oo ↔ \∀ A \near +oo%R, \∀ x \near F , A %:E ≤ f x.

Lemma cvgeNyPler f :
  f @ F --> -oo ↔ ∀ A, A \is Num.real → \∀ x \near F , A %:E ≥ f x.

Lemma cvgeNyPltr f :
  f @ F --> -oo ↔ ∀ A, A \is Num.real → \∀ x \near F , A %:E > f x.

Lemma cvgeNyPltNy f :
  f @ F --> -oo ↔ \∀ A \near -oo%R, \∀ x \near F , A %:E > f x.

Lemma cvgeNyPleNy f :
  f @ F --> -oo ↔ \∀ A \near -oo%R, \∀ x \near F , A %:E ≥ f x.

Lemma cvgey_ger f :
  f @ F --> +oo → ∀ A, A \is Num.real → \∀ x \near F , A %:E ≤ f x.

Lemma cvgey_gtr f :
  f @ F --> +oo → ∀ A, A \is Num.real → \∀ x \near F , A %:E < f x.

Lemma cvgeNy_ler f :
  f @ F --> -oo → ∀ A, A \is Num.real → \∀ x \near F , A %:E ≥ f x.

Lemma cvgeNy_ltr f :
  f @ F --> -oo → ∀ A, A \is Num.real → \∀ x \near F , A %:E > f x.

Lemma cvgNey f : (\- f @ F --> +oo ) ↔ (f @ F --> -oo ).

Lemma cvgNeNy f : (\- f @ F --> -oo ) ↔ (f @ F --> +oo ).

Lemma cvgeryP u : ((u x )%:E @[x --> F ] --> +oo ) ↔ (u @ F --> +oo%R).

Lemma cvgerNyP u : ((u x )%:E @[x --> F ] --> -oo ) ↔ (u @ F --> -oo%R).

End ecvg_infty_numField.

Section ecvg_infty_realField.
Local Open Scope ereal_scope.
Context {R : realFieldType}.
Context {T} {F : set (set T)} {FF : Filter F} (f : T → \bar R).

Lemma cvgeyPge : f @ F --> +oo ↔ ∀ A, \∀ x \near F , A %:E ≤ f x.

Lemma cvgeyPgt : f @ F --> +oo ↔ ∀ A, \∀ x \near F , A %:E < f x.

Lemma cvgeNyPle : f @ F --> -oo ↔ ∀ A, \∀ x \near F , A %:E ≥ f x.

Lemma cvgeNyPlt : f @ F --> -oo ↔ ∀ A, \∀ x \near F , A %:E > f x.

Lemma cvgey_ge : f @ F --> +oo → ∀ A, \∀ x \near F , A %:E ≤ f x.

Lemma cvgey_gt : f @ F --> +oo → ∀ A, \∀ x \near F , A %:E < f x.

Lemma cvgeNy_le : f @ F --> -oo → ∀ A, \∀ x \near F , A %:E ≥ f x.

Lemma cvgeNy_lt : f @ F --> -oo → ∀ A, \∀ x \near F , A %:E > f x.

End ecvg_infty_realField.

Lemma cvgenyP {R : realType} {T} {F : set (set T)} {FF : Filter F} (f : T → nat) :
   (((f n)%:R : R )%:E @[n --> F ] --> +oo%E) ↔ (f @ F --> \oo ).

Modules with a norm

realType

rcfType

Canonical rcf_lmodType.
Canonical rcf_lalgType.
Canonical rcf_algType.
Canonical rcf_comAlgType.
Canonical rcf_unitAlgType.
Canonical rcf_comUnitAlgType.
Canonical rcf_vectType.
Canonical rcf_FalgType.
Canonical rcf_fieldExtType.
Canonical rcf_pseudoMetricNormedZmodType.
Canonical rcf_normedModType.
Coercion rcf_lmodType : rcfType >-> lmodType.
Coercion rcf_lalgType : rcfType >-> lalgType.
Coercion rcf_algType : rcfType >-> algType.
Coercion rcf_comAlgType : rcfType >-> comAlgType.
Coercion rcf_unitAlgType : rcfType >-> unitAlgType.
Coercion rcf_comUnitAlgType : rcfType >-> comUnitAlgType.
Coercion rcf_vectType : rcfType >-> vectType.
Coercion rcf_FalgType : rcfType >-> FalgType.
Coercion rcf_fieldExtType : rcfType >-> fieldExtType.
Coercion rcf_pseudoMetricNormedZmodType :
rcfType >-> pseudoMetricNormedZmodType.
Coercion rcf_normedModType : rcfType >-> normedModType.

archiFieldType

realFieldType

numClosedFieldType

numFieldType

if we do not give the V argument to nbhs, the universally quantified set that appears inside the notation for cvg_to has type set (let '{| PseudoMetricNormedZmodule.sort := T |} := V in T) instead of set V, which causes an inference problem in derive.v

Lemma nbhs_nbhs_norm : nbhs_norm = nbhs.

Lemma nbhs_normP x (P : V → Prop) : (\near x , P x ) ↔ nbhs_norm x P.

Lemma nbhs_le_nbhs_norm (x : V) : @nbhs V _ x `=>` nbhs_norm x.

Lemma nbhs_norm_le_nbhs x : nbhs_norm x `=>` nbhs x.

Lemma filter_from_norm_nbhs x :
  @filter_from R _ [set x : R | 0 < x ] (ball_norm x) = nbhs x.

Lemma nbhs_normE (x : V) (P : V → Prop) :
  nbhs_norm x P = \near x , P x.

Lemma filter_from_normE (x : V) (P : V → Prop) :
  @filter_from R _ [set x : R | 0 < x ] (ball_norm x) P = \near x , P x.

Lemma near_nbhs_norm (x : V) (P : V → Prop) :
  (\∀ x \near nbhs_norm x , P x ) = \near x , P x.

Lemma nbhs_norm_ball_norm x (e : {posnum R }) :
  nbhs_norm x (ball_norm x e %:num).

Lemma nbhs_ball_norm (x : V) (eps : {posnum R }) : nbhs x (ball_norm x eps %:num).

Lemma ball_norm_dec x y (e : R) : {ball_norm x e y } + {¬ ball_norm x e y }.

Lemma ball_norm_sym x y (e : R) : ball_norm x e y → ball_norm y e x.

Lemma ball_norm_le x (e1 e2 : R) :
  e1 ≤ e2 → ball_norm x e1 `<=` ball_norm x e2.

Let nbhs_simpl := (nbhs_simpl ,@nbhs_nbhs_norm ,@filter_from_norm_nbhs ).

Lemma fcvgrPdist_lt {F : set (set V)} {FF : Filter F} (y : V) :
  F --> y ↔ ∀ eps, 0 < eps → \∀ y' \near F , `|y - y'| < eps.

Lemma cvgrPdist_lt {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y ↔ ∀ eps, 0 < eps → \∀ t \near F , `|y - f t| < eps.

Lemma cvgrPdistC_lt {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y ↔ ∀ eps, 0 < eps → \∀ t \near F , `|f t - y| < eps.

Lemma cvgr_dist_lt {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y → ∀ eps, eps > 0 → \∀ t \near F , `|y - f t| < eps.

Lemma __deprecated__cvg_dist {F : set (set V)} {FF : Filter F} (y : V) :
  F --> y → ∀ eps, eps > 0 → \∀ y' \near F , `|y - y'| < eps.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgr_dist_lt` or a variation instead")]
Notation cvg_dist := __deprecated__cvg_dist.

Lemma cvgr_distC_lt {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y → ∀ eps, eps > 0 → \∀ t \near F , `|f t - y| < eps.

Lemma cvgr_dist_le {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y → ∀ eps, eps > 0 → \∀ t \near F , `|y - f t| ≤ eps.

Lemma cvgr_distC_le {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y → ∀ eps, eps > 0 → \∀ t \near F , `|f t - y| ≤ eps.

Lemma nbhs_norm0P {P : V → Prop} :
  (\∀ x \near 0, P x ) ↔
  filter_from [set e | 0 < e ] (fun e ⇒ [set y | `|y| < e ]) P.

Lemma cvgr0Pnorm_lt {T} {F : set (set T)} {FF : Filter F} (f : T → V) :
  f @ F --> 0 ↔ ∀ eps, 0 < eps → \∀ t \near F , `|f t| < eps.

Lemma cvgr0_norm_lt {T} {F : set (set T)} {FF : Filter F} (f : T → V) :
  f @ F --> 0 → ∀ eps, eps > 0 → \∀ t \near F , `|f t| < eps.

Lemma cvgr0_norm_le {T} {F : set (set T)} {FF : Filter F} (f : T → V) :
  f @ F --> 0 → ∀ eps, eps > 0 → \∀ t \near F , `|f t| ≤ eps.

Lemma nbhs0_lt e : 0 < e → \∀ x \near (0 : V ), `|x| < e.

Lemma dnbhs0_lt e : 0 < e → \∀ x \near (0 : V )^', `|x| < e.

Lemma nbhs0_le e : 0 < e → \∀ x \near (0 : V ), `|x| ≤ e.

Lemma dnbhs0_le e : 0 < e → \∀ x \near (0 : V )^', `|x| ≤ e.

Lemma nbhs_norm_ball x (eps : {posnum R }) : nbhs_norm x (ball x eps %:num).

Lemma nbhsDl (P : set V) (x y : V) :
  (\∀ z \near (x + y ), P z ) ↔ (\near x , P (x + y)).

Lemma nbhsDr (P : set V) x y :
  (\∀ z \near (x + y ), P z ) ↔ (\near y , P (x + y)).

Lemma nbhs0P (P : set V) x : (\near x , P x ) ↔ (\∀ e \near 0, P (x + e)).

End PseudoNormedZmod_numDomainType.
#[global] Hint Resolve normr_ge0 : core.
Arguments cvgr_dist_lt {_ _ _ F FF}.
Arguments cvgr_distC_lt {_ _ _ F FF}.
Arguments cvgr_dist_le {_ _ _ F FF}.
Arguments cvgr_distC_le {_ _ _ F FF}.
Arguments cvgr0_norm_lt {_ _ _ F FF}.
Arguments cvgr0_norm_le {_ _ _ F FF}.

#[global] Hint Extern 0 (is_true (`|_ - ?x| < _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr_dist_lt end : core.
#[global] Hint Extern 0 (is_true (`|?x - _| < _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr_distC_lt end : core.
#[global] Hint Extern 0 (is_true (`|?x| < _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr0_norm_lt end : core.
#[global] Hint Extern 0 (is_true (`|_ - ?x| ≤ _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr_dist_le end : core.
#[global] Hint Extern 0 (is_true (`|?x - _| ≤ _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr_distC_le end : core.
#[global] Hint Extern 0 (is_true (`|?x| ≤ _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr0_norm_le end : core.

#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgrPdist_lt` or a variation instead")]
Notation cvg_distP := fcvgrPdist_lt.

Section open_closed_sets.

TODO: duplicate theory within the subspace topology of Num.real in a numDomainType

Variable R : realFieldType.

Some open sets of [R]

Lemma open_lt (y : R) : open [set x : R | x < y ].
Hint Resolve open_lt : core.

Lemma open_gt (y : R) : open [set x : R | x > y ].
Hint Resolve open_gt : core.

Lemma open_neq (y : R) : open [set x : R | x != y ].

Lemma interval_open a b : ~~ bound_side true a → ~~ bound_side false b →
open [set x : R^o | x \in Interval a b ].

Some closed sets of [R] TODO: we can probably extend these results to numFieldType by adding a precondition that y \is Num.real

Lemma closed_le (y : R) : closed [set x : R | x ≤ y ].

Lemma closed_ge (y : R) : closed [set x : R | y ≤ x ].

Lemma closed_eq (y : R) : closed [set x : R | x = y ].

Lemma interval_closed a b : ~~ bound_side false a → ~~ bound_side true b →
  closed [set x : R^o | x \in Interval a b ].

End open_closed_sets.

#[global] Hint Extern 0 (open _) ⇒ now apply: open_gt : core.
#[global] Hint Extern 0 (open _) ⇒ now apply: open_lt : core.
#[global] Hint Extern 0 (open _) ⇒ now apply: open_neq : core.
#[global] Hint Extern 0 (closed _) ⇒ now apply: closed_ge : core.
#[global] Hint Extern 0 (closed _) ⇒ now apply: closed_le : core.
#[global] Hint Extern 0 (closed _) ⇒ now apply: closed_eq : core.

Section at_left_right.
Variable R : numFieldType.

Definition at_left (x : R) := within (fun u ⇒ u < x) (nbhs x).
Definition at_right (x : R) := within (fun u ⇒ x < u) (nbhs x).

Global Instance at_right_proper_filter (x : R) : ProperFilter x ^'+.

Global Instance at_left_proper_filter (x : R) : ProperFilter x ^'-.

Lemma nbhs_right0P x (P : set R) :
  (\∀ y \near x ^'+, P y ) ↔ \∀ e \near 0^'+, P (x + e).

Lemma nbhs_left0P x (P : set R) :
  (\∀ y \near x ^'-, P y ) ↔ \∀ e \near 0^'+, P (x - e).

Lemma nbhs_right_gt x : \∀ y \near x ^'+, x < y.

Lemma nbhs_left_lt x : \∀ y \near x ^'-, y < x.

Lemma nbhs_right_neq x : \∀ y \near x ^'+, y != x.

Lemma nbhs_left_neq x : \∀ y \near x ^'-, y != x.

Lemma nbhs_right_ge x : \∀ y \near x ^'+, x ≤ y.

Lemma nbhs_left_le x : \∀ y \near x ^'-, y ≤ x.

Lemma nbhs_right_lt x z : x < z → \∀ y \near x ^'+, y < z.

Lemma nbhs_right_le x z : x < z → \∀ y \near x ^'+, y ≤ z.

Lemma nbhs_left_gt x z : z < x → \∀ y \near x ^'-, z < y.

Lemma nbhs_left_ge x z : z < x → \∀ y \near x ^'-, z ≤ y.

End at_left_right.
#[global] Typeclasses Opaque at_left at_right.
Notation "x ^'-" := (at_left x) : classical_set_scope.
Notation "x ^'+" := (at_right x) : classical_set_scope.

Section at_left_right_topologicalType.
Variables (R : numFieldType) (V : topologicalType) (f : R → V) (x : R).

Lemma cvg_at_right_filter : f z @[z --> x ] --> f x → f z @[z --> x ^'+] --> f x.

Lemma cvg_at_left_filter : f z @[z --> x ] --> f x → f z @[z --> x ^'-] --> f x.

Lemma cvg_at_right_within : f x @[x --> x ^'+] --> f x →
  f x @[x --> within (fun u ⇒ x ≤ u) (nbhs x)] --> f x.

Lemma cvg_at_left_within : f x @[x --> x ^'-] --> f x →
  f x @[x --> within (fun u ⇒ u ≤ x) (nbhs x)] --> f x.

End at_left_right_topologicalType.

Section at_left_right_pmNormedZmod.
Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R).

Lemma nbhsr0P (P : set V) x :
  (\∀ y \near x , P y ) ↔
  (\∀ e \near 0^'+, ∀ y, `|x - y| ≤ e → P y ).

Let cvgrP {F : set (set V)} {FF : Filter F} (y : V) : [<->
  F --> y;
  ∀ eps, 0 < eps → \∀ t \near F , `|y - t| ≤ eps;
  \∀ eps \near 0^'+, \∀ t \near F , `|y - t| ≤ eps;
  \∀ eps \near 0^'+, \∀ t \near F , `|y - t| < eps].

Lemma cvgrPdist_le {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y ↔ ∀ eps, 0 < eps → \∀ t \near F , `|y - f t| ≤ eps.

Lemma cvgrPdist_ltp {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y ↔ \∀ eps \near 0^'+, \∀ t \near F , `|y - f t| < eps.

Lemma cvgrPdist_lep {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y ↔ \∀ eps \near 0^'+, \∀ t \near F , `|y - f t| ≤ eps.

Lemma cvgrPdistC_le {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y ↔ ∀ eps, 0 < eps → \∀ t \near F , `|f t - y| ≤ eps.

Lemma cvgrPdistC_ltp {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y ↔ \∀ eps \near 0^'+, \∀ t \near F , `|f t - y| < eps.

Lemma cvgrPdistC_lep {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y ↔ \∀ eps \near 0^'+, \∀ t \near F , `|f t - y| ≤ eps.

Lemma cvgr0Pnorm_le {T} {F : set (set T)} {FF : Filter F} (f : T → V) :
  f @ F --> 0 ↔ ∀ eps, 0 < eps → \∀ t \near F , `|f t| ≤ eps.

Lemma cvgr0Pnorm_ltp {T} {F : set (set T)} {FF : Filter F} (f : T → V) :
  f @ F --> 0 ↔ \∀ eps \near 0^'+, \∀ t \near F , `|f t| < eps.

Lemma cvgr0Pnorm_lep {T} {F : set (set T)} {FF : Filter F} (f : T → V) :
  f @ F --> 0 ↔ \∀ eps \near 0^'+, \∀ t \near F , `|f t| ≤ eps.

Lemma cvgr_norm_lt {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y → ∀ u, `|y| < u → \∀ t \near F , `|f t| < u.

Lemma cvgr_norm_le {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y → ∀ u, `|y| < u → \∀ t \near F , `|f t| ≤ u.

Lemma cvgr_norm_gt {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y → ∀ u, `|y| > u → \∀ t \near F , `|f t| > u.

Lemma cvgr_norm_ge {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y → ∀ u, `|y| > u → \∀ t \near F , `|f t| ≥ u.

Lemma cvgr_neq0 {T} {F : set (set T)} {FF : Filter F} (f : T → V) (y : V) :
  f @ F --> y → y != 0 → \∀ t \near F , f t != 0.

End at_left_right_pmNormedZmod.
Arguments cvgr_norm_lt {R V T F FF f}.
Arguments cvgr_norm_le {R V T F FF f}.
Arguments cvgr_norm_gt {R V T F FF f}.
Arguments cvgr_norm_ge {R V T F FF f}.
Arguments cvgr_neq0 {R V T F FF f}.

#[global] Hint Extern 0 (is_true (`|_ - ?x| < _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr_dist_lt end : core.
#[global] Hint Extern 0 (is_true (`|?x - _| < _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr_distC_lt end : core.
#[global] Hint Extern 0 (is_true (`|?x| < _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr0_norm_lt end : core.
#[global] Hint Extern 0 (is_true (`|_ - ?x| ≤ _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr_dist_le end : core.
#[global] Hint Extern 0 (is_true (`|?x - _| ≤ _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr_distC_le end : core.
#[global] Hint Extern 0 (is_true (`|?x| ≤ _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: cvgr0_norm_le end : core.

#[global] Hint Extern 0 (is_true (_ < ?x)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_right_gt end : core.
#[global] Hint Extern 0 (is_true (?x < _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_left_lt end : core.
#[global] Hint Extern 0 (is_true (?x != _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_right_neq end : core.
#[global] Hint Extern 0 (is_true (?x != _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_left_neq end : core.
#[global] Hint Extern 0 (is_true (_ < ?x)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_left_gt end : core.
#[global] Hint Extern 0 (is_true (?x < _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_right_lt end : core.
#[global] Hint Extern 0 (is_true (_ ≤ ?x)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_right_ge end : core.
#[global] Hint Extern 0 (is_true (?x ≤ _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_left_le end : core.
#[global] Hint Extern 0 (is_true (_ ≤ ?x)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_right_ge end : core.
#[global] Hint Extern 0 (is_true (?x ≤ _)) ⇒ match goal with
  H : x \is_near _ |- _ ⇒ near: x; exact: nbhs_left_le end : core.

#[global] Hint Extern 0 (ProperFilter _^'-) ⇒
  (apply: at_left_proper_filter) : typeclass_instances.
#[global] Hint Extern 0 (ProperFilter _^'+) ⇒
  (apply: at_right_proper_filter) : typeclass_instances.

Section at_left_rightR.
Variable (R : numFieldType).

Lemma real_cvgr_lt {T} {F : set (set T)} {FF : Filter F} (f : T → R) (y : R) :
    y \is Num.real → f @ F --> y →
  ∀ z, z > y → \∀ t \near F , f t \is Num.real → f t < z.

Lemma real_cvgr_le {T} {F : set (set T)} {FF : Filter F} (f : T → R) (y : R) :
    y \is Num.real → f @ F --> y →
  ∀ z, z > y → \∀ t \near F , f t \is Num.real → f t ≤ z.

Lemma real_cvgr_gt {T} {F : set (set T)} {FF : Filter F} (f : T → R) (y : R) :
    y \is Num.real → f @ F --> y →
  ∀ z, y > z → \∀ t \near F , f t \is Num.real → f t > z.

Lemma real_cvgr_ge {T} {F : set (set T)} {FF : Filter F} (f : T → R) (y : R) :
    y \is Num.real → f @ F --> y →
  ∀ z, z < y → \∀ t \near F , f t \is Num.real → f t ≥ z.

End at_left_rightR.
Arguments real_cvgr_le {R T F FF f}.
Arguments real_cvgr_lt {R T F FF f}.
Arguments real_cvgr_ge {R T F FF f}.
Arguments real_cvgr_gt {R T F FF f}.

Section realFieldType.
Context (R : realFieldType).

Lemma at_right_in_segment (x : R) (P : set R) :
  (\∀ e \near 0^'+, {in `[x - e, x + e], ∀ x, P x }) ↔ (\near x , P x ).

Lemma cvgr_lt {T} {F : set (set T)} {FF : Filter F} (f : T → R) (y : R) :
  f @ F --> y → ∀ z, z > y → \∀ t \near F , f t < z.

Lemma cvgr_le {T} {F : set (set T)} {FF : Filter F} (f : T → R) (y : R) :
  f @ F --> y → ∀ z, z > y → \∀ t \near F , f t ≤ z.

Lemma cvgr_gt {T} {F : set (set T)} {FF : Filter F} (f : T → R) (y : R) :
  f @ F --> y → ∀ z, y > z → \∀ t \near F , f t > z.

Lemma cvgr_ge {T} {F : set (set T)} {FF : Filter F} (f : T → R) (y : R) :
  f @ F --> y → ∀ z, z < y → \∀ t \near F , f t ≥ z.

End realFieldType.
Arguments cvgr_le {R T F FF f}.
Arguments cvgr_lt {R T F FF f}.
Arguments cvgr_ge {R T F FF f}.
Arguments cvgr_gt {R T F FF f}.

Definition self_sub (K : numDomainType) (V W : normedModType K)
  (f : V → W) (x : V × V) : W := f x .1 - f x .2.
Arguments self_sub {K V W} f x /.

Definition fun1 {T : Type} {K : numFieldType} : T → K := fun ⇒ 1.
Arguments fun1 {T K} x /.

Definition dominated_by {T : Type} {K : numDomainType} {V W : pseudoMetricNormedZmodType K}
  (h : T → V) (k : K) (f : T → W) (F : set (set T)) :=
  F [set x | `|f x| ≤ k × `|h x|].

Definition strictly_dominated_by {T : Type} {K : numDomainType} {V W : pseudoMetricNormedZmodType K}
  (h : T → V) (k : K) (f : T → W) (F : set (set T)) :=
  F [set x | `|f x| < k × `|h x|].

Lemma sub_dominatedl (T : Type) (K : numDomainType) (V W : pseudoMetricNormedZmodType K)
   (h : T → V) (k : K) (F G : set (set T)) : F `=>` G →
  (@dominated_by T K V W h k )^~ G `<=` (dominated_by h k )^~ F.

Lemma sub_dominatedr (T : Type) (K : numDomainType) (V : pseudoMetricNormedZmodType K)
    (h : T → V) (k : K) (f g : T → V) (F : set (set T)) (FF : Filter F) :
   (\∀ x \near F , `|f x| ≤ `|g x|) →
   dominated_by h k g F → dominated_by h k f F.

Lemma dominated_by1 {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K} :
  @dominated_by T K _ V fun1 = fun k f F ⇒ F [set x | `|f x| ≤ k ].

Lemma strictly_dominated_by1 {T : Type} {K : numFieldType}
    {V : pseudoMetricNormedZmodType K} :
  @strictly_dominated_by T K _ V fun1 = fun k f F ⇒ F [set x | `|f x| < k ].

Lemma ex_dom_bound {T : Type} {K : numFieldType} {V W : pseudoMetricNormedZmodType K}
    (h : T → V) (f : T → W) (F : set (set T)) {PF : ProperFilter F}:
  (\∀ M \near +oo , dominated_by h M f F ) ↔
  ∃ M , dominated_by h M f F.

Lemma ex_strict_dom_bound {T : Type} {K : numFieldType}
    {V W : pseudoMetricNormedZmodType K}
    (h : T → V) (f : T → W) (F : set (set T)) {PF : ProperFilter F} :
  (\∀ x \near F , h x != 0) →
  (\∀ M \near +oo , dominated_by h M f F ) ↔
   ∃ M , strictly_dominated_by h M f F.

Definition bounded_near {T : Type} {K : numFieldType}
    {V : pseudoMetricNormedZmodType K}
  (f : T → V) (F : set (set T)) :=
  \∀ M \near +oo , F [set x | `|f x| ≤ M ].

Lemma boundedE {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K} :
  @bounded_near T K V = fun f F ⇒ \∀ M \near +oo , dominated_by fun1 M f F.

Lemma sub_boundedr (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K)
     (F G : set (set T)) : F `=>` G →
  (@bounded_near T K V )^~ G `<=` bounded_near ^~ F.

Lemma sub_boundedl (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K)
     (f g : T → V) (F : set (set T)) (FF : Filter F) :
(\∀ x \near F , `|f x| ≤ `|g x|) → bounded_near g F → bounded_near f F.

Lemma ex_bound {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}
  (f : T → V) (F : set (set T)) {PF : ProperFilter F}:
  bounded_near f F ↔ ∃ M , F [set x | `|f x| ≤ M ].

Lemma ex_strict_bound {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}
  (f : T → V) (F : set (set T)) {PF : ProperFilter F}:
  bounded_near f F ↔ ∃ M , F [set x | `|f x| < M ].

Lemma ex_strict_bound_gt0 {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}
  (f : T → V) (F : set (set T)) {PF : Filter F}:
  bounded_near f F → exists2 M , M > 0 & F [set x | `|f x| < M ].

Notation "[ 'bounded' E | x 'in' A ]" :=
  (bounded_near (fun x ⇒ E) (globally A)).
Notation bounded_set := [set A | [bounded x | x in A ]].
Notation bounded_fun := [set f | [bounded f x | x in setT ]].

Lemma bounded_fun_has_ubound (T : Type) (R : realFieldType) (a : T → R) :
  bounded_fun a → has_ubound (range a).

Lemma bounded_funN (T : Type) (R : realFieldType) (a : T → R) :
  bounded_fun a → bounded_fun (- a).

Lemma bounded_fun_has_lbound (T : Type) (R : realFieldType) (a : T → R) :
  bounded_fun a → has_lbound (range a).

Lemma bounded_funD (T : Type) (R : realFieldType) (a b : T → R) :
  bounded_fun a → bounded_fun b → bounded_fun (a \+ b).

Lemma bounded_locally (T : topologicalType)
    (R : numFieldType) (V : normedModType R) (A : set T) (f : T → V) :
  [bounded f x | x in A ] → [locally [bounded f x | x in A ]].

Notation "k .-lipschitz_on f" :=
  (dominated_by (self_sub id) k (self_sub f)) : type_scope.

Definition sub_klipschitz (K : numFieldType) (V W : normedModType K) (k : K)
           (f : V → W) (F G : set (set (V × V))) :
  F `=>` G → k .-lipschitz_on f G → k .-lipschitz_on f F.

Definition lipschitz_on (K : numFieldType) (V W : normedModType K)
           (f : V → W) (F : set (set (V × V))) :=
  \∀ M \near +oo , M .-lipschitz_on f F.

Definition sub_lipschitz (K : numFieldType) (V W : normedModType K)
           (f : V → W) (F G : set (set (V × V))) :
  F `=>` G → lipschitz_on f G → lipschitz_on f F.

Lemma klipschitzW (K : numFieldType) (V W : normedModType K) (k : K)
      (f : V → W) (F : set (set (V × V))) {PF : ProperFilter F} :
  k .-lipschitz_on f F → lipschitz_on f F.

Notation "k .-lipschitz_ A f" :=
  (k.-lipschitz_on f (globally (A `*` A ))) : type_scope.
Notation "k .-lipschitz f" := (k.-lipschitz_setT f) : type_scope.
Notation "[ 'lipschitz' E | x 'in' A ]" :=
  (lipschitz_on (fun x ⇒ E) (globally (A `*` A))) : type_scope.
Notation lipschitz f := [lipschitz f x | x in setT ].

Lemma lipschitz_set0 (K : numFieldType) (V W : normedModType K)
  (f : V → W) : [lipschitz f x | x in set0 ].

Lemma lipschitz_set1 (K : numFieldType) (V W : normedModType K)
  (f : V → W) (a : V) : [lipschitz f x | x in [set a ]].

Lemma klipschitz_locally (R : numFieldType) (V W : normedModType R) (k : R)
    (f : V → W) (A : set V) :
  k .-lipschitz_A f → [locally k .-lipschitz_A f ].

Lemma lipschitz_locally (R : numFieldType) (V W : normedModType R)
    (A : set V) (f : V → W) :
  [lipschitz f x | x in A ] → [locally [lipschitz f x | x in A ]].

Lemma lipschitz_id (R : numFieldType) (V : normedModType R) :
  1.-lipschitz (@id V ).
Arguments lipschitz_id {R V}.

Section contractions.
Context {R : numDomainType} {X Y : normedModType R} {U : set X} {V : set Y}.

Definition contraction (q : {nonneg R }) (f : {fun U >-> V }) :=
  q %:num < 1 ∧ q %:num .-lipschitz_U f.

Definition is_contraction (f : {fun U >-> V }) := ∃ q , contraction q f.

End contractions.

Lemma contraction_fixpoint_unique {R : realDomainType}
    {X : normedModType R} (U : set X) (f : {fun U >-> U }) (x y : X) :
  is_contraction f → U x → U y → x = f x → y = f y → x = y.

Section PseudoNormedZMod_numFieldType.
Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R).

Lemma norm_hausdorff : hausdorff_space V.
Hint Extern 0 (hausdorff_space _) ⇒ solve[apply: norm_hausdorff] : core.

TODO: check if the following lemma are indeed useless i.e. where the generic lemma is applied, check that norm_hausdorff is not used in a hard way

Lemma norm_closeE (x y : V): close x y = (x = y ).
Lemma norm_close_eq (x y : V) : close x y → x = y.

Lemma norm_cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : V | F --> x ].

Lemma norm_cvg_eq (x y : V) : x --> y → x = y.
Lemma norm_lim_id (x : V) : lim x = x.

Lemma norm_cvg_lim {F} {FF : ProperFilter F} (l : V) : F --> l → lim F = l.

Lemma norm_lim_near_cst U {F} {FF : ProperFilter F} (l : V) (f : U → V) :
   (\∀ x \near F , f x = l ) → lim (f @ F) = l.

Lemma norm_lim_cst U {F} {FF : ProperFilter F} (k : V) :
   lim ((fun _ : U ⇒ k ) @ F) = k.

Lemma norm_cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U → set V) :
  {near F , is_fun f } → is_subset1 [set x : V | f `@ F --> x ].

Lemma norm_cvgi_lim {U} {F} {FF : ProperFilter F} (f : U → V → Prop) (l : V) :
  F (fun x : U ⇒ is_subset1 (f x)) →
  f `@ F --> l → lim (f `@ F) = l.

Lemma distm_lt_split (z x y : V) (e : R) :
  `|x - z| < e / 2 → `|z - y| < e / 2 → `|x - y| < e.

Lemma distm_lt_splitr (z x y : V) (e : R) :
  `|z - x| < e / 2 → `|z - y| < e / 2 → `|x - y| < e.

Lemma distm_lt_splitl (z x y : V) (e : R) :
  `|x - z| < e / 2 → `|y - z| < e / 2 → `|x - y| < e.

Lemma normm_leW (x : V) (e : R) : e > 0 → `|x| ≤ e / 2 → `|x| < e.

Lemma normm_lt_split (x y : V) (e : R) :
  `|x| < e / 2 → `|y| < e / 2 → `|x + y| < e.

Lemma __deprecated__cvg_distW {F : set (set V)} {FF : Filter F} (y : V) :
  (∀ eps, 0 < eps → \∀ y' \near F , `|y - y'| ≤ eps ) →
  F --> y.

End PseudoNormedZMod_numFieldType.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgrPdist_le` or a variation instead")]
Notation cvg_distW := __deprecated__cvg_distW.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `norm_cvgi_lim`")]
Notation norm_cvgi_map_lim := norm_cvgi_lim.

Section NormedModule_numFieldType.
Variables (R : numFieldType) (V : normedModType R).

Section cvgr_norm_infty.
Variables (I : Type) (F : set (set I)) (FF : Filter F) (f : I → V) (y : V).

Lemma cvgr_norm_lty :
  f @ F --> y → \∀ M \near +oo , \∀ y' \near F , `|f y'| < M.

Lemma cvgr_norm_ley :
  f @ F --> y → \∀ M \near +oo , \∀ y' \near F , `|f y'| ≤ M.

Lemma cvgr_norm_gtNy :
  f @ F --> y → \∀ M \near -oo , \∀ y' \near F , `|f y'| > M.

Lemma cvgr_norm_geNy :
  f @ F --> y → \∀ M \near -oo , \∀ y' \near F , `|f y'| ≥ M.

End cvgr_norm_infty.

Lemma __deprecated__cvg_bounded_real {F : set (set V)} {FF : Filter F} (y : V) :
  F --> y → \∀ M \near +oo , \∀ y' \near F , `|y'| < M.

Lemma cvg_bounded {I} {F : set (set I)} {FF : Filter F} (f : I → V) (y : V) :
  f @ F --> y → bounded_near f F.

End NormedModule_numFieldType.
Arguments cvgr_norm_lty {R V I F FF}.
Arguments cvgr_norm_ley {R V I F FF}.
Arguments cvgr_norm_gtNy {R V I F FF}.
Arguments cvgr_norm_geNy {R V I F FF}.
Arguments cvg_bounded {R V I F FF}.
#[global]
Hint Extern 0 (hausdorff_space _) ⇒ solve[apply: norm_hausdorff] : core.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgr_norm_lty` or a variation instead")]
Notation cvg_bounded_real := __deprecated__cvg_bounded_real.

Module Export NbhsNorm.
Definition nbhs_simpl := (nbhs_simpl ,@nbhs_nbhs_norm ,@filter_from_norm_nbhs ).
End NbhsNorm.

Section hausdorff.

Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.

Lemma pseudoMetricNormedZModType_hausdorff (R : realFieldType)
    (V : pseudoMetricNormedZmodType R) :
  hausdorff_space V.

End hausdorff.

Module Export NearNorm.
Definition near_simpl := (@near_simpl , @nbhs_normE , @filter_from_normE ,
  @near_nbhs_norm ).
Ltac near_simpl := rewrite ?near_simpl.
End NearNorm.

Lemma __deprecated__continuous_cvg_dist {R : numFieldType}
  (V W : pseudoMetricNormedZmodType R) (f : V → W) x l :
  continuous f → x --> l → ∀ e : {posnum R }, `|f l - f x| < e %:num.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="simply use the fact that `(x --> l) -> (x = l)`")]
Notation continuous_cvg_dist := __deprecated__continuous_cvg_dist.

Matrices

Section mx_norm.
Variables (K : numDomainType) (m n : nat).
Implicit Types x y : 'M[K]_(m, n).

Definition mx_norm x : K := (\big[maxr/0%:nng]_i `|x i .1 i .2|%:nng )%:num.

Lemma mx_normE x : mx_norm x = (\big[maxr/0%:nng]_i `|x i .1 i .2|%:nng )%:num.

Lemma ler_mx_norm_add x y : mx_norm (x + y) ≤ mx_norm x + mx_norm y.

Lemma mx_norm_eq0 x : mx_norm x = 0 → x = 0.

Lemma mx_norm0 : mx_norm 0 = 0.

Lemma mx_norm_neq0 x : mx_norm x != 0 → ∃ i , mx_norm x = `|x i .1 i .2|.

Lemma mx_norm_natmul x k : mx_norm (x *+ k) = (mx_norm x) *+ k.

Lemma mx_normN x : mx_norm (- x) = mx_norm x.

End mx_norm.

Lemma mx_normrE (K : realDomainType) (m n : nat) (x : 'M[K]_(m, n)) :
  mx_norm x = \big[maxr/0]_ij `|x ij .1 ij .2|.

Definition matrix_normedZmodMixin (K : numDomainType) (m n : nat) :=
  @Num.NormedMixin _ _ _ (@mx_norm K m.+1 n.+1) (@ler_mx_norm_add _ _ _)
    (@mx_norm_eq0 _ _ _) (@mx_norm_natmul _ _ _) (@mx_normN _ _ _).

Canonical matrix_normedZmodType (K : numDomainType) (m n : nat) :=
  NormedZmodType K 'M[K]_(m.+1, n.+1) (matrix_normedZmodMixin K m n).

Section matrix_NormedModule.
Variables (K : numFieldType) (m n : nat).

Lemma mx_norm_ball :
  @ball _ [pseudoMetricType K of 'M[K]_(m.+1, n.+1)] = ball_ (fun x ⇒ `| x |).

Definition matrix_PseudoMetricNormedZmodMixin :=
  PseudoMetricNormedZmodule.Mixin mx_norm_ball.
Canonical matrix_pseudoMetricNormedZmodType :=
  PseudoMetricNormedZmodType K 'M[K]_(m.+1, n.+1) matrix_PseudoMetricNormedZmodMixin.

Lemma mx_normZ (l : K) (x : 'M[K]_(m.+1, n.+1)) : `| l *: x | = `| l | × `| x |.

Definition matrix_NormedModMixin := NormedModMixin mx_normZ.
Canonical matrix_normedModType :=
  NormedModType K 'M[K]_(m.+1, n.+1) matrix_NormedModMixin.

End matrix_NormedModule.

Pairs

Section prod_PseudoMetricNormedZmodule.
Context {K : numDomainType} {U V : pseudoMetricNormedZmodType K}.

Lemma ball_prod_normE : ball = ball_ (fun x ⇒ `| x : U × V |).

Lemma prod_norm_ball : @ball _ [pseudoMetricType K of U × V ] = ball_ (fun x ⇒ `|x|).

Definition prod_pseudoMetricNormedZmodMixin :=
  PseudoMetricNormedZmodule.Mixin prod_norm_ball.
Canonical prod_pseudoMetricNormedZmodType :=
  PseudoMetricNormedZmodType K (U × V) prod_pseudoMetricNormedZmodMixin.

End prod_PseudoMetricNormedZmodule.

Section prod_NormedModule.
Context {K : numDomainType} {U V : normedModType K}.

Lemma prod_norm_scale (l : K) (x : U × V) : `| l *: x | = `|l| × `| x |.

Definition prod_NormedModMixin := NormedModMixin prod_norm_scale.
Canonical prod_normedModType :=
  NormedModType K (U × V) prod_NormedModMixin.

End prod_NormedModule.

Section example_of_sharing.
Variables (K : numDomainType).

Example matrix_triangke m n (M N : 'M[K]_(m.+1, n.+1)) :
  `|M + N| ≤ `|M| + `|N|.

Example pair_triangle (x y : K × K) : `|x + y| ≤ `|x| + `|y|.

End example_of_sharing.

Section prod_NormedModule_lemmas.

Context {T : Type} {K : numDomainType} {U V : normedModType K}.

Lemma fcvgr2dist_ltP {F : set (set U)} {G : set (set V)}
  {FF : Filter F} {FG : Filter G} (y : U) (z : V) :
  (F , G ) --> (y , z ) ↔
  ∀ eps, 0 < eps →
   \∀ y' \near F & z' \near G , `| (y , z ) - (y', z') | < eps.

Lemma cvgr2dist_ltP {I J} {F : set (set I)} {G : set (set J)}
  {FF : Filter F} {FG : Filter G} (f : I → U) (g : J → V) (y : U) (z : V) :
  (f @ F , g @ G ) --> (y , z ) ↔
  ∀ eps, 0 < eps →
   \∀ i \near F & j \near G , `| (y , z ) - (f i , g j ) | < eps.

Lemma cvgr2dist_lt {I J} {F : set (set I)} {G : set (set J)}
  {FF : Filter F} {FG : Filter G} (f : I → U) (g : J → V) (y : U) (z : V) :
  (f @ F , g @ G ) --> (y , z ) →
  ∀ eps, 0 < eps →
   \∀ i \near F & j \near G , `| (y , z ) - (f i , g j ) | < eps.

Lemma __deprecated__cvg_dist2 {F : set (set U)} {G : set (set V)}
  {FF : Filter F} {FG : Filter G} (y : U) (z : V):
  (F , G ) --> (y , z ) →
  ∀ eps, 0 < eps →
   \∀ y' \near F & z' \near G , `|(y , z ) - (y', z')| < eps.
#[deprecated(since="mathcomp-analysis 0.6.0",
note="use `cvgr2dist_lt` or a variant instead")]
Notation cvg_dist2 := __deprecated__cvg_dist2.

End prod_NormedModule_lemmas.
Arguments cvgr2dist_ltP {_ _ _ _ _ F G FF FG}.
Arguments cvgr2dist_lt {_ _ _ _ _ F G FF FG}.

#[deprecated(since="mathcomp-analysis 0.6.0",
note="use `fcvgr2dist_ltP` or a variant instead")]
Notation cvg_dist2P := fcvgr2dist_ltP.

Normed vector spaces have some continuous functions that are in fact continuous on pseudoMetricNormedZmodType

Section NVS_continuity_pseudoMetricNormedZmodType.
Context {K : numFieldType} {V : pseudoMetricNormedZmodType K}.

Lemma opp_continuous : continuous (@GRing.opp V).

Lemma add_continuous : continuous (fun z : V × V ⇒ z .1 + z .2).

Lemma natmul_continuous n : continuous (fun x : V ⇒ x *+ n).

Lemma norm_continuous : continuous (normr : V → K).

End NVS_continuity_pseudoMetricNormedZmodType.

Section NVS_continuity_normedModType.
Context {K : numFieldType} {V : normedModType K}.

Lemma scale_continuous : continuous (fun z : K × V ⇒ z .1 *: z .2).

Arguments scale_continuous _ _ : clear implicits.

Lemma scaler_continuous k : continuous (fun x : V ⇒ k *: x).

Lemma scalel_continuous (x : V) : continuous (fun k : K ⇒ k *: x).

Continuity of norm

End NVS_continuity_normedModType.

Section NVS_continuity_mul.

Context {K : numFieldType}.

Lemma mul_continuous : continuous (fun z : K × K ⇒ z .1 × z .2).

Lemma mulrl_continuous (x : K) : continuous ( *%R x).

Lemma mulrr_continuous (y : K) : continuous ( *%R^~ y).

Lemma inv_continuous (x : K) : x != 0 → {for x , continuous GRing.inv}.

End NVS_continuity_mul.

Section cvg_composition_pseudometric.

Context {K : numFieldType} {V : pseudoMetricNormedZmodType K} {T : Type}.
Context (F : set (set T)) {FF : Filter F}.
Implicit Types (f g : T → V) (s : T → K) (k : K) (x : T) (a b : V).

Lemma cvgN f a : f @ F --> a → - f @ F --> - a.

Lemma cvgNP f a : - f @ F --> - a ↔ f @ F --> a.

Lemma is_cvgN f : cvg (f @ F) → cvg (- f @ F).

Lemma is_cvgNE f : cvg ((- f ) @ F) = cvg (f @ F).

Lemma cvgMn f n a : f @ F --> a → ((@GRing.natmul _)^~n \o f ) @ F --> a *+ n.

Lemma is_cvgMn f n : cvg (f @ F) → cvg (((@GRing.natmul _)^~n \o f ) @ F).

Lemma cvgD f g a b : f @ F --> a → g @ F --> b → (f + g ) @ F --> a + b.

Lemma is_cvgD f g : cvg (f @ F) → cvg (g @ F) → cvg (f + g @ F).

Lemma cvgB f g a b : f @ F --> a → g @ F --> b → (f - g ) @ F --> a - b.

Lemma is_cvgB f g : cvg (f @ F) → cvg (g @ F) → cvg (f - g @ F).

Lemma is_cvgDlE f g : cvg (g @ F) → cvg ((f + g ) @ F) = cvg (f @ F).

Lemma is_cvgDrE f g : cvg (f @ F) → cvg ((f + g ) @ F) = cvg (g @ F).

Lemma cvg_sub0 f g a : (f - g ) @ F --> (0 : V ) → g @ F --> a → f @ F --> a.

Lemma cvg_zero f a : (f - cst a ) @ F --> (0 : V ) → f @ F --> a.

Lemma cvg_norm f a : f @ F --> a → `|f x| @[x --> F ] --> (`|a| : K ).

Lemma is_cvg_norm f : cvg (f @ F) → cvg ((Num.norm \o f : T → K ) @ F).

Lemma norm_cvg0P f : `|f x| @[x --> F ] --> 0 ↔ f @ F --> 0.

Lemma norm_cvg0 f : `|f x| @[x --> F ] --> 0 → f @ F --> 0.

End cvg_composition_pseudometric.

Lemma __deprecated__cvg_dist0 {U} {K : numFieldType} {V : normedModType K}
  {F : set (set U)} {FF : Filter F} (f : U → V) :
  (fun x ⇒ `|f x|) @ F --> (0 : K )
  → f @ F --> (0 : V ).
#[deprecated(since="mathcomp-analysis 0.6.0",
note="renamed to `norm_cvg0` and generalized to `pseudoMetricNormedZmodType`")]
Notation cvg_dist0 := __deprecated__cvg_dist0.

Section cvg_composition_normed.
Context {K : numFieldType} {V : normedModType K} {T : Type}.
Context (F : set (set T)) {FF : Filter F}.
Implicit Types (f g : T → V) (s : T → K) (k : K) (x : T) (a b : V).

Lemma cvgZ s f k a : s @ F --> k → f @ F --> a →
                     s x *: f x @[x --> F ] --> k *: a.

Lemma is_cvgZ s f : cvg (s @ F) →
  cvg (f @ F) → cvg ((fun x ⇒ s x *: f x ) @ F).

Lemma cvgZl s k a : s @ F --> k → s x *: a @[x --> F ] --> k *: a.

Lemma is_cvgZl s a : cvg (s @ F) → cvg ((fun x ⇒ s x *: a ) @ F).

Lemma cvgZr k f a : f @ F --> a → k \*: f @ F --> k *: a.

Lemma is_cvgZr k f : cvg (f @ F) → cvg (k *: f @ F).

Lemma is_cvgZrE k f : k != 0 → cvg (k *: f @ F) = cvg (f @ F).

End cvg_composition_normed.

Section cvg_composition_field.
Context {K : numFieldType} {T : Type}.
Context (F : set (set T)) {FF : Filter F}.
Implicit Types (f g : T → K) (a b : K).

Lemma cvgV f a : a != 0 → f @ F --> a → f \^-1 @ F --> a^-1.

Lemma cvgVP f a : a != 0 → f \^-1 @ F --> a^-1 ↔ f @ F --> a.

Lemma is_cvgV f : lim (f @ F) != 0 → cvg (f @ F) → cvg (f \^-1 @ F).

Lemma cvgM f g a b : f @ F --> a → g @ F --> b → (f \* g ) @ F --> a × b.

Lemma cvgMl f a b : f @ F --> a → (f x × b ) @[x --> F ] --> a × b.

Lemma cvgMr g a b : g @ F --> b → (a × g x ) @[x --> F ] --> a × b.

Lemma is_cvgM f g : cvg (f @ F) → cvg (g @ F) → cvg (f \* g @ F).

Lemma is_cvgMr g a (f := fun ⇒ a) : cvg (g @ F) → cvg (f \* g @ F).

Lemma is_cvgMrE g a (f := fun ⇒ a) : a != 0 → cvg (f \* g @ F) = cvg (g @ F).

Lemma is_cvgMl f a (g := fun ⇒ a) : cvg (f @ F) → cvg (f \* g @ F).

Lemma is_cvgMlE f a (g := fun ⇒ a) : a != 0 → cvg (f \* g @ F) = cvg (f @ F).

End cvg_composition_field.

Section limit_composition_pseudometric.

Context {K : numFieldType} {V : pseudoMetricNormedZmodType K} {T : Type}.
Context (F : set (set T)) {FF : ProperFilter F}.
Implicit Types (f g : T → V) (s : T → K) (k : K) (x : T) (a : V).

Lemma limN f : cvg (f @ F) → lim (- f @ F) = - lim (f @ F).

Lemma limD f g : cvg (f @ F) → cvg (g @ F) →
   lim (f + g @ F) = lim (f @ F) + lim (g @ F).

Lemma limB f g : cvg (f @ F) → cvg (g @ F) →
   lim (f - g @ F) = lim (f @ F) - lim (g @ F).

Lemma lim_norm f : cvg (f @ F) → lim ((fun x ⇒ `|f x| : K ) @ F) = `|lim (f @ F)|.

End limit_composition_pseudometric.

Section limit_composition_normed.

Context {K : numFieldType} {V : normedModType K} {T : Type}.
Context (F : set (set T)) {FF : ProperFilter F}.
Implicit Types (f g : T → V) (s : T → K) (k : K) (x : T) (a : V).

Lemma limZ s f : cvg (s @ F) → cvg (f @ F) →
   lim ((fun x ⇒ s x *: f x ) @ F) = lim (s @ F) *: lim (f @ F).

Lemma limZl s a : cvg (s @ F) →
   lim ((fun x ⇒ s x *: a ) @ F) = lim (s @ F) *: a.

Lemma limZr k f : cvg (f @ F) → lim (k *: f @ F) = k *: lim (f @ F).

End limit_composition_normed.

Section limit_composition_field.

Context {K : numFieldType} {T : Type}.
Context (F : set (set T)) {FF : ProperFilter F}.
Implicit Types (f g : T → K).

Lemma limM f g : cvg (f @ F) → cvg (g @ F) →
   lim (f \* g @ F) = lim (f @ F) × lim (g @ F).

End limit_composition_field.

Section cvg_composition_field_proper.

Context {K : numFieldType} {T : Type}.
Context (F : set (set T)) {FF : ProperFilter F}.
Implicit Types (f g : T → K) (a b : K).

Lemma limV f : lim (f @ F) != 0 → lim (f \^-1 @ F) = (lim (f @ F))^-1.

Lemma is_cvgVE f : lim (f @ F) != 0 → cvg (f \^-1 @ F) = cvg (f @ F).

End cvg_composition_field_proper.

Section ProperFilterRealType.
Context {T : Type} {F : set (set T)} {FF : ProperFilter F} {R : realFieldType}.
Implicit Types (f g h : T → R) (a b : R).

Lemma cvgr_to_ge f a b : f @ F --> a → (\near F , b ≤ f F ) → b ≤ a.

Lemma cvgr_to_le f a b : f @ F --> a → (\near F , f F ≤ b ) → a ≤ b.

Lemma limr_ge x f : cvg (f @ F) → (\near F , x ≤ f F ) → x ≤ lim (f @ F).

Lemma limr_le x f : cvg (f @ F) → (\near F , x ≥ f F ) → x ≥ lim (f @ F).

Lemma __deprecated__cvg_gt_ge (u : T → R) a b :
  u @ F --> b → a < b → \∀ n \near F , a ≤ u n.

Lemma __deprecated__cvg_lt_le (u : T → R) c b :
  u @ F --> b → b < c → \∀ n \near F , u n ≤ c.

End ProperFilterRealType.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgr_ge` and generalized to a `Filter`")]
Notation cvg_gt_ge := __deprecated__cvg_gt_ge.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgr_le` and generalized to a `Filter`")]
Notation cvg_lt_le_:= __deprecated__cvg_lt_le.

Section local_continuity.

Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.
Implicit Types (f g : T → V) (s t : T → K) (x : T) (k : K) (a : V).

Lemma continuousN (f : T → V) x :
  {for x , continuous f } → {for x , continuous (fun x ⇒ - f x)}.

Lemma continuousD f g x :
  {for x , continuous f } → {for x , continuous g } →
  {for x , continuous (f + g)}.

Lemma continuousB f g x :
  {for x , continuous f } → {for x , continuous g } →
  {for x , continuous (f - g)}.

Lemma continuousZ s f x :
  {for x , continuous s } → {for x , continuous f } →
  {for x , continuous (fun x ⇒ s x *: f x)}.

Lemma continuousZr f k x :
  {for x , continuous f } → {for x , continuous (k \*: f)}.

Lemma continuousZl s a x :
  {for x , continuous s } → {for x , continuous (fun z ⇒ s z *: a)}.

Lemma continuousM s t x :
  {for x , continuous s } → {for x , continuous t } →
  {for x , continuous (s × t)}.

Lemma continuousV s x : s x != 0 →
  {for x , continuous s } → {for x , continuous (fun x ⇒ (s x)^-1%R)}.

End local_continuity.

Section nbhs_ereal.
Context {R : numFieldType} (P : \bar R → Prop).

Lemma nbhs_EFin (x : R) : (\∀ y \near x %:E , P y ) ↔ \near x , P x %:E.

Lemma nbhs_ereal_pinfty :
  (\∀ x \near +oo%E, P x ) ↔ [/\ P +oo%E & \∀ x \near +oo , P x %:E ].

Lemma nbhs_ereal_ninfty :
  (\∀ x \near -oo%E, P x ) ↔ [/\ P -oo%E & \∀ x \near -oo , P x %:E ].
End nbhs_ereal.

Section cvg_fin.
Context {R : numFieldType}.

Section filter.
Context {F : set (set \bar R)} {FF : Filter F}.

Lemma fine_fcvg a : F --> a %:E → fine @ F --> a.

Lemma fcvg_is_fine a : F --> a %:E → \near F , F \is a fin_num.

End filter.

Section limit.
Context {I : Type} {F : set (set I)} {FF : Filter F} (f : I → \bar R).

Lemma fine_cvg a : f @ F --> a %:E → fine \o f @ F --> a.

Lemma cvg_is_fine a : f @ F --> a %:E → \near F , f F \is a fin_num.

Lemma cvg_EFin a : (\near F , f F \is a fin_num ) → fine \o f @ F --> a →
  f @ F --> a %:E.

Lemma fine_cvgP a :
   f @ F --> a %:E ↔ (\near F , f F \is a fin_num ) ∧ fine \o f @ F --> a.

Lemma neq0_fine_cvgP a : a != 0 → f @ F --> a %:E ↔ fine \o f @ F --> a.

End limit.

End cvg_fin.

Lemma eq_cvg (T T' : Type) (F : set (set T)) (f g : T → T') (x : set (set T')) :
  f =1 g → (f @ F --> x ) = (g @ F --> x ).

Lemma eq_is_cvg (T T' : Type) (fT : filteredType T') (F : set (set T)) (f g : T → T') :
  f =1 g → [cvg (f @ F ) in fT ] = [cvg (g @ F ) in fT ].

Section ecvg_realFieldType.
Context {I} {F : set (set I)} {FF : Filter F} {R : realFieldType}.
Implicit Types f g u v : I → \bar R.
Local Open Scope ereal_scope.

Lemma cvgeD f g a b :
  a +? b → f @ F --> a → g @ F --> b → f \+ g @ F --> a + b.

Lemma cvgeN f x : f @ F --> x → - f x @[x --> F ] --> - x.

Lemma cvgeNP f a : - f x @[x --> F ] --> - a ↔ f @ F --> a.

Lemma cvgeB f g a b :
  a +? - b → f @ F --> a → g @ F --> b → f \- g @ F --> a - b.

Lemma cvge_sub0 f (k : \bar R) :
  k \is a fin_num → (fun x ⇒ f x - k ) @ F --> 0 ↔ f @ F --> k.

Lemma abse_continuous : continuous (@abse R).

Lemma cvg_abse f (a : \bar R) : f @ F --> a → `|f x |%E @[x --> F ] --> `|a |%E.

Lemma is_cvg_abse (f : I → \bar R) : cvg (f @ F) → cvg (`|f x |%E @[x --> F ]).

Lemma is_cvgeN f : cvg (f @ F) → cvg (\- f @ F).

Lemma is_cvgeNE f : cvg (\- f @ F) = cvg (f @ F).

Lemma mule_continuous (r : R) : continuous (mule r %:E).

Lemma cvgeMl f x y : y \is a fin_num →
  f @ F --> x → (fun n ⇒ y × f n ) @ F --> y × x.

Lemma is_cvgeMl f y : y \is a fin_num →
  cvg (f @ F) → cvg ((fun n ⇒ y × f n ) @ F).

Lemma cvgeMr f x y : y \is a fin_num →
  f @ F --> x → (fun n ⇒ f n × y ) @ F --> x × y.

Lemma is_cvgeMr f y : y \is a fin_num →
  cvg (f @ F) → cvg ((fun n ⇒ f n × y ) @ F).

Lemma cvg_abse0P f : abse \o f @ F --> 0 ↔ f @ F --> 0.

Let cvgeM_gt0_pinfty f g b :
  (0 < b)%R → f @ F --> +oo → g @ F --> b %:E → f \* g @ F --> +oo.

Let cvgeM_lt0_pinfty f g b :
  (b < 0)%R → f @ F --> +oo → g @ F --> b %:E → f \* g @ F --> -oo.

Let cvgeM_gt0_ninfty f g b :
  (0 < b)%R → f @ F --> -oo → g @ F --> b %:E → f \* g @ F --> -oo.

Let cvgeM_lt0_ninfty f g b :
  (b < 0)%R → f @ F --> -oo → g @ F --> b %:E → f \* g @ F --> +oo.

Lemma cvgeM f g (a b : \bar R) :
a *? b → f @ F --> a → g @ F --> b → f \* g @ F --> a × b.

End ecvg_realFieldType.

#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to cvgeN, and generalized to filter in Type")]
Notation ereal_cvgN := cvgeN.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to is_cvgeN, and generalized to filter in Type")]
Notation ereal_is_cvgN := is_cvgeN.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to cvgeMl, and generalized to filter in Type")]
Notation ereal_cvgrM := cvgeMl.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to is_cvgeMl, and generalized to filter in Type")]
Notation ereal_is_cvgrM := is_cvgeMl.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to cvgeMr, and generalized to filter in Type")]
Notation ereal_cvgMr := cvgeMr.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to is_cvgeMr, and generalized to filter in Type")]
Notation ereal_is_cvgMr := is_cvgeMr.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to cvgeM, and generalized to a realFieldType")]
Notation ereal_cvgM := cvgeM.

Section open_closed_sets_ereal.
Variable R : realFieldType .
Local Open Scope ereal_scope.
Implicit Types x y : \bar R.
Implicit Types r : R.

Lemma open_ereal_lt y : open [set r : R | r %:E < y ].

Lemma open_ereal_gt y : open [set r : R | y < r %:E ].

Lemma open_ereal_lt' x y : x < y → ereal_nbhs x (fun u ⇒ u < y).

Lemma open_ereal_gt' x y : y < x → ereal_nbhs x (fun u ⇒ y < u).

Lemma open_ereal_lt_ereal x : open [set y | y < x ].

Lemma open_ereal_gt_ereal x : open [set y | x < y ].

Lemma closed_ereal_le_ereal y : closed [set x | y ≤ x ].

Lemma closed_ereal_ge_ereal y : closed [set x | y ≥ x ].

End open_closed_sets_ereal.

Section closure_left_right_open.
Variable R : realFieldType.
Implicit Types z : R.

Lemma closure_gt z : closure ([set x | z < x ] : set R) = [set x | z ≤ x ].

Lemma closure_lt z : closure ([set x : R | x < z ]) = [set x | x ≤ z ].

End closure_left_right_open.

Complete Normed Modules

Extended Types

The topology on real numbers

Lemma R_complete (R : realType) (F : set (set R)) : ProperFilter F → cauchy F → cvg F.

Canonical R_regular_completeType (R : realType) :=
  CompleteType R^o (@R_complete R).
Canonical R_regular_CompleteNormedModule (R : realType) :=
  [completeNormedModType R of R^o].

Canonical R_completeType (R : realType) :=
  [completeType of R for [completeType of R^o]].
Canonical R_CompleteNormedModule (R : realType) :=
  [completeNormedModType R of R ].

Section cvg_seq_bounded.
Context {K : numFieldType}.

Lemma cvg_seq_bounded {V : normedModType K} (a : nat → V) :
  cvg a → bounded_fun a.

End cvg_seq_bounded.

Lemma closure_sup (R : realType) (A : set R) :
  A !=set0 → has_ubound A → closure A (sup A).

Lemma near_infty_natSinv_lt (R : archiFieldType) (e : {posnum R }) :
  \∀ n \near \oo , n.+1%:R^-1 < e %:num.

Lemma near_infty_natSinv_expn_lt (R : archiFieldType) (e : {posnum R }) :
  \∀ n \near \oo , 1 / 2 ^+ n < e %:num.

Lemma limit_pointP (T : archiFieldType) (A : set T) (x : T) :
  limit_point A x ↔ ∃ a_ : nat → T ,
    [/\ a_ @` setT `<=` A , ∀ n, a_ n != x & a_ --> x ].

Section interval.
Variable R : numDomainType.

Definition is_interval (E : set R) :=
  ∀ x y, E x → E y → ∀ z, x ≤ z ≤ y → E z.

Lemma is_intervalPlt (E : set R) :
  is_interval E ↔ ∀ x y, E x → E y → ∀ z, x < z < y → E z.

Lemma interval_is_interval (i : interval R) : is_interval [set ` i ].

End interval.

Section ereal_is_hausdorff.
Variable R : realFieldType.
Implicit Types r : R.

Lemma nbhs_image_EFin (x : R) (X : set R) :
  nbhs x X → nbhs x %:E ((fun r ⇒ r %:E ) @` X).

Lemma nbhs_open_ereal_lt r (f : R → R) : r < f r →
  nbhs r %:E [set y | y < (f r )%:E ]%E.

Lemma nbhs_open_ereal_gt r (f : R → R) : f r < r →
  nbhs r %:E [set y | (f r )%:E < y ]%E.

Lemma nbhs_open_ereal_pinfty r : (nbhs +oo [set y | r %:E < y ])%E.

Lemma nbhs_open_ereal_ninfty r : (nbhs -oo [set y | y < r %:E ])%E.

Lemma ereal_hausdorff : hausdorff_space (ereal_topologicalType R).

End ereal_is_hausdorff.

#[global]
Hint Extern 0 (hausdorff_space _) ⇒ solve[apply: ereal_hausdorff] : core.

#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `nbhs_image_EFin`")]
Notation nbhs_image_ERFin := nbhs_image_EFin.

Lemma EFin_lim (R : realFieldType) (f : nat → R) : cvg f →
  lim (EFin \o f) = (lim f )%:E.

Section ProperFilterERealType.
Context {T : Type} {a : set (set T)} {Fa : ProperFilter a} {R : realFieldType}.
Local Open Scope ereal_scope.
Implicit Types f g h : T → \bar R.

Lemma cvge_to_ge f b c : f @ a --> c → (\near a , b ≤ f a ) → b ≤ c.

Lemma cvge_to_le f b c : f @ a --> c → (\near a , f a ≤ b ) → c ≤ b.

Lemma lime_ge x f : cvg (f @ a) → (\near a , x ≤ f a ) → x ≤ lim (f @ a).

Lemma lime_le x f : cvg (f @ a) → (\near a , x ≥ f a ) → x ≥ lim (f @ a).

End ProperFilterERealType.

Section ecvg_realFieldType_proper.
Context {I} {F : set (set I)} {FF : ProperFilter F} {R : realFieldType}.
Implicit Types (f g : I → \bar R) (u v : I → R) (x : \bar R) (r : R).
Local Open Scope ereal_scope.

Lemma is_cvgeD f g :
  lim (f @ F) +? lim (g @ F) → cvg (f @ F) → cvg (g @ F) → cvg (f \+ g @ F).

Lemma limeD f g :
  cvg (f @ F) → cvg (g @ F) → lim (f @ F) +? lim (g @ F) →
  lim (f \+ g @ F) = lim (f @ F) + lim (g @ F).

Lemma limeMl f y : y \is a fin_num → cvg (f @ F) →
  lim ((fun n ⇒ y × f n ) @ F) = y × lim (f @ F).

Lemma limeMr f y : y \is a fin_num → cvg (f @ F) →
  lim ((fun n ⇒ f n × y ) @ F) = lim (f @ F) × y.

Lemma is_cvgeM f g :
  lim (f @ F) *? lim (g @ F) → cvg (f @ F) → cvg (g @ F) → cvg (f \* g @ F).

Lemma limeM f g :
  cvg (f @ F) → cvg (g @ F) → lim (f @ F) *? lim (g @ F) →
  lim (f \* g @ F) = lim (f @ F) × lim (g @ F).

Lemma limeN f : cvg (f @ F) → lim (\- f @ F) = - lim (f @ F).

Lemma cvge_ge f a b : (\∀ x \near F , b ≤ f x ) → f @ F --> a → b ≤ a.

Lemma cvge_le f a b : (\∀ x \near F , b ≥ f x ) → f @ F --> a → b ≥ a.

Lemma cvg_nnesum (J : Type) (r : seq J) (f : J → I → \bar R)
   (l : J → \bar R) (P : pred J) :
  (∀ j, P j → \near F , 0 ≤ f j F ) →
  (∀ j, P j → f j @ F --> l j ) →
  \sum_(j <- r | P j ) f j i @[i --> F ] --> \sum_(j <- r | P j ) l j.

Lemma lim_nnesum (J : Type) (r : seq J) (f : J → I → \bar R)
   (l : J → \bar R) (P : pred J) :
  (∀ j, P j → \near F , 0 ≤ f j F ) →
  (∀ j, P j → cvg (f j @ F)) →
  lim (\sum_(j <- r | P j ) f j i @[i --> F ]) = \sum_(j <- r | P j ) (lim (f j @ F)).

End ecvg_realFieldType_proper.

#[deprecated(since="mathcomp-analysis 0.6.0", note="generalized to `limeMl`")]
Notation ereal_limrM := limeMl.
#[deprecated(since="mathcomp-analysis 0.6.0", note="generalized to `limeMr`")]
Notation ereal_limMr := limeMr.
#[deprecated(since="mathcomp-analysis 0.6.0", note="generalized to `limeN`")]
Notation ereal_limN := limeN.

Section cvg_0_pinfty.
Context {R : realFieldType} {I : Type} {a : set (set I)} {FF : Filter a}.
Implicit Types f : I → R.

Lemma gtr0_cvgV0 f : (\near a , 0 < f a ) → f \^-1 @ a --> 0 ↔ f @ a --> +oo.

Lemma cvgrVy f : (\near a , 0 < f a ) → f \^-1 @ a --> +oo ↔ f @ a --> 0.

Lemma ltr0_cvgV0 f : (\near a , 0 > f a ) → f \^-1 @ a --> 0 ↔ f @ a --> -oo.

Lemma cvgrVNy f : (\near a , 0 > f a ) → f \^-1 @ a --> -oo ↔ f @ a --> 0.

End cvg_0_pinfty.

Section FilterRealType.
Context {T : Type} {a : set (set T)} {Fa : Filter a} {R : realFieldType}.
Implicit Types f g h : T → R.

Lemma squeeze_cvgr f g h : (\near a , f a ≤ g a ≤ h a ) →
  ∀ (l : R), f @ a --> l → h @ a --> l → g @ a --> l.

Lemma ger_cvgy f g : (\near a , f a ≤ g a ) →
  f @ a --> +oo → g @ a --> +oo.

Lemma ler_cvgNy f g : (\near a , f a ≥ g a ) →
  f @ a --> -oo → g @ a --> -oo.

End FilterRealType.

Section TopoProperFilterRealType.
Context {T : topologicalType} {a : set (set T)} {Fa : ProperFilter a}.
Context {R : realFieldType}.
Implicit Types f g h : T → R.

Lemma ler_cvg_to f g l l' : f @ a --> l → g @ a --> l' →
  (\near a , f a ≤ g a ) → l ≤ l'.

Lemma ler_lim f g : cvg (f @ a) → cvg (g @ a) →
  (\near a , f a ≤ g a ) → lim (f @ a) ≤ lim (g @ a).

End TopoProperFilterRealType.

Section FilterERealType.
Context {T : Type} {a : set (set T)} {Fa : Filter a} {R : realFieldType}.
Local Open Scope ereal_scope.
Implicit Types f g h : T → \bar R.

Lemma gee_cvgy f g : (\near a , f a ≤ g a ) →
  f @ a --> +oo → g @ a --> +oo.

Lemma lee_cvgNy f g : (\near a , f a ≥ g a ) →
  f @ a --> -oo → g @ a --> -oo.

Lemma squeeze_fin f g h : (\near a , f a ≤ g a ≤ h a ) →
    (\near a , f a \is a fin_num ) → (\near a , h a \is a fin_num ) →
  (\near a , g a \is a fin_num ).

Lemma squeeze_cvge f g h : (\near a , f a ≤ g a ≤ h a ) →
  ∀ (l : \bar R), f @ a --> l → h @ a --> l → g @ a --> l.

End FilterERealType.

Section TopoProperFilterERealType.
Context {T : topologicalType} {a : set (set T)} {Fa : ProperFilter a}.
Context {R : realFieldType}.
Local Open Scope ereal_scope.
Implicit Types f g h : T → \bar R.

Lemma lee_cvg_to f g l l' : f @ a --> l → g @ a --> l' →
  (\near a , f a ≤ g a ) → l ≤ l'.

Lemma lee_lim f g : cvg (f @ a) → cvg (g @ a) →
  (\near a , f a ≤ g a ) → lim (f @ a) ≤ lim (g @ a).

End TopoProperFilterERealType.

Section open_union_rat.
Variable R : realType.
Implicit Types A U : set R.

Let ointsub A U := [/\ open A , is_interval A & A `<=` U ].

Let ointsub_rat U q := [set A | ointsub A U ∧ A (ratr q)].

Let ointsub_rat0 q : ointsub_rat set0 q = set0.

Definition bigcup_ointsub U q := \bigcup_(A in ointsub_rat U q ) A.

Lemma bigcup_ointsub0 q : bigcup_ointsub set0 q = set0.

Lemma open_bigcup_ointsub U q : open (bigcup_ointsub U q).

Lemma is_interval_bigcup_ointsub U q : is_interval (bigcup_ointsub U q).

Lemma bigcup_ointsub_sub U q : bigcup_ointsub U q `<=` U.

Lemma open_bigcup_rat U : open U →
  U = \bigcup_(q in [set q | ratr q \in U ]) bigcup_ointsub U q.

End open_union_rat.

Lemma right_bounded_interior (R : realType) (X : set R) :
  has_ubound X → X ^° `<=` [set r | r < sup X ].

Lemma left_bounded_interior (R : realType) (X : set R) :
  has_lbound X → X ^° `<=` [set r | inf X < r ].

Section interval_realType.
Variable R : realType.

Lemma interval_unbounded_setT (X : set R) : is_interval X →
  ¬ has_lbound X → ¬ has_ubound X → X = setT.

Lemma interval_left_unbounded_interior (X : set R) : is_interval X →
  ¬ has_lbound X → has_ubound X → X ^° = [set r | r < sup X ].

Lemma interval_right_unbounded_interior (X : set R) : is_interval X →
  has_lbound X → ¬ has_ubound X → X ^° = [set r | inf X < r ].

Lemma interval_bounded_interior (X : set R) : is_interval X →
  has_lbound X → has_ubound X → X ^° = [set r | inf X < r < sup X ].

Definition Rhull (X : set R) : interval R := Interval
  (if `[< has_lbound X >] then BSide `[< X (inf X) >] (inf X)
                          else BInfty _ true)
  (if `[< has_ubound X >] then BSide (~~ `[< X (sup X) >]) (sup X)
                          else BInfty _ false).

Lemma Rhull0 : Rhull set0 = `]0, 0[ :> interval R.

Lemma sub_Rhull (X : set R) : X `<=` [set x | x \in Rhull X ].

Lemma is_intervalP (X : set R) : is_interval X ↔ X = [set x | x \in Rhull X ].

Lemma connected_intervalP (E : set R) : connected E ↔ is_interval E.
End interval_realType.

Section segment.
Variable R : realType.

properties of segments in [R]

Lemma segment_connected (a b : R) : connected `[a , b ].

Lemma segment_compact (a b : R) : compact `[a , b ].

End segment.

Lemma __deprecated__ler0_addgt0P (R : numFieldType) (x : R) :
  reflect (∀ e, e > 0 → x ≤ e) (x ≤ 0).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `ler_gtP` instead which generalizes it to any upper bound.")]
Notation ler0_addgt0P := __deprecated__ler0_addgt0P.

Lemma IVT (R : realType) (f : R → R) (a b v : R) :
  a ≤ b → {within `[a , b ], continuous f } →
  minr (f a) (f b) ≤ v ≤ maxr (f a) (f b) →
  exists2 c , c \in `[a, b] & f c = v.

Local properties in [R] Topology on [R]² Lemma locally_2d_align : forall (P Q : R -> R -> Prop) x y, ( forall eps : {posnum R}, (forall uv, ball (x, y) eps uv -> P uv.1 uv.2) -> forall uv, ball (x, y) eps uv -> Q uv.1 uv.2 ) -> {near x & y, forall x y, P x y} -> {near x & y, forall x y, Q x y}. Proof. move=> P Q x y /= K => /locallyP [d _ H]. apply/locallyP; exists d => // uv Huv. by apply (K d) => //. Qed. Lemma locally_2d_1d_const_x : forall (P : R -> R -> Prop) x y, locally_2d x y P -> locally y (fun t => P x t). Proof. move=> P x y /locallyP [d _ Hd]. exists d => // z Hz. by apply (Hd (x, z)). Qed. Lemma locally_2d_1d_const_y : forall (P : R -> R -> Prop) x y, locally_2d x y P -> locally x (fun t => P t y). Proof. move=> P x y /locallyP [d _ Hd]. apply/locallyP; exists d => // z Hz. by apply (Hd (z, y)). Qed. Lemma locally_2d_1d_strong (P : R -> R -> Prop) (x y : R): (\near x & y, P x y) -> \forall u \near x & v \near y, forall (t : R), 0 <= t <= 1 -> \forall z \near t, \forall a \near (x + z * (u - x)) & b \near (y + z * (v - y)), P a b. Proof. move=> P x y. apply locally_2d_align => eps HP uv Huv t Ht. set u := uv.1. set v := uv.2. have Zm : 0 <= Num.max `|u - x| `|v - y| by rewrite ler_maxr 2!normr_ge0. rewrite ler_eqVlt in Zm. case/orP : Zm => Zm.

apply filterE => z. apply/locallyP. exists eps => // pq. rewrite !(RminusE,RmultE,RplusE). move: (Zm). have : Num.max `|u - x| `|v - y| <= 0 by rewrite -(eqP Zm). rewrite ler_maxl => /andP[H1 H2] _. rewrite (_ : u - x = 0); last by apply/eqP; rewrite -normr_le0. rewrite (_ : v - y = 0); last by apply/eqP; rewrite -normr_le0. rewrite !(mulr0,addr0); by apply HP.
have : Num.max (`|u - x|) (`|v - y|) < eps. rewrite ltr_maxl; apply/andP; split.
- case: Huv => /sub_ball_abs /=; by rewrite mul1r absrB.
- case: Huv => _ /sub_ball_abs /=; by rewrite mul1r absrB.
rewrite -subr_gt0 => /RltP H1. set d1 := mk{posnum R} _ H1. have /RltP H2 : 0 < pos d1 / 2 / Num.max `|u - x| `|v - y| by rewrite mulr_gt0 // invr_gt0. set d2 := mk{posnum R} _ H2. exists d2 => // z Hz. apply/locallyP. exists [{posnum R} of d1 / 2] => //= pq Hpq. set p := pq.1. set q := pq.2. apply HP; split. + apply/sub_abs_ball => /=. rewrite absrB. rewrite (_ : p - x = p - (x + z * (u - x)) + (z - t + t) * (u - x)); last first. by rewrite subrK opprD addrA subrK. apply: (ler_lt_trans (ler_abs_add _ _)). rewrite (_ : pos eps = pos d1 / 2 + (pos eps - pos d1 / 2)); last first. by rewrite addrCA subrr addr0. rewrite (_ : pos eps - _ = d1) // in Hpq. case: Hpq => /sub_ball_abs Hp /sub_ball_abs Hq. rewrite mul1r /= (_ : pos eps - _ = d1) // !(RminusE,RplusE,RmultE,RdivE) // in Hp, Hq. rewrite absrB in Hp. rewrite absrB in Hq. rewrite (ltr_le_add Hp) // (ler_trans (absrM _ _)) //. apply (@ler_trans _ ((pos d2 + 1) * Num.max `|u - x| `|v - y|)). apply ler_pmul; [by rewrite normr_ge0 | by rewrite normr_ge0 | | ]. rewrite (ler_trans (ler_abs_add _ _)) // ler_add //. move/sub_ball_abs : Hz; rewrite mul1r => tzd2; by rewrite absrB ltrW. rewrite absRE ger0_norm //; by case/andP: Ht. by rewrite ler_maxr lerr. rewrite /d2 /d1 /=. set n := Num.max _ _. rewrite mulrDl mul1r -mulrA mulVr ?unitfE ?lt0r_neq0 // mulr1. rewrite ler_sub_addr addrAC -mulrDl -mulr2n -mulr_natr. by rewrite -mulrA mulrV ?mulr1 ?unitfE // subrK. + apply/sub_abs_ball => /=. rewrite absrB. rewrite (_ : (q - y) = (q - (y + z * (v - y)) + (z - t + t) * (v - y))); last first. by rewrite subrK opprD addrA subrK. apply: (ler_lt_trans (ler_abs_add _ _)). rewrite (_ : pos eps = pos d1 / 2 + (pos eps - pos d1 / 2)); last first. by rewrite addrCA subrr addr0. rewrite (_ : pos eps - _ = d1) // in Hpq. case: Hpq => /sub_ball_abs Hp /sub_ball_abs Hq. rewrite mul1r /= (_ : pos eps - _ = d1) // !(RminusE,RplusE,RmultE,RdivE) // in Hp, Hq. rewrite absrB in Hp. rewrite absrB in Hq. rewrite (ltr_le_add Hq) // (ler_trans (absrM _ _)) //. rewrite (@ler_trans _ ((pos d2 + 1) * Num.max `|u - x| `|v - y|)) //. apply ler_pmul; [by rewrite normr_ge0 | by rewrite normr_ge0 | | ]. rewrite (ler_trans (ler_abs_add _ _)) // ler_add //. move/sub_ball_abs : Hz; rewrite mul1r => tzd2; by rewrite absrB ltrW. rewrite absRE ger0_norm //; by case/andP: Ht. by rewrite ler_maxr lerr orbT. rewrite /d2 /d1 /=. set n := Num.max _ _. rewrite mulrDl mul1r -mulrA mulVr ?unitfE ?lt0r_neq0 // mulr1. rewrite ler_sub_addr addrAC -mulrDl -mulr2n -mulr_natr. by rewrite -mulrA mulrV ?mulr1 ?unitfE // subrK.

Qed. Admitted. TODO redo Lemma locally_2d_1d (P : R -> R -> Prop) x y : locally_2d x y P -> locally_2d x y (fun u v => forall t, 0 <= t <= 1 -> locally_2d (x + t * (u - x)) (y + t * (v - y)) P). Proof. move/locally_2d_1d_strong. apply: locally_2d_impl. apply locally_2d_forall => u v H t Ht. specialize (H t Ht). have : locally t (fun z => locally_2d (x + z * (u - x)) (y + z * (v - y)) P) by [ ]. by apply: locally_singleton. Qed. TODO redo Lemma locally_2d_ex_dec : forall P x y, (forall x y, P x y \/ ~P x y) -> locally_2d x y P -> {d : {posnum R} | forall u v, `|u - x| < d -> `|v - y| < d -> P u v}. Proof. move=> P x y P_dec H. destruct (@locally_ex _ (x, y) (fun z => P (fst z) (snd z))) as [d Hd].

move: H => /locallyP [e _ H]. by apply/locallyP; exists e.

exists d=> u v Hu Hv. by apply (Hd (u, v)) => /=; split; apply sub_abs_ball; rewrite absrB. Qed.

Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) :
  compact A → bounded_set A.

Lemma rV_compact (T : topologicalType) n (A : 'I_n.+1 → set T) :
  (∀ i, compact (A i)) →
  compact [ set v : 'rV[T]_n.+1 | ∀ i, A i (v ord0 i)].

Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R]_n.+1) :
  bounded_set A → closed A → compact A.

Some limits on real functions

Section Shift.

Context {R : zmodType} {T : Type}.

Definition shift (x y : R) := y + x.
Notation center c := (shift (- c)).
Arguments shift x / y.

Lemma comp_shiftK (x : R) (f : R → T) : (f \o shift x ) \o center x = f.

Lemma comp_centerK (x : R) (f : R → T) : (f \o center x ) \o shift x = f.

Lemma shift0 : shift 0 = id.

Lemma center0 : center 0 = id.

End Shift.
Arguments shift {R} x / y.
Notation center c := (shift (- c)).

Lemma near_shift {K : numDomainType} {R : normedModType K}
   (y x : R) (P : set R) :
   (\near x , P x ) = (\∀ z \near y , (P \o shift (x - y)) z ).

Lemma cvg_comp_shift {T : Type} {K : numDomainType} {R : normedModType K}
  (x y : R) (f : R → T) :
  (f \o shift x ) @ y = f @ (y + x ).

Section continuous.
Variables (K : numFieldType) (U V : normedModType K).

Lemma continuous_shift (f : U → V) u :
  {for u , continuous f } = {for 0, continuous (f \o shift u)}.

Lemma continuous_withinNshiftx (f : U → V) u :
  f \o shift u @ 0^' --> f u ↔ {for u , continuous f }.

End continuous.

Section Closed_Ball.

Lemma ball_open (R : numDomainType) (V : normedModType R) (x : V) (r : R) :
  0 < r → open (ball x r).

Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V → R)
  (x : V) (e : R) := [set y | norm (x - y) ≤ e ].

Lemma closed_closed_ball_ (R : realFieldType) (V : normedModType R)
  (x : V) (e : R) : closed (closed_ball_ normr x e).

Definition closed_ball (R : numDomainType) (V : pseudoMetricType R)
  (x : V) (e : R) := closure (ball x e).

Lemma closed_ballxx (R: numDomainType) (V : pseudoMetricType R) (x : V)
  (e : R) : 0 < e → closed_ball x e x.

Lemma closed_ballE (R : realFieldType) (V : normedModType R) (x : V)
  (r : R) : 0 < r → closed_ball x r = closed_ball_ normr x r.

Lemma closed_ball_closed (R : realFieldType) (V : normedModType R) (x : V)
  (r : R) : 0 < r → closed (closed_ball x r).

Lemma closed_ballR_compact (R : realType) (x e : R) : 0 < e →
  compact (closed_ball x e).

Lemma closed_ball_subset (R : realFieldType) (M : normedModType R) (x : M)
  (r0 r1 : R) : 0 < r0 → r0 < r1 → closed_ball x r0 `<=` ball x r1.

Lemma nbhs_closedballP (R : realFieldType) (M : normedModType R) (B : set M)
  (x : M) : nbhs x B ↔ ∃ (r : {posnum R }), closed_ball x r %:num `<=` B.

Lemma subset_closed_ball (R : realFieldType) (V : normedModType R) (x : V)
  (r : R) : 0 < r → ball x r `<=` closed_ball x r.

Lemma locally_compactR (R : realType) : locally_compact [set : R ].

TBA topology.v once ball_normE is there

Lemma interior_closed_ballE (R : realType) (V : normedModType R) (x : V)
(r : R) : 0 < r → (closed_ball x r )^° = ball x r.

Lemma open_nbhs_closed_ball (R : realType) (V : normedModType R) (x : V)
(r : R) : 0 < r → open_nbhs x (closed_ball x r )^°.

End Closed_Ball.

multi-rule bound_in_itv already exists in interval.v, but we advocate that it should actually have the following statement. This does not expose the order between interval bounds.

Lemma bound_itvE (R : numDomainType) (a b : R) :
  ((a \in `[a, b]) = (a ≤ b )) ×
  ((b \in `[a, b]) = (a ≤ b )) ×
  ((a \in `[a, b[) = (a < b )) ×
  ((b \in `]a, b]) = (a < b )) ×
  (a \in `[a, +oo[) ×
  (a \in `]-oo, a]).

Lemma near_in_itv {R : realFieldType} (a b : R) :
  {in `]a, b[, ∀ y, \∀ z \near y , z \in `]a, b[}.

Notation "f @`[ a , b ]" :=
  (`[minr (f a) (f b), maxr (f a) (f b)]) : ring_scope.
Notation "f @`[ a , b ]" :=
  (`[minr (f a) (f b), maxr (f a) (f b)]%classic) : classical_set_scope.
Notation "f @`] a , b [" :=
  (`](minr (f a) (f b)), (maxr (f a) (f b))[) : ring_scope.
Notation "f @`] a , b [" :=
  (`](minr (f a) (f b)), (maxr (f a) (f b))[%classic) : classical_set_scope.

Section image_interval.
Variable R : realDomainType.
Implicit Types (a b : R) (f : R → R).

Lemma mono_mem_image_segment a b f : monotonous `[a, b] f →
  {homo f : x / x \in `[a, b] >-> x \in f @`[a , b ]}.

Lemma mono_mem_image_itvoo a b f : monotonous `[a, b] f →
  {homo f : x / x \in `]a, b[ >-> x \in f @`]a , b [}.

Lemma mono_surj_image_segment a b f : a ≤ b →
    monotonous `[a, b] f → set_surj `[a , b ] (f @`[a , b ]) f →
  f @` `[a , b ] = f @`[a , b ]%classic.

Lemma inc_segment_image a b f : f a ≤ f b → f @`[a , b ] = `[f a, f b].

Lemma dec_segment_image a b f : f b ≤ f a → f @`[a , b ] = `[f b, f a].

Lemma inc_surj_image_segment a b f : a ≤ b →
    {in `[a, b] &, {mono f : x y / x ≤ y }} →
    set_surj `[a , b ] `[f a , f b ] f →
  f @` `[a , b ] = `[f a , f b ]%classic.

Lemma dec_surj_image_segment a b f : a ≤ b →
    {in `[a, b] &, {mono f : x y /~ x ≤ y }} →
    set_surj `[a , b ] `[f b , f a ] f →
  f @` `[a , b ] = `[f b , f a ]%classic.

Lemma inc_surj_image_segmentP a b f : a ≤ b →
    {in `[a, b] &, {mono f : x y / x ≤ y }} →
    set_surj `[a , b ] `[f a , f b ] f →
  ∀ y, reflect (exists2 x , x \in `[a, b] & f x = y) (y \in `[f a, f b]).

Lemma dec_surj_image_segmentP a b f : a ≤ b →
    {in `[a, b] &, {mono f : x y /~ x ≤ y }} →
    set_surj `[a , b ] `[f b , f a ] f →
  ∀ y, reflect (exists2 x , x \in `[a, b] & f x = y) (y \in `[f b, f a]).

Lemma mono_surj_image_segmentP a b f : a ≤ b →
    monotonous `[a, b] f → set_surj `[a , b ] (f @`[a , b ]) f →
  ∀ y, reflect (exists2 x , x \in `[a, b] & f x = y) (y \in f @`[a , b ]).

End image_interval.

Section LinearContinuousBounded.

Variables (R : numFieldType) (V W : normedModType R).

Lemma linear_boundedP (f : {linear V → W}) : bounded_near f (nbhs 0) ↔
  \∀ r \near +oo , ∀ x, `|f x| ≤ r × `|x|.

Lemma continuous_linear_bounded (x : V) (f : {linear V → W}) :
  {for 0, continuous f } → bounded_near f (nbhs x).

Lemma __deprecated__linear_continuous0 (f : {linear V → W}) :
  {for 0, continuous f } → bounded_near f (nbhs (0 : V)).

Lemma bounded_linear_continuous (f : {linear V → W}) :
  bounded_near f (nbhs (0 : V)) → continuous f.

Lemma __deprecated__linear_bounded0 (f : {linear V → W}) :
  bounded_near f (nbhs (0 : V)) → {for 0, continuous f }.

Lemma continuousfor0_continuous (f : {linear V → W}) :
  {for 0, continuous f } → continuous f.

Lemma linear_bounded_continuous (f : {linear V → W}) :
  bounded_near f (nbhs 0) ↔ continuous f.

Lemma bounded_funP (f : {linear V → W}) :
  (∀ r, ∃ M , ∀ x, `|x| ≤ r → `|f x| ≤ M ) ↔
  bounded_near f (nbhs (0 : V)).

End LinearContinuousBounded.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="generalized to `continuous_linear_bounded`")]
Notation linear_continuous0 := __deprecated__linear_continuous0.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="generalized to `bounded_linear_continuous`")]
Notation linear_bounded0 := __deprecated__linear_bounded0.