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.
Require Import boolp mathcomp_extra ereal reals cardinality.
Require Import classical_sets signed topology prodnormedzmodule.
Require Import functions.

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

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

End infty_nbhs_instances.

#[global] 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.
#[global] 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 name, 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 (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))
  (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 name, 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}.
#[global]
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.

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

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 abse_continuous (R : realFieldType) : continuous (@abse R).

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

Lemma is_cvg_abse (T : topologicalType) (R : realFieldType) (F : set (set T))
    (f : T → \bar R) : Filter F →
  cvg (f @ F) → cvg ((abse \o f : T → \bar R ) @ F).

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

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

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.

#[global] 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 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 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.

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

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

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.

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

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

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