Library mathcomp.analysis.normedtype

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
From mathcomp Require Import seq fintype bigop order ssralg ssrint ssrnum.
From mathcomp Require Import finmap matrix interval zmodp vector fieldext.
From mathcomp Require Import falgebra.
Require Import boolp ereal reals cardinality.
Require Import classical_sets posnum nngnum 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

is_interval E == the set E is an interval Rhull E == the real interval hull of a set 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 [").

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) = [set [set - y | y in A ] | A in nbhs 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 ler_addgt0Pr (R : numFieldType) (x y : R) :
   reflect (∀ e, e > 0 → x ≤ y + e) (x ≤ y).

Lemma ler_addgt0Pl (R : numFieldType) (x y : R) :
  reflect (∀ e, e > 0 → x ≤ e + y) (x ≤ y).

Lemma in_segment_addgt0Pr (R : numFieldType) (x y z : R) :
  reflect (∀ e, e > 0 → y \in `[x - e, z + e]) (y \in `[x, z]).

Lemma in_segment_addgt0Pl (R : numFieldType) (x y z : R) :
  reflect (∀ e, e > 0 → y \in `[(- e + x), (e + z)]) (y \in `[x, z]).

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 Instance Proper_dnbhs_realType (R : realType) (x : R) :
  ProperFilter x ^'.

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" := (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 near_pinfty_div2 (A : set R) :
  (\∀ k \near +oo , A k ) → (\∀ k \near +oo , A (k / 2)).

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_pinfty_gt_pos r : 0 < r → \∀ x \near +oo , r < x.

Lemma nbhs_pinfty_ge_pos r : 0 < r → \∀ 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_ninfty_lt_pos r : 0 < r → \∀ x \near -oo , r > x.

Lemma nbhs_ninfty_le_pos r : 0 < r → \∀ x \near -oo , r ≥ x.

End infty_nbhs_instances.

Hint Extern 0 (is_true (0 < _)) ⇒ match goal with
  H : ?x \is_near (nbhs +oo ) |- _ ⇒
    solve[near: x; ∃ 0 ⇒ _/posnumP[x] //] end : core.

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_le_nbhs_norm (x : V) : @nbhs V _ x `=>` nbhs_norm x.

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

Lemma nbhs_nbhs_norm : nbhs_norm = nbhs.

Lemma nbhs_normP x P : nbhs x P ↔ nbhs_norm x P.

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 : set V) :
  nbhs_norm x P = \near x , P x.

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

Lemma near_nbhs_norm (x : V) (P : set V) :
  (\∀ 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 cvg_distP {F : set (set V)} {FF : Filter F} (y : V) :
  F --> y ↔ ∀ eps, 0 < eps → \∀ y' \near F , `|y - y'| < eps.

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

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

End PseudoNormedZmod_numDomainType.
Hint Resolve normr_ge0 : core.
Arguments cvg_dist {_ _ F FF}.

Lemma cvg_gt_ge T (F : set (set T)) (R : realFieldType) {PF : ProperFilter F}
    (u : T → R) a b :
  u @ F --> b → (a < b)%R → \∀ n \near F , (a ≤ u n)%R.

Lemma cvg_lt_le T (F : set (set T)) (R : realFieldType) {PF : ProperFilter F}
    (u : T → R) c b :
  u @ F --> b → (b < c)%R → \∀ n \near F , (u n ≤ c)%R.

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

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

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 : numFieldType) (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 : numFieldType) (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))
  (at level 0, x ident, format "[ 'bounded' E | x 'in' 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 [set of 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 [set of 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))
  (at level 2, format "k .-lipschitz_on 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 )))
  (at level 2, A at level 0, format "k .-lipschitz_ A f").
Notation "k .-lipschitz f" := (k.-lipschitz_setT f)
  (at level 2, format "k .-lipschitz f") : type_scope.
Notation "[ 'lipschitz' E | x 'in' A ]" :=
  (lipschitz_on (fun x ⇒ E) (globally (A `*` A)))
  (at level 0, x ident, format "[ 'lipschitz' E | x 'in' A ]").
Notation lipschitz f := [lipschitz f x | x in setT ].

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 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_map_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 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.

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

Lemma 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 {F : set (set V)} {FF : Filter F} (y : V) :
  F --> y → bounded_near id F.

Lemma normrZV (x : V) : x != 0 → `| `| x |^-1 *: x | = 1.

End NormedModule_numFieldType.
Arguments cvg_bounded {_ _ F FF}.
Hint Extern 0 (hausdorff_space _) ⇒ solve[apply: norm_hausdorff] : core.

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

TODO: generalize to R : numFieldType

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 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.

Module Bigminr.
Section bigminr.
Variable (R : realDomainType).

Lemma bigminr_maxr I r (P : pred I) (F : I → R) x :
  \big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i.

Lemma bigminr_mkcond I r (P : pred I) (F : I → R) x :
  \big[minr/x]_(i <- r | P i) F i =
     \big[minr/x]_(i <- r) (if P i then F i else x).

Lemma bigminr_split I r (P : pred I) (F1 F2 : I → R) x :
  \big[minr/x]_(i <- r | P i) (minr (F1 i) (F2 i)) =
  minr (\big[minr/x]_(i <- r | P i) F1 i) (\big[minr/x]_(i <- r | P i) F2 i).

Lemma bigminr_idl I r (P : pred I) (F : I → R) x :
  \big[minr/x]_(i <- r | P i) F i = minr x (\big[minr/x]_(i <- r | P i) F i).

Lemma bigminrID I r (a P : pred I) (F : I → R) x :
  \big[minr/x]_(i <- r | P i) F i =
  minr (\big[minr/x]_(i <- r | P i && a i) F i)
    (\big[minr/x]_(i <- r | P i && ~~ a i) F i).

Lemma bigminr_seq1 I (i : I) (F : I → R) x :
  \big[minr/x]_(j <- [:: i]) F j = minr (F i) x.

Lemma bigminr_pred1_eq (I : finType) (i : I) (F : I → R) x :
  \big[minr/x]_(j | j == i) F j = minr (F i) x.

Lemma bigminr_pred1 (I : finType) i (P : pred I) (F : I → R) x :
  P =1 pred1 i → \big[minr/x]_(j | P j) F j = minr (F i) x.

Lemma bigminrD1 (I : finType) j (P : pred I) (F : I → R) x :
  P j → \big[minr/x]_(i | P i) F i
    = minr (F j) (\big[minr/x]_(i | P i && (i != j )) F i).

Lemma bigminr_ler_cond (I : finType) (P : pred I) (F : I → R) x i0 :
  P i0 → \big[minr/x]_(i | P i) F i ≤ F i0.

Lemma bigminr_ler (I : finType) (F : I → R) (i0 : I) x :
  \big[minr/x]_i F i ≤ F i0.

Lemma bigminr_gerP (I : finType) (P : pred I) m (F : I → R) x :
  reflect (m ≤ x ∧ ∀ i, P i → m ≤ F i)
    (m ≤ \big[minr/x]_(i | P i) F i).

Lemma bigminr_inf (I : finType) i0 (P : pred I) m (F : I → R) x :
  P i0 → F i0 ≤ m → \big[minr/x]_(i | P i) F i ≤ m.

Lemma bigminr_gtrP (I : finType) (P : pred I) m (F : I → R) x :
  reflect (m < x ∧ ∀ i, P i → m < F i)
    (m < \big[minr/x]_(i | P i) F i).

Lemma bigminr_lerP (I : finType) (P : pred I) m (F : I → R) x :
  reflect (x ≤ m ∨ exists2 i , P i & F i ≤ m)
  (\big[minr/x]_(i | P i) F i ≤ m).

Lemma bigminr_ltrP (I : finType) (P : pred I) m (F : I → R) x :
  reflect (x < m ∨ exists2 i , P i & F i < m)
  (\big[minr/x]_(i | P i) F i < m).

Lemma bigminr_eq_arg (I : finType) i0 (P : pred I) (F : I → R) x :
  P i0 → (∀ i, P i → F i ≤ x ) →
  \big[minr/x]_(i | P i) F i = F [arg min_(i < i0 | P i) F i]%O.

Lemma eq_bigminr (I : finType) i0 (P : pred I) (F : I → R) x :
  P i0 → (∀ i, P i → F i ≤ x ) →
  {i0 | i0 \in I & \big[minr/x]_(i | P i) F i = F i0 }.

End bigminr.
Module Exports.
Arguments bigminr_mkcond {R I r}.
Arguments bigminrID {R I r}.
Arguments bigminr_pred1 {R I} i {P F}.
Arguments bigminrD1 {R I} j {P F}.
Arguments bigminr_ler_cond {R I P F}.
Arguments bigminr_ler {R I F}.
Arguments bigminr_inf {R I} i0 {P m F}.
Arguments bigminr_eq_arg {R I} i0 {P F}.
Arguments eq_bigminr {R I} i0 {P F}.
End Exports.
End Bigminr.
Export Bigminr.Exports.

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 )%:nngnum.

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

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

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

Lemma add_continuous {K : numFieldType} {V : pseudoMetricNormedZmodType K} :
continuous (fun z : V × V ⇒ z .1 + z .2).

Global Instance filter_nbhs (K' : numFieldType) (k : K') :
Filter (nbhs k).

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

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

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).

TODO: generalize to pseudometricnormedzmod

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

Continuity of norm

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

End NVS_continuity_normedModType.

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

Section mule_continuous.
Variable (R : realFieldType).

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

End mule_continuous.

Lemma 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 ).

Section NVS_continuity_mul.

Context {K : numFieldType}.

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

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

End NVS_continuity_mul.

Section cvg_composition.

Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.
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 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 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).

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).

End cvg_composition.

Section cvg_composition_ereal.
Context (R : realFieldType) {T : topologicalType}.
Context (F : set (set T)) {FF : Filter F}.
Local Open Scope ereal_scope.
Implicit Types (f : T → \bar R) (g : T → R) (x y : \bar R) (r : R).

Lemma ereal_cvgN f x : f @ F --> x → (-%E \o f @ F ) --> - x.

Lemma ereal_is_cvgN f : cvg (f @ F) → cvg ((-%E \o f ) @ F).

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

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

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

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

End cvg_composition_ereal.

Section cvg_composition_field.

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

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).

Lemma cvgV f a : a != 0 → f @ F --> a → (f x)^-1 @[x --> F ] --> a^-1.

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

End cvg_composition_field.

Section limit_composition_normedmod.

Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.
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 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).

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

End limit_composition_normedmod.

Section limit_composition_field.

Context {K : numFieldType} {T : topologicalType}.
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).

Lemma limV f : cvg (f @ F) → lim (f @ F) != 0 → lim ((fun x ⇒ (f x)^-1) @ F) = (lim (f @ F))^-1.

End limit_composition_field.

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)}.

End local_continuity.

Complete Normed Modules

Extended Types

The topology on real numbers

Arguments cvg_distW {_ _ F FF}.

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 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 : R ⇒ x < u) (nbhs x).

Global Instance at_right_proper_filter (x : R) : ProperFilter (at_right x).

Global Instance at_left_proper_filter (x : R) : ProperFilter (at_left x).
End at_left_right.

Typeclasses Opaque at_left at_right.

TODO: backport to mathcomp in progress

Lemma itvxx d (T : porderType d) (x : T) : `[x, x] =i pred1 x.

Lemma itvxxP d (T : porderType d) (x y : T) : reflect (y = x) (y \in `[x, x]).

Lemma subset_itv_oo_cc d (T : porderType d) (a b : T) : {subset `]a, b[ ≤ `[a, b]}.

/TODO: backport to mathcomp in progress

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

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 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 open_closed_sets.
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 ].

Some closed sets of [R]

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 ].

Definition bound_side d (T : porderType d) (c : bool) (x : itv_bound T) :=
  if x is BSide c' _ then c == c' else false.

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

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.

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

Section closure_left_right_open.
Variable R : archiFieldType.
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.

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.

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 ler0_addgt0P (R : numFieldType) (x : R) :
  reflect (∀ e, e > 0 → x ≤ e) (x ≤ 0).

Lemma IVT (R : realType) (f : R → R) (a b v : R) :
  a ≤ b → {in `[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]

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.

Section open_closed_sets_ereal.
Variable R : realFieldType (* TODO: generalize to numFieldType? *).
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).

Let open_ereal_lt_real r : open (fun x ⇒ x < r %:E).

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

Let open_ereal_gt_real r : open (fun x ⇒ r %:E < 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 ereal_is_hausdorff.
Variable R : realFieldType.
Implicit Types r : R.

Lemma nbhs_image_ERFin (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.

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

Section limit_composition_ereal.

Context {R : realFieldType} {T : topologicalType}.
Context (F : set (set T)) {FF : ProperFilter F}.
Local Open Scope ereal_scope.
Implicit Types (f : T → \bar R) (g : T → R) (x : \bar R) (r : R).

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

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

Lemma ereal_limN f : cvg (f @ F) → lim ((-%E \o f ) @ F) = - lim (f @ F).

End limit_composition_ereal.

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_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.

TBA topology.v once ball_normE is there

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

Lemma dnbhs0_lt (K : numFieldType) (V : normedModType K) e :
  0 < e → \∀ x \near dnbhs (0 : V), `|x| < e.

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

Lemma dnbhs0_le (K : numFieldType) (V : normedModType K) e :
  0 < e → \∀ x \near dnbhs (0 : V), `|x| ≤ e.

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 → surjective `[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 }} →
    surjective `[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 }} →
    surjective `[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 }} →
    surjective `[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 }} →
    surjective `[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 → surjective `[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 : V)) ↔
  \∀ r \near +oo , ∀ x, `|f x| ≤ r × `|x|.

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

Lemma 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 : V)) ↔ 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.