Module mathcomp.analysis.normedtype_theory.normed_module

From HB Require Import structures.
From mathcomp Require Import boot order finmap ssralg ssrnum ssrint
  interval_inference archimedean rat interval zmodp vector.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets filter functions cardinality
  set_interval.
From mathcomp Require Import reals real_interval ereal topology convex
  tvs num_normedtype ereal_normedtype pseudometric_normed_Zmodule.

# Normed modules We define normed modules. We prove the intermediate value theorem (IVT). ## Normed modules ``` normedModType K == interface type for a normed module structure over the numDomainType K The HB class is NormedModule. subNormedModType R V S == join of SubChoice NormedModule SubLmodule SubNormedZmodule SubConvexTvs normedVectType K == interface type for a normed vectType structure over the numDomainType K The HB class is NormedVector. `|x| == the norm of x (notation from ssrnum.v) ``` We endow `numFieldType` with the types of norm-related notions (accessible with `Import numFieldNormedType.Exports`). ``` pseudoMetric_normed M == an alias for the pseudometric structure defined from a normed module M : normedZmodType K with K : numFieldType. Lmodule_isNormed M == factory for a normed module defined using an L-module M over R : numFieldType subLmodule_isSubNormedmodule R V S == light-weight factory that builds a SubNormedmodule given a SubLmodule over a normedModType ``` ## Hulls ``` Rhull A == the real interval hull of a set A ``` ## Lipschitz functions ``` self_sub f x := f x.1 - f x.2 lipschitz_on f F == f is lipschitz near F k.-lipschitz_on f F == f is k.-lipschitz near F k.-lipschitz_A f == f is k.-lipschitz on A k.-lipschitz f := k.-lipschitz_setT [lipschitz f x | x in A] == f is lipschitz on A [locally [lipschitz f x | x in A] == f is locally lipschitz on A [locally k.-lipschitz_A f] == f is locally k.-lipschitz on A contraction q f == f is q.-lipschitz and q < 1 is_contraction f == exists q, f is q.-lipschitz and q < 1 ```

Reserved Notation "k .-lipschitz_on f"
  (at level 2, format "k .-lipschitz_on f").
Reserved Notation "k .-lipschitz_ A f"
  (at level 2, A at level 0, format "k .-lipschitz_ A f").
Reserved Notation "k .-lipschitz f" (at level 2, format "k .-lipschitz f").
Reserved Notation "[ 'lipschitz' E | x 'in' A ]"
  (at level 0, x name, format "[ 'lipschitz' E | x 'in' A ]").

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Modules with a norm depending on a numDomain

.
    () V & MetricNormedZmodule K V & ConvexTvs K V := {
  normrZ : forall ( : K) ( : V), `| l *: x | = `| l | * `| x |;
}.

#[deprecated(since="mathcomp-analysis 1.19.0",
             use=MetricNormedZmod_ConvexTvs_isNormedModule)]
Notation x1 x2 :=
  (MetricNormedZmod_ConvexTvs_isNormedModule x1 x2).

Module .
#[deprecated(since="mathcomp-analysis 1.19.0",
             use=MetricNormedZmod_ConvexTvs_isNormedModule.Build)]
Notation x1 x2 x3 :=
  (MetricNormedZmod_ConvexTvs_isNormedModule.Build x1 x2 x3) (only parsing).
End PseudoMetricNormedZmod_ConvexTvs_isNormedModule.

()
. () :=
  { of MetricNormedZmodule K T & ConvexTvs K T
     & MetricNormedZmod_ConvexTvs_isNormedModule K T}.

()
. ()
    (V : normedModType R) (S : pred V) :=
  { of SubChoice V S U & NormedModule R U & @GRing.SubLmodule R V S U
       & @Num.SubNormedZmodule R V S U & @SubConvexTvs R V S U}.

.
  () V & MetricNormedZmodule K V & GRing.Lmodule K V := {
normrZ : forall ( : K) ( : V), `| l *: x | = `| l | * `| x |;
}.

. K V.

NB: we have almost the same proof in `tvs.v`

Let : continuous (fun : K^o * V => z.1 *: z.2).

Proof.

move=> [/= k x]; apply/cvgrPdist_lt => _/posnumP[e]; near +oo_K => M.
near=> l z => /=; have M0 : 0 < M by [].
rewrite (@distm_lt_split _ _ (k *: z)) // -?(scalerBr, scalerBl) normrZ.
  rewrite (@le_lt_trans _ _ (M * `|x - z|)) ?ler_wpM2r -?ltr_pdivlMl//.
  by near: z; apply: cvgr_dist_lt; rewrite // mulr_gt0 ?invr_gt0.
rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//.
  by near: z; near: M; apply: cvg_bounded (@cvg_refl _ _).
by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0.
Unshelve. all: by end_near. Qed.

Local Open Scope convex_scope.

Lemma ( : convex_lmodType V) ( : K) : convex_set (ball x r).

Proof.

apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
rewrite inE/=.
rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
(x - y : convex_lmodType _)).
by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr.
rewrite (le_lt_trans (ler_normD _ _))// !normrZ.
rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//.
rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
by rewrite ltrD// ltr_pM2l// onem_gt0.
Qed.

#[local] Lemma ( : K) : balanced_set (ball (0 : V) r).

Proof.

move=> t /= t1 z /= [y].
rewrite -ball_normE /= !sub0r !normrN => + <-.
by rewrite normrZ; apply: le_lt_trans; rewrite ler_piMl.
Qed.

NB: we have almost the same proof in `tvs.v`

Let :
exists2 : set_system (convex_lmodType V),
(forall , b \in B -> absolutely_convex_set b) & (nbhs_basis 0) B.

Proof.

exists [set | exists2 , 0 < r &  B = ball 0 r].
  move=> b; rewrite inE /= => -[r _ ->]; split; first exact: ball_convex_set.
  exact: ball_balanced_set.
split; first by move=> /= a [r r0 ->]; apply: nbhsx_ballx.
move=> /= b; rewrite -nbhs_ballE => -[r /= r0] b0r /=.
by exists (ball 0 r)=> //; exists r.
Qed.

.
  TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous.
..Build K V locally_convex_set.

.
  MetricNormedZmod_ConvexTvs_isNormedModule.Build K V normrZ.

..

()
. () :=
  { of NormedModule K T & Vector K T}.

see also `Section standard_topology_metricNormedZmod` in `pseudometric_normed_Zmodule.v`

Section standard_topology_normedMod.
Variable : numFieldType.

.
  MetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _).

End standard_topology_normedMod.

Module .

Section realType.
Variable ( : realType).

..ComNzAlgebra.copy R R^o.

..copy R R^o.

..copy R R^o.
End realType.

Section rcfType.
Variable ( : rcfType).

..ComNzAlgebra.copy R R^o.

..copy R R^o.

..copy R R^o.
End rcfType.

Section archiFieldType.
Variable ( : archiRealFieldType).

..ComNzAlgebra.copy R R^o.

..copy R R^o.

..copy R R^o.
End archiFieldType.

Section realFieldType.
Variable ( : realFieldType).

..ComNzAlgebra.copy R R^o.

..copy R R^o.

..copy R R^o.
End realFieldType.

Section numClosedFieldType.
Variable ( : numClosedFieldType).

..ComNzAlgebra.copy R R^o.

..copy R R^o.

..copy R R^o.

..ClosedField.on R.
End numClosedFieldType.

Section numFieldType.
Variable ( : numFieldType).

..ComNzAlgebra.copy R R^o.

..copy R R^o.

..copy R R^o.
End numFieldType.

Module . Export numFieldTopology.Exports. HB.reexport. End Exports.

End numFieldNormedType.
Import numFieldNormedType.Exports.

Lemma { : realFieldType} { : numDomainType}
    { : metricNormedZmodType K} ( : R -> U) ( : R) :
  {within `[- b, - a], continuous f} -> {within `[a, b], continuous f \o -%R}.

Proof.

have [ab|ba _ |-> _] := ltgtP a b; last 2 first.
  by rewrite set_itv_ge ?bnd_simp -?ltNge//; exact: continuous_subspace0.
  by rewrite set_itv1; exact: continuous_subspace1.
move/continuous_within_itvccP; rewrite ltrN2 => /(_ ab)[cf fb fa].
apply/(continuous_within_itvccP _ ab); split.
- move=> t tab.
  apply: (@cvg_comp _ _ _ -%R f); first exact: oppr_continuous.
  by apply: cf; rewrite oppr_itvoo !opprK.
- by rewrite -{1}(opprK a); apply/cvg_at_leftNP; exact: fa.
- by rewrite -{1}(opprK b); apply/cvg_at_rightNP; exact: fb.
Qed.

Definition ( : Type) : Type := M.

. () (M : normedZmodType K) :=
Choice.on (pseudoMetric_normed M).
. () (M : normedZmodType K) :=
Num.NormedZmodule.on (pseudoMetric_normed M).

Module .
Section pseudoMetric_from_normedZmodType.
Variables ( : numFieldType) ( : normedZmodType K).

Notation := (pseudoMetric_normed M).

Definition ( : T) ( : K) : set T := ball_ Num.norm x r.

Definition : set_system (T * T) := entourage_ ball.

Definition ( : T) : set_system T := nbhs_ ent x.

Lemma : nbhs = nbhs_ ent

Proof.

by []. Qed.

..Build T nbhs.

Lemma ( : K) : 0 < e -> ball x e x.

Proof.

by rewrite /ball/= subrr normr0. Qed.

Lemma ( : K) : ball x e y -> ball y e x.

Proof.

by rewrite /ball /= distrC. Qed.

Lemma : ball x e1 y -> ball y e2 z ->
ball x (e1 + e2) z.

Proof.

rewrite /ball /= => ? ?.
rewrite -[x](subrK y) -(addrA (x + _)).
by rewrite (le_lt_trans (ler_normD _ _))// ltrD.
Qed.

Lemma : ent = entourage_ ball.

Proof.

by []. Qed.

..Build K T
  ent nbhsE ball ball_center ball_sym ball_triangle entourageE.

End pseudoMetric_from_normedZmodType.
Module . HB.reexport. End Exports.
End pseudoMetric_from_normedZmodType.
Export pseudoMetric_from_normedZmodType.Exports.

Section filter_ent.

Import pseudoMetric_from_normedZmodType.

Global Instance { : realFieldType} ( : normedZmodType R)
  : Filter [set | exists2 : set (pseudoMetric_normed U *
                                     pseudoMetric_normed U),
           ent A & xsection A x `<=` P].

Proof.

apply: Build_Filter => /=.
- by exists setT => //; exact: (@entourageT (pseudoMetric_normed U)).
- move=> A B/= [A' [r/= r0 ballA'] A'A] [B' [d/= d0 ballB'] B'B].
  exists (A' `&` B'); last by rewrite xsectionI; exact: setISS.
  rewrite entourageE /entourage_.
  exists (Num.min r d); first by rewrite /= lt_min r0.
  move=> z/= Hz; split.
  + by apply: ballA' => /=; rewrite /ball/= (lt_le_trans Hz)// ge_min lexx.
  + by apply: ballB' => /=; rewrite /ball/= (lt_le_trans Hz)// ge_min lexx orbT.
- by move=> P Q PQ [A entA AP]; exists A => //; exact: (subset_trans AP).
Qed.

End filter_ent.

. () M
& GRing.Lmodule R M := {
norm : M -> R;
ler_normD : forall , norm (x + y) <= norm x + norm y ;
normrZ : forall ( : R) ( : M), norm (l *: x) = `|l| * norm x ;
normr0_eq0 : forall : M, norm x = 0 -> x = 0
}.

. R M.

Lemma : norm (x *+ n) = norm x *+ n.

Proof.

have := normrZ n%:R x; rewrite ger0_norm// mulr_natl => <-.
by rewrite scaler_nat.
Qed.

Lemma : norm (- x) = norm x.

Proof.

by have := normrZ (- 1)%R x; rewrite scaleN1r normrN normr1 mul1r. Qed.

..Zmodule_isNormed.Build
  R M ler_normD normr0_eq0 normrMn normrN.

..copy M (pseudoMetric_normed M).

..Build M 0.

..Build R M erefl.

..Build R M.

..Build
  M (@PseudoMetricNormedZmodule_add_unif_continuous _ M).

..Build
  M (@PseudoMetricNormedZmodule_opp_unif_continuous _ M).

.
  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ.

..

Definition ( : realFieldType)
  ( : normedModType R) ( : pred V) ( : Type) : Type := U.

Section SubLmodule_isSubNormedmodule.
Context ( : realFieldType) ( : normedModType R) ( : pred V)
  ( : subLmodType S).

Local Notation := (subLmodule_isSubNormedmodule S U').

..SubLmodule.on U.

Local Definition := fun : U => `|\val u|.

Let ( : U) : normu (x + y) <= normu x + normu y.

Proof.

by rewrite /normu GRing.valD; exact: ler_normD. Qed.

Let : normu x = 0 -> x = 0.

Proof.

by move/eqP; rewrite normr_eq0 -(@GRing.val0 V S U) => /eqP/val_inj. Qed.

Let : normu (x *+ n) = normu x *+ n.

Proof.

by rewrite /normu raddfMn /=; exact: normrMn. Qed.

Let : normu (- x) = normu x.

Proof.

by rewrite /normu raddfN /=; exact: normrN. Qed.

Let ( : R) ( : U) : normu (l *: x) = `|l| * normu x.

Proof.

by rewrite /normu GRing.valZ; exact: normrZ. Qed.

.
.Build R U normu ler_normuD normruZ normru0_eq0.

Let : forall , @Num.norm _ V ((val : U -> V) x) = @Num.norm _ U x.

Proof.

by []. Qed.

. Num.Zmodule_isSubNormed.Build _ _ _ U normu_valE.

Let : continuous (val : U -> V).

Proof.

move=> /= x.
rewrite /continuous_at.
set rhs := (X in _ --> X).
apply/cvgrPdist_le => //=.
move=> e e0; near=> t.
rewrite -GRing.valN -GRing.valD normu_valE.
by near: t; exact: cvgr_dist_le e e0.
Unshelve. all: by end_near. Qed.

..Build _ _ U continuous_valE.

End SubLmodule_isSubNormedmodule.

Lemma { : numFieldType} : h%:A = h :> R.

Proof.

by rewrite /GRing.scale/= mulr1. Qed.

Lemma { : realType} ( : R -> \bar R) ( : R) :
limf_esup f a^' = limf_esup (fun => f (- x)%R) (- a)%R^'.

Proof.

rewrite /limf_esup dnbhsN image_comp/=.
congr (ereal_inf [set _ | _ in _]); apply/funext => A /=.
rewrite image_comp/= -compA (_ : _ \o _ = idfun)// funeqE => x/=.
by rewrite opprK.
Qed.

Lemma { : realType} ( : R -> R^o) ( : R) ( : R) : (a < b)%R ->
  x \in `]a, b[ ->
  f @ (x : subspace `[a, b]) --> f x ->
  (f \_ `[a, b] x) @[ --> x] --> f x.

Proof.

move=> ab xab xf; apply/cvgrPdist_lt => /= e e0.
move/cvgrPdist_lt : xf => /(_ e e0) xf.
near=> z.
rewrite patchE ifT//.
  rewrite inE; apply: subset_itv_oo_cc.
  by near: z; exact: near_in_itvoo.
near: z.
rewrite /prop_near1 /nbhs/= /nbhs_subspace ifT// in xf.
  by rewrite inE/=; exact: subset_itv_oo_cc xab.
case: xf => x0 /= x00 xf.
near=> z.
apply: xf => //=.
rewrite inE; apply: subset_itv_oo_cc.
by near: z; exact: near_in_itvoo.
Unshelve. all: by end_near. Qed.

Lemma ( : numDomainType) ( : normedModType K) ( : V) :
`|x| \in GRing.unit -> `| `| x |^-1 *: x | = 1.

Proof.

by move=> nxu; rewrite normrZ normrV// normr_id mulVr. Qed.

. () (V : normedModType K) :=
  Norm.isSemiNorm.Build K V (@Num.norm K V) (normr0 V)
    (@normr_ge0 _ V) (@ler_normD _ V) (@normrZ _ V).

. () (V : normedModType K) :=
  Norm.SemiNorm_isNorm.Build K V (@Num.norm K V) (@normr0_eq0 _ V).

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

Section NormedModule_numFieldType.
Context { : numFieldType} { : normedModType K}.

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

Proof.

by rewrite -normr_eq0 -unitfE => /normrZV->. Qed.

Lemma ( : K -> V) :
cvg (f @ x^') -> lim (f @ x^') = lim (f @ x^'+).

Proof.

move=> cvfx; apply/Logic.eq_sym.
apply: cvg_lim => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
by exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
Qed.

Lemma ( : K -> V) :
cvg (f @ x^') -> lim (f @ x^') = lim (f @ x^'-).

Proof.

move=> cvfx; apply/Logic.eq_sym.
apply: cvg_lim => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _].
by apply: xe_A => //; rewrite eq_sym.
Qed.

Arguments scale_continuous _ _ : clear implicits.

Lemma : continuous (fun : V => k *: x).

Proof.

by move=> x; exact: (cvg_comp2 _ cvg_id (scale_continuous _ _ (_, _))).
Qed.

Lemma ( : V) : continuous (fun : K => k *: x).

Proof.

by move=> k; apply: (cvg_comp2 cvg_id _ (scale_continuous _ _ (_, _))).
Qed.

End NormedModule_numFieldType.
Arguments cvg_at_rightE {K V} f x.
Arguments cvg_at_leftE {K V} f x.

Section NormedModule_continuous.
Variables ( : numFieldType) ( : normedModType K).

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

Proof.

by rewrite [in RHS]forE /continuous_at/= add0r cvg_comp_shift add0r.
Qed.

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

Proof.

rewrite continuous_shift; split=> [cfu|].
by apply/(continuous_withinNx _ _).2/(cvg_trans cfu); rewrite /= add0r.
by move/(continuous_withinNx _ _).1/cvg_trans; apply; rewrite /= add0r.
Qed.

End NormedModule_continuous.

Lemma { : numFieldType} { : normedModType R} ( : V) ( : set V) :
(\forall \near 0, P x) -> (\forall \near 0, P (k *: y)).

Proof.

by have /= := @scalel_continuous R V y 0 _; rewrite scale0r; apply.
Qed.

Section NVS_continuity_mul.
Context { : numFieldType}.

Lemma : continuous (fun : K * K => z.1 * z.2).

Proof.

exact: scale_continuous. Qed.

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

Proof.

exact: scaler_continuous. Qed.

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

Proof.

exact: scalel_continuous. Qed.

Lemma ( : K) : x != 0 -> {for x, continuous (@GRing.inv K)}.

Proof.

move=> x_neq0; have nx_gt0 : `|x| > 0 by rewrite normr_gt0.
apply/(@cvgrPdist_ltp _ _ _ (nbhs x)); near (0 : K)^'+ => d. near=> e.
near=> y; have y_neq0 : y != 0 by near: y; apply: (cvgr_neq0 x).
rewrite /= -div1r -[y^-1]div1r -mulNr addf_div// mul1r mulN1r normrM normfV.
rewrite ltr_pdivrMr ?normr_gt0 ?mulf_neq0// (@lt_le_trans _ _ (e * d))//.
by near: y; apply: cvgr_distC_lt => //; rewrite mulr_gt0.
rewrite ler_pM2l => //=; rewrite normrM -ler_pdivrMl//.
near: y; apply: (cvgr_norm_ge x) => //; rewrite ltr_pdivrMl//.
by near: d; apply: nbhs_right_lt; rewrite mulr_gt0.
Unshelve. all: by end_near. Qed.

End NVS_continuity_mul.

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

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

Proof.

move=> ? ?; apply: continuous2_cvg => //.
exact: (@scale_continuous K V (k, a)).
Qed.

Lemma : cvg (s @ F) ->
cvg (f @ F) -> cvg ((fun => s x *: f x) @ F).

Proof.

by have := cvgP _ (cvgZ _ _); apply. Qed.

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

Proof.

by move=> ?; exact: cvgZ. Qed.

Lemma : s @ F --> (1 : K) -> f @ F --> a -> s x *: f x @[ --> F] --> a.

Proof.

by move=> /cvgZ /[apply]; rewrite scale1r. Qed.

Lemma : s @ F --> (0 : K) -> f @ F --> a -> s x *: f x @[ --> F] --> 0.

Proof.

by move=> /cvgZ /[apply]; rewrite scale0r. Qed.

Lemma : s @ F --> k -> f @ F --> (0 : V) -> s x *: f x @[ --> F] --> 0.

Proof.

by move=> /cvgZ /[apply]; rewrite scaler0. Qed.

Lemma : cvg (s @ F) -> cvg ((fun => s x *: a) @ F).

Proof.

by have := cvgP _ (cvgZr_tmp _); apply. Qed.

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

Proof.

exact: cvgZ. Qed.

Lemma : cvg (f @ F) -> cvg (k *: f @ F).

Proof.

by have := cvgP _ (cvgZl_tmp _); apply. Qed.

Lemma : k != 0 -> cvg (k *: f @ F) = cvg (f @ F).

Proof.

move=> k_neq0.
rewrite propeqE; split => [/(@cvgZl_tmp k^-1)|/(@cvgZl_tmp k)/cvgP//].
by under [_ \*: _]funext => x /= do rewrite scalerK//; exact: cvgP.
Qed.

End cvg_composition_normed.

Lemma ( : topologicalType) ( : set T) ( : numFieldType)
( : normedModType K) ( : K) ( : T -> V) :
{within A, continuous f} -> {within A, continuous k *: f}.

Proof.

by move=> cf x; apply: cvgZl_tmp; exact: cf. Qed.

#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgZr_tmp`")]
Notation := cvgZr_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZr_tmp`")]
Notation := is_cvgZr_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgZl_tmp`")]
Notation := cvgZl_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZl_tmp`")]
Notation := is_cvgZl_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZlE`")]
Notation := is_cvgZlE (only parsing).

Section cvg_composition_field.
Context { : numFieldType} { : Type} ( : set_system T) { : Filter F}.
Implicit Types (f g : T -> K) (a b : K).

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

Proof.

by move=> k_neq0 f_cvg; apply: continuous_cvg => //; apply: inv_continuous.
Qed.

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

Proof.

move=> aN0; split=> /(cvgV _); last exact.
by rewrite invrK invr_eq0 inv_funK; apply.
Qed.

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

Proof.

by move=> /cvgV cvf /cvf /cvgP. Qed.

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

Proof.

exact: cvgZ. Qed.

Lemma : f @ F --> a -> f x * b @[ --> F] --> a * b.

Proof.

exact: cvgZr_tmp. Qed.

Lemma : g @ F --> b -> a * g x @[ --> F] --> a * b.

Proof.

exact: cvgZl_tmp. Qed.

Lemma : f @ F --> (1 :> K) -> g @ F --> a -> f \* g @ F --> a.

Proof.

by move=> /cvgM /[apply]; rewrite mul1r. Qed.

Lemma : f @ F --> a -> g @ F --> (1 :> K) -> f \* g @ F --> a.

Proof.

by move=> /cvgM /[apply]; rewrite mulr1. Qed.

Lemma : f @ F --> 0 -> g @ F --> a -> f \* g @ F --> 0.

Proof.

by move=> /cvgM /[apply]; rewrite mul0r. Qed.

Lemma : f @ F --> a -> g @ F --> 0 -> f \* g @ F --> 0.

Proof.

by move=> /cvgM /[apply]; rewrite mulr0. Qed.

Lemma : cvg (f @ F) -> cvg (g @ F) -> cvg (f \* g @ F).

Proof.

exact: is_cvgZ. Qed.

Lemma ( := fun=> a) : cvg (g @ F) -> cvg (f \* g @ F).

Proof.

exact: is_cvgZl_tmp. Qed.

Lemma ( := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (g @ F).

Proof.

exact: is_cvgZlE. Qed.

Lemma ( := fun=> a) : cvg (f @ F) -> cvg (f \* g @ F).

Proof.

move=> f_cvg; have -> : f \* g = g \* f by apply/funeqP=> x; rewrite /= mulrC.
exact: is_cvgMl_tmp.
Qed.

Lemma ( := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (f @ F).

Proof.

move=> a_neq0; have -> : f \* g = g \* f by apply/funeqP=> x; rewrite /= mulrC.
exact: is_cvgMlE_tmp.
Qed.

End cvg_composition_field.
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMr_tmp`")]
Notation := cvgMr_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMl_tmp`")]
Notation := cvgMl_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMl_tmp`")]
Notation := is_cvgMl_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMr_tmp`")]
Notation := is_cvgMr_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMrE_tmp`")]
Notation := is_cvgMrE_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMlE_tmp`")]
Notation := is_cvgMlE_tmp (only parsing).

Section within_continuous_lemmas.
Context { : topologicalType} { : numFieldType} ( : set T).
Implicit Types f g : T -> K.

Lemma : {within A, continuous f} ->
{within A, continuous g} -> {within A, continuous f * g}.

Proof.

by move=> cf cg x; apply: cvgM; [exact: cf | exact: cg]. Qed.

Lemma ( : K) :
{within A, continuous f} -> {within A, continuous cst c * f}.

Proof.

by move=> cf x; apply: cvgMl_tmp; exact: cf. Qed.

Lemma ( : K) :
{within A, continuous f} -> {within A, continuous f * cst c}.

Proof.

by move=> cf x; apply: cvgMr_tmp; exact: cf. Qed.

End within_continuous_lemmas.

Section limit_composition_normed.
Context { : numFieldType} { : normedModType K} { : Type}.
Context ( : set_system T) { : ProperFilter F}.
Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a : V).

Lemma : cvg (s @ F) -> cvg (f @ F) ->
lim ((fun => s x *: f x) @ F) = lim (s @ F) *: lim (f @ F).

Proof.

by move=> ? ?; apply: cvg_lim => //; exact: cvgZ. Qed.

Lemma : cvg (s @ F) ->
lim ((fun => s x *: a) @ F) = lim (s @ F) *: a.

Proof.

by move=> ?; apply: cvg_lim => //; exact: cvgZr_tmp. Qed.

Lemma : cvg (f @ F) -> lim (k *: f @ F) = k *: lim (f @ F).

Proof.

by move=> ?; apply: cvg_lim => //; exact: cvgZl_tmp. Qed.

End limit_composition_normed.
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `limZr_tmp`")]
Notation := limZr_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `limZl_tmp`")]
Notation := limZl_tmp (only parsing).

Section limit_composition_field.
Context { : numFieldType} { : Type}.
Context ( : set_system T) { : ProperFilter F}.
Implicit Types (f g : T -> K).

Lemma : cvg (f @ F) -> cvg (g @ F) ->
lim (f \* g @ F) = lim (f @ F) * lim (g @ F).

Proof.

by move=> ? ?; apply: cvg_lim => //; exact: cvgM. Qed.

End limit_composition_field.

Section cvg_composition_field_proper.
Context { : numFieldType} { : Type}.
Context ( : set_system T) { : ProperFilter F}.
Implicit Types (f g : T -> K) (a b : K).

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

Proof.

by move=> ?; apply: cvg_lim => //; apply: cvgV => //; exact: cvgNpoint.
Qed.

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

Proof.

move=> ?; apply/propeqP; split=> /is_cvgV; last exact.
by rewrite inv_funK; apply; rewrite limV ?invr_eq0.
Qed.

End cvg_composition_field_proper.

Section ProperFilterRealType.
Context { : Type} { : set_system T} { : ProperFilter F} { : realFieldType}.
Implicit Types (f g h : T -> R) (a b : R).

Lemma : f @ F --> a -> (\forall \near F, b <= f x) -> b <= a.

Proof.

by move=> /[swap]/(closed_cvg _ (@closed_ge _ b))/[apply]. Qed.

Lemma : f @ F --> a -> (\forall \near F, f x <= b) -> a <= b.

Proof.

by move=> /[swap]/(closed_cvg _ (@closed_le _ b))/[apply]. Qed.

Lemma : cvg (f @ F) ->
(\forall \near F, x <= f x0) -> x <= lim (f @ F).

Proof.

exact: cvgr_to_ge. Qed.

Lemma : cvg (f @ F) ->
(\forall \near F, x >= f x0) -> x >= lim (f @ F).

Proof.

exact: cvgr_to_le. Qed.

End ProperFilterRealType.

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

Lemma ( : T -> V) :
{for x, continuous f} -> {for x, continuous (fun => - f x)}.

Proof.

by move=> ?; apply: cvgN. Qed.

Lemma :
{for x, continuous f} -> {for x, continuous g} ->
{for x, continuous (f + g)}.

Proof.

by move=> ? ?; exact: cvgD. Qed.

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

Proof.

by move=> ? ?; exact: cvgB. Qed.

Lemma :
{for x, continuous s} -> {for x, continuous f} ->
{for x, continuous (fun => s x *: f x)}.

Proof.

by move=> ? ?; exact: cvgZ. Qed.

Lemma :
{for x, continuous f} -> {for x, continuous (k \*: f)}.

Proof.

by move=> ?; exact: cvgZl_tmp. Qed.

Lemma :
{for x, continuous s} -> {for x, continuous (fun => s z *: a)}.

Proof.

by move=> ?; exact: cvgZr_tmp. Qed.

Lemma :
{for x, continuous s} -> {for x, continuous t} ->
{for x, continuous (s \* t)}.

Proof.

by move=> ? ?; exact: cvgM. Qed.

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

Proof.

by move=> ?; exact: cvgV. Qed.

End local_continuity.
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `continuousZl_tmp`")]
Notation := continuousZl_tmp (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `continuousZr_tmp`")]
Notation := continuousZr_tmp (only parsing).

Section cvg_fin.
Context { : numFieldType}
{ : Type} { : set_system I} { : Filter F} ( : I -> \bar R).

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

Proof.

move=> a_neq0; split=> [|Fa]; first exact: fine_cvg.
apply: cvg_EFin=> //; near (0 : R)^'+ => e.
have lea : e <= `|a| by near: e; apply: nbhs_right_le; rewrite normr_gt0.
near=> x; have : `|a - fine (f x)| < e by near: x; apply: cvgr_dist_lt.
by case: f=> //=; rewrite subr0; apply: contra_ltT.
Unshelve. all: by end_near. Qed.

End cvg_fin.

Section ecvg_realFieldType.
Context {} { : set_system I} { : Filter F} { : realFieldType}.
Implicit Types f g u v : I -> \bar R.
Local Open Scope ereal_scope.

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

Proof.

have yE u v x : u @ F --> +oo -> v @ F --> x%:E -> u \+ v @ F --> +oo.
  move=> /cvgeyPge/= foo /fine_cvgP[Fg gb]; apply/cvgeyPgey.
  near=> A; near=> n; have /(_ _)/wrap[//|Fgn] := near Fg n.
  rewrite -leeBlDr// (@le_trans _ _ (A - (x - 1))%:E)//; last by near: n.
  rewrite ?EFinB leeB// leeBlDr// -[v n]fineK// -EFinD lee_fin.
  by rewrite ler_distlDr// ltW//; near: n; apply: cvgr_dist_lt.
have NyE u v x : u @ F --> -oo -> v @ F --> x%:E -> u \+ v @ F --> -oo.
  move=> /cvgeNyPle/= foo /fine_cvgP -[Fg gb]; apply/cvgeNyPleNy.
  near=> A; near=> n; have /(_ _)/wrap[//|Fgn] := near Fg n.
  rewrite -leeBrDr// (@le_trans _ _ (A - (x + 1))%:E)//; first by near: n.
  rewrite ?EFinB ?EFinD leeB// -[v n]fineK// -EFinD lee_fin.
  by rewrite ler_distlCDr// ltW//; near: n; apply: cvgr_dist_lt.
have yyE u v : u @ F --> +oo -> v @ F --> +oo -> u \+ v @ F --> +oo.
  move=> /cvgeyPge foo /cvgeyPge goo; apply/cvgeyPge => A; near=> y.
  by rewrite -[leLHS]adde0 leeD//; near: y; [apply: foo|apply: goo].
have NyNyE u v : u @ F --> -oo -> v @ F --> -oo -> u \+ v @ F --> -oo.
  move=> /cvgeNyPle foo /cvgeNyPle goo; apply/cvgeNyPle => A; near=> y.
  by rewrite -[leRHS]adde0 leeD//; near: y; [apply: foo|apply: goo].
have addfC u v : u \+ v = v \+ u.
  by apply/funeqP => x; rewrite /= addeC.
move: a b => [a| |] [b| |] //= _; rewrite ?(addey, addye, addeNy, addNye)//=;
  do ?by [apply: yE|apply: NyE|apply: yyE|apply: NyNyE].
- move=> /fine_cvgP[Ff fa] /fine_cvgP[Fg ga]; rewrite -EFinD.
  apply/fine_cvgP; split.
    by near do [rewrite fin_numD; apply/andP; split].
  apply: (@cvg_trans _ ((fine \o f) \+ (fine \o g) @ F))%R; last exact: cvgD.
  by apply: near_eq_cvg; near do rewrite /= fineD//.
- by move=> /[swap]; rewrite addfC; apply: yE.
- by move=> /[swap]; rewrite addfC; apply: NyE.
Unshelve. all: by end_near. Qed.

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

Proof.

by move=> ?; apply: continuous_cvg => //; exact: oppe_continuous. Qed.

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

Proof.

by split=> /cvgeN//; rewrite oppeK//; under eq_cvg do rewrite /= oppeK.
Qed.

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

Proof.

by move=> ab fa gb; apply: cvgeD => //; exact: cvgeN. Qed.

Lemma ( : \bar R) :
k \is a fin_num -> (fun => f x - k) @ F --> 0 <-> f @ F --> k.

Proof.

move=> kfin; split.
move=> /cvgeD-/(_ (cst k) _ isT (cvg_cst _)).
by rewrite add0e; under eq_fun => x do rewrite subeK//.
move: k kfin => [k _ fk| |]//; rewrite -(@subee _ k%:E)//.
exact: cvgeB.
Qed.

Lemma : continuous (@abse R).

Proof.

case=> [r|A /= [r [rreal rA]]|A /= [r [rreal rA]]]/=.
- exact/(cvg_comp _ _ (@norm_continuous _ R r)).
- by exists r; split => // y ry; apply: rA; rewrite (lt_le_trans ry)// lee_abs.
- exists (- r)%R; rewrite realN; split => // y; rewrite EFinN -lteNr => yr.
by apply: rA; rewrite (lt_le_trans yr)// -abseN lee_abs.
Qed.

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

Proof.

by apply: continuous_cvg => //; exact: abse_continuous. Qed.

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

Proof.

by move/cvg_abse/cvgP. Qed.

Lemma : cvg (f @ F) -> cvg (\- f @ F).

Proof.

by move=> /cvg_ex[l fl]; apply: (cvgP (- l)); exact: cvgeN. Qed.

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

Proof.

rewrite propeqE; split=> /cvgeNP/cvgP//.
by under [X in X -> _]eq_is_cvg do rewrite oppeK.
Qed.

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

Proof.

rewrite /continuous_at; wlog r0 : r / (r > 0)%R => [hwlog|].
  have [r0|r0|->] := ltrgtP r 0; do ?exact: hwlog; last first.
    by move=> x; rewrite mul0e; apply: cvg_near_cst; near=> y; rewrite mul0e.
  have -> : *%E r%:E = \- ( *%E (- r)%:E ).
    by apply/funeqP=> x /=; rewrite EFinN mulNe oppeK.
  move=> x; apply: (continuous_comp (hwlog (- r)%R _ _)); rewrite ?oppr_gt0//.
  exact: oppe_continuous.
move=> [s||]/=.
- rewrite -EFinM; apply: cvg_EFin => /=.
    by apply/nbhs_EFin; near do rewrite fin_numM//.
  move=> P /= Prs; apply/nbhs_EFin=> //=.
  by apply: near_fun => //=; apply: continuousM => //=; exact: cst_continuous.
- rewrite gt0_muley ?lte_fin// => A [u [realu uA]].
  exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
  by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivrMl.
- rewrite gt0_muleNy ?lte_fin// => A [u [realu uA]].
  exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
  by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivlMl.
Unshelve. all: by end_near. Qed.

Lemma : y \is a fin_num ->
f @ F --> x -> (fun => y * f n) @ F --> y * x.

Proof.

by move: y => [r| |]// _ /cvg_comp; apply; exact: mule_continuous. Qed.

Lemma : y \is a fin_num ->
cvg (f @ F) -> cvg ((fun => y * f n) @ F).

Proof.

by move=> fy /(cvgeZl fy)/cvgP. Qed.

Lemma : y \is a fin_num ->
f @ F --> x -> (fun => f n * y) @ F --> x * y.

Proof.

by move=> ? ?; rewrite muleC; under eq_fun do rewrite muleC; exact: cvgeZl.
Qed.

Lemma : y \is a fin_num ->
cvg (f @ F) -> cvg ((fun => f n * y) @ F).

Proof.

by move=> fy /(cvgeZr fy)/cvgP. Qed.

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

Proof.

split; last by move=> /cvg_abse; rewrite abse0.
move=> /cvg_ballP f0; apply/cvg_ballP => _/posnumP[e].
have := [elaborate f0 _ (gt0 e)].
rewrite !near_simpl => absf0; rewrite near_simpl.
apply: filterS absf0 => x /=; rewrite /ball/= /ereal_ball !contract0 !sub0r !normrN.
have [fx0|fx0] := leP 0 (f x); first by rewrite gee0_abs.
by rewrite (lte0_abs fx0) contractN normrN.
Qed.

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

Proof.

move=> b_gt0 /cvgeyPge foo /fine_cvgP[gfin gb]; apply/cvgeyPgey.
near (0%R : R)^'+ => e; near=> A; near=> n.
rewrite (@le_trans _ _ (f n * e%:E))// ?lee_pmul// ?lee_fin//.
- by rewrite -lee_pdivrMr ?divr_gt0//; near: n; apply: foo.
- by rewrite (@le_trans _ _ 1) ?lee_fin//; near: n; apply: foo.
rewrite -(@fineK _ (g n)) ?lee_fin; first by near: n; exact: gfin.
by near: n; apply: (cvgr_ge b).
Unshelve. all: end_near. Qed.

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

Proof.

move=> b0 /cvgeyPge foo /fine_cvgP -[gfin gb]; apply/cvgeNyPleNy.
near (0%R : R)^'+ => e; near=> A; near=> n.
rewrite -leeN2 -muleN (@le_trans _ _ (f n * e%:E))//.
by rewrite -lee_pdivrMr ?mulr_gt0 ?oppr_gt0//; near: n; apply: foo.
rewrite lee_pmul ?lee_fin//.
by rewrite (@le_trans _ _ 1) ?lee_fin//; near: n; apply: foo.
rewrite -(@fineK _ (g n)) ?lee_fin; first by near: n; exact: gfin.
near: n; apply: (cvgr_ge (- b)); rewrite 1?cvgNP//.
by near: e; apply: nbhs_right_lt; rewrite oppr_gt0.
Unshelve. all: end_near. Qed.

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

Proof.

move=> b0 foo gb; under eq_fun do rewrite -muleNN.
apply: (@cvgeM_lt0_pinfty _ _ (- b)%R); first by rewrite oppr_lt0.
- by rewrite -(oppeK +oo); apply: cvgeN.
- by rewrite EFinN; apply: cvgeN.
Qed.

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

Proof.

move=> b0 foo gb; under eq_fun do rewrite -muleNN.
apply: (@cvgeM_gt0_pinfty _ _ (- b)%R); first by rewrite oppr_gt0.
- by rewrite -(oppeK +oo); apply: cvgeN.
- by rewrite EFinN; apply: cvgeN.
Qed.

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

Proof.

move=> [:apoo] [:bnoo] [:poopoo] [:poonoo]; move: a b => [a| |] [b| |] //.
- move=> _ /fine_cvgP[finf fa] /fine_cvgP[fing gb].
  apply/fine_cvgP; split.
    by near do apply: fin_numM; [apply: finf | apply: fing].
  apply: (@cvg_trans _ (((fine \o f) \* (fine \o g)) @ F)%R).
    apply: near_eq_cvg; near=> n => //=.
    rewrite -[in RHS](@fineK _ (f n)); first by near: n; exact: finf.
    by rewrite -[in RHS](@fineK _ (g n)) //; near: n; exact: fing.
  exact: cvgM.
- move: f g a; abstract: apoo.
  move=> {}f {}g {}a + fa goo; have [a0 _|a0 _|->] := ltgtP a 0%R.
  + rewrite mulry ltr0_sg// mulN1e.
    by under eq_fun do rewrite muleC; exact: (cvgeM_lt0_pinfty a0).
  + rewrite mulry gtr0_sg// mul1e.
    by under eq_fun do rewrite muleC; exact: (cvgeM_gt0_pinfty a0).
  + by rewrite /mule_def eqxx.
- move: f g a; abstract: bnoo.
  move=> {}f {}g {}a + fa goo; have [a0 _|a0 _|->] := ltgtP a 0%R.
  + rewrite mulrNy ltr0_sg// mulN1e.
    by under eq_fun do rewrite muleC; exact: (cvgeM_lt0_ninfty a0).
  + rewrite mulrNy gtr0_sg// mul1e.
    by under eq_fun do rewrite muleC; exact: (cvgeM_gt0_ninfty a0).
  + by rewrite /mule_def eqxx.
- rewrite mule_defC => ? foo gb; rewrite muleC.
  by under eq_fun do rewrite muleC; exact: apoo.
- move=> _; move: f g; abstract: poopoo.
  move=> {}f {}g /cvgeyPge foo /cvgeyPge goo.
  rewrite mulyy; apply/cvgeyPgey; near=> A; near=> n.
  have A_gt0 : (0 <= A)%R by [].
  by rewrite -[leLHS]mule1 lee_pmul//=; near: n; [apply: foo|apply: goo].
- move=> _; move: f g; abstract: poonoo.
  move=> {}f {}g /cvgeyPge foo /cvgeNyPle goo.
  rewrite mulyNy; apply/cvgeNyPle => A; near=> n.
  rewrite (@le_trans _ _ (g n))//; last by near: n; exact: goo.
  apply: lee_nemull; last by near: n; apply: foo.
  by rewrite (@le_trans _ _ (- 1)%:E)//; near: n; apply: goo; rewrite ltrN10.
- rewrite mule_defC => ? foo gb; rewrite muleC.
  by under eq_fun do rewrite muleC; exact: bnoo.
- move=> _ foo goo.
  by under eq_fun do rewrite muleC; exact: poonoo.
- move=> _ foo goo; rewrite mulNyNy -mulyy.
  by under eq_fun do rewrite -muleNN; apply: poopoo;
    rewrite -/(- -oo); apply: cvgeN.
Unshelve. all: end_near. Qed.

End ecvg_realFieldType.

Section max_cts.
Context { : realType} { : topologicalType}.

Lemma ( : T -> R^o) :
{for x, continuous f} -> {for x, continuous g} ->
{for x, continuous (f \min g)}.

Proof.

move=> ctsf ctsg.
under [_ \min _]eq_fun => ? do rewrite minr_absE.
apply: cvgM => //; apply: cvgD; first exact: cvgD.
by apply: cvgN; apply: cvg_norm; exact: cvgB.
Qed.

Lemma ( : T -> R^o) :
{for x, continuous f} -> {for x, continuous g} ->
{for x, continuous (f \max g)}.

Proof.

move=> ctsf ctsg.
under [_ \max _]eq_fun => ? do rewrite maxr_absE.
apply: cvgM => //; apply: cvgD; first exact: cvgD.
by apply: cvg_norm; exact: cvgB.
Qed.

End max_cts.

Lemma { : archiRealFieldType} ( : set T) ( : T) :
limit_point A x <-> exists : nat -> T,
[/\ a_ @` setT `<=` A, forall , a_ n != x & a_ @ \oo --> x].

Proof.

split=> [Ax|[a_ [aTA a_x] ax]]; last first.
  move=> U /ax[m _ a_U]; near \oo => n; exists (a_ n); split => //.
  by apply aTA; exists n.
  by apply a_U; near: n; exists m.
pose U := fun : nat => [set : T | `|x - z| < n.+1%:R^-1].
suff /(_ _)/cid-/all_sig[a_ anx] : forall , exists , a != x /\ (U n `&` A) a.
  exists a_; split.
  - by move=> a [n _ <-]; have [? []] := anx n.
  - by move=> n; have [] := anx n.
  - apply/cvgrPdist_lt => _/posnumP[e]; near=> n;  have [? [] Uan Aan] := anx n.
    by rewrite (lt_le_trans Uan)// ltW//; near: n; exact: near_infty_natSinv_lt.
move=> n; have : nbhs (x : T) (U n).
  by apply/(nbhs_ballP (x:T) (U n)); rewrite nbhs_ballE; exists n.+1%:R^-1 => //=.
by move/Ax/cid => [/= an [anx Aan Uan]]; exists an.
Unshelve. all: by end_near. Qed.

Lemma { : archiRealFieldType} ( : set R) ( : R) :
limit_point E a <-> (forall , nbhs a U -> infinite_set (U `&` E)).

Proof.

split=> [Ea V aV|]; last first.
  move=> aE U /aE /infiniteP /pcard_leP /injfunPex[/= f funf injf].
  have [f0a|f0a] := eqVneq (f O) a; last first.
    by exists (f 0); case: (funf 0 Logic.I).
  have [Uf1 Ef1]:= funf 1 Logic.I.
  exists (f 1); split=> //; apply/eqP => f1a.
  have := injf 1 0 (in_setT _) (in_setT _).
  by rewrite f1a f0a => /(_ erefl); exact/eqP/oner_neq0.
(* we build 2 sequences a_ and r_ s.t. a_i and r_i have the properties: *)
pose elt_prop ( : R * R) := [/\ ball a ar.2 `<=` V,
  ar.1 \in E, ar.1 \in (ball a ar.2 : set R), ar.2 > 0 & ar.1 != a].
pose elt_type := { : R * R | elt_prop ar}.
pose a_ ( : elt_type) := (proj1_sig x).1.
pose r_ ( : elt_type) := (proj1_sig x).2.
(* two successive (a_i, r_i) and (a_j, r_j) satisfy the relation: *)
pose elt_rel := `|a - a_ i| = r_ j /\ ball a (r_ j) `<=` ball a (r_ i) /\
  `|a - a_ j| < `|a - a_ i| /\ a_ i != a_ j.
move: aV => -[r0/= r0_gt0 ar0V].
pose V0 : set R := ball a r0.
move/limit_pointP : Ea => [y_ [y_E y_neq_a y_cvg_a]].
have [a0 [a0a a0V0 a0E]] : exists , [/\ a0 != a, a0 \in V0 & a0 \in E].
  move/cvgrPdist_lt : y_cvg_a => /(_ _ r0_gt0)[M _ May_r0].
  exists (y_ M); split=> //.
  - by apply/mem_set/May_r0 => /=.
  - by apply/mem_set/y_E/imageT.
have [v [v0 Pv]] : { : nat -> elt_type |
    v 0 = exist _ (a0, r0) (And5 ar0V a0E a0V0 r0_gt0 a0a) /\
    forall , elt_rel (v n) (v n.+1)}.
apply: dependent_choice => -[[ai ri] [/= ariV xE aiari ri_gt0 aia]].
  pose rj : R := `|a - ai|.
  have rj_gt0 : 0 < rj by rewrite /rj normr_gt0 subr_eq0 eq_sym.
  apply/cid; move/cvgrPdist_lt : y_cvg_a => /(_ _ rj_gt0)[M/= _ May_rj].
  pose Vj : set R := ball a rj.
  have VjV : Vj `<=` V.
    apply: subset_trans ariV => z /lt_trans; apply.
    by move: aiari; rewrite inE.
  have y_MVj : y_ M \in Vj.
    rewrite inE; apply: (@lt_le_trans _ _ rj) => //.
    by apply: May_rj => /=.
  have y_ME : y_ M \in E by rewrite inE; apply/y_E/imageT.
  exists (exist _ (y_ M, rj) (And5 VjV y_ME y_MVj rj_gt0 (y_neq_a M))) => /=.
  split; first exact.
  split; rewrite /r_ /a_/=.
    by apply: le_ball; move: aiari; rewrite inE => /ltW.
  split; first by move: y_MVj; rewrite inE.
  by apply/eqP => aiyM; move: y_MVj; rewrite -aiyM inE /Vj /ball/= /rj ltxx.
apply/infiniteP/pcard_leP/injfunPex => /=; exists (a_ \o v).
  move=> n _; rewrite /a_ /=.
  by case: (v n) => -[ai ri] [/= ariV /set_mem Eai /set_mem/ariV aiari _ _].
have arv q p : (p < q)%N -> `|a - a_ (v q)| < `|a - a_ (v p)|.
  elim: q p => [[]//|q ih p].
  by rewrite ltnS leq_eqVlt => /predU1P[->|/ih]; last apply: lt_trans;
    by case: (Pv q) => _ [] _ [].
move=> p q _ _ /=; apply: contraPP => /eqP.
by rewrite neq_lt => /orP[] /arv /[swap] ->; rewrite ltxx.
Qed.

Lemma { : archiRealFieldType} ( : set R) :
finite_set V -> limit_point A a -> limit_point (A `\` V) a.

Proof.

move=> finV /limit_point_infinite_setP aA.
apply/limit_point_infinite_setP => U aU.
by rewrite setIDA; apply: infinite_setD => //; exact: aA.
Qed.

Lemma ( : realFieldType) ( : nat -> R) : cvgn f ->
limn (EFin \o f) = (limn f)%:E.

Proof.

move=> cf; apply: cvg_lim => //; move/cvg_ex : cf => [l fl].
by apply: (cvg_comp _ _ fl); rewrite (cvg_lim _ fl).
Qed.

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

Lemma :
lim (f @ F) +? lim (g @ F) -> cvg (f @ F) -> cvg (g @ F) -> cvg (f \+ g @ F).

Proof.

by move=> fg fc gc; have /(_ _)/cvgP := cvgeD fg fc gc. Qed.

Lemma :
cvg (f @ F) -> cvg (g @ F) -> lim (f @ F) +? lim (g @ F) ->
lim (f \+ g @ F) = lim (f @ F) + lim (g @ F).

Proof.

by move=> cf cg fg; apply/cvg_lim => //; exact: cvgeD. Qed.

Lemma : y \is a fin_num -> cvg (f @ F) ->
lim ((fun => y * f n) @ F) = y * lim (f @ F).

Proof.

by move=> yfn cf; apply/cvg_lim => //; exact: cvgeZl. Qed.

Lemma : y \is a fin_num -> cvg (f @ F) ->
lim ((fun => f n * y) @ F) = lim (f @ F) * y.

Proof.

by move=> yfn cf; apply/cvg_lim => //; apply: cvgeZr. Qed.

Lemma :
lim (f @ F) *? lim (g @ F) -> cvg (f @ F) -> cvg (g @ F) -> cvg (f \* g @ F).

Proof.

by move=> fg fc gc; have /(_ _)/cvgP := cvgeM fg fc gc. Qed.

Lemma :
cvg (f @ F) -> cvg (g @ F) -> lim (f @ F) *? lim (g @ F) ->
lim (f \* g @ F) = lim (f @ F) * lim (g @ F).

Proof.

by move=> cf cg fg; apply/cvg_lim => //; exact: cvgeM. Qed.

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

Proof.

by move=> cf; apply/cvg_lim => //; apply: cvgeN. Qed.

Lemma : (\forall \near F, b <= f x) -> f @ F --> a -> b <= a.

Proof.

by move=> ? fa; rewrite -(cvg_lim _ fa) ?lime_ge//=; apply: cvgP fa. Qed.

Lemma : (\forall \near F, b >= f x) -> f @ F --> a -> b >= a.

Proof.

by move=> ? fa; rewrite -(cvg_lim _ fa) ?lime_le//=; apply: cvgP fa. Qed.

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

Proof.

pose bigsimp := (big_nil, big_cons);
elim: r => [|x r IHr]/= f0 fl; rewrite bigsimp; under eq_fun do rewrite bigsimp.
exact: cvg_cst.
case: ifPn => [Px|Pnx]; last exact: IHr.
apply: cvgeD; [|exact: fl|exact: IHr].
by rewrite ge0_adde_def ?inE// ?sume_ge0// => [|j Pj];
rewrite (cvge_ge _ (fl _ _))//; apply: f0.
Qed.

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

Proof.

by move=> ? ?; apply/cvg_lim => //; apply: cvg_nnesum. Qed.

End ecvg_realFieldType_proper.

Section cvg_0_pinfty.
Context { : realFieldType} { : Type} { : set_system I} { : Filter F}.
Implicit Types f : I -> R.

Lemma : (\forall \near F, 0 < f a) ->
f\^-1 @ F --> 0 <-> f @ F --> +oo.

Proof.

move=> f_gt0; split; last first.
  move=> /cvgryPgt cvg_f_oo; apply/cvgr0Pnorm_lt => _/posnumP[e].
  near=> i; rewrite gtr0_norm ?invr_gt0//=; first by near: i.
  by rewrite -ltf_pV2 ?qualifE/= ?invr_gt0 ?invrK//=; near: i.
move=> /cvgr0Pnorm_lt uB; apply/cvgryPgty.
near=> M; near=> i; suff: `|(f i)^-1| < M^-1.
  by rewrite gtr0_norm ?ltf_pV2 ?qualifE ?invr_gt0//=; near: i.
by near: i; apply: uB; rewrite ?invr_gt0.
Unshelve. all: by end_near. Qed.

Lemma : (\forall \near F, 0 < f a) ->
f\^-1 @ F --> +oo <-> f @ F --> 0.

Proof.

by move=> f_gt0; rewrite -gtr0_cvgV0 ?inv_funK//; near do rewrite invr_gt0.
Unshelve. all: by end_near. Qed.

Lemma : (\forall \near F, 0 > f a) ->
f\^-1 @ F --> 0 <-> f @ F --> -oo.

Proof.

move=> fL0; rewrite -cvgNP oppr0 (_ : - f\^-1 = (- f)\^-1).
by apply/funeqP => i; rewrite opprfctE/= invrN.
by rewrite gtr0_cvgV0 ?cvgNry//; near do rewrite oppr_gt0.
Unshelve. all: by end_near. Qed.

Lemma : (\forall \near F, 0 > f a) ->
f\^-1 @ F --> -oo <-> f @ F --> 0.

Proof.

by move=> f_lt0; rewrite -ltr0_cvgV0 ?inv_funK//; near do rewrite invr_lt0.
Unshelve. all: by end_near. Qed.

End cvg_0_pinfty.

Section FilterRealType.
Context { : Type} { : set_system T} { : Filter F} { : realFieldType}.
Implicit Types f g h : T -> R.

Lemma : (\forall \near F, f a <= g a) ->
f @ F --> +oo -> g @ F --> +oo.

Proof.

move=> uv /cvgryPge ucvg; apply/cvgryPge => A.
by near=> x do rewrite (le_trans _ (near uv x _))//.
Unshelve. all: end_near. Qed.

Lemma : (\forall \near F, f a >= g a) ->
f @ F --> -oo -> g @ F --> -oo.

Proof.

move=> uv /cvgrNyPle ucvg; apply/cvgrNyPle => A.
by near=> x do rewrite (le_trans (near uv x _))//.
Unshelve. all: end_near. Qed.

End FilterRealType.

Section TopoProperFilterRealType.
Context { : topologicalType} { : set_system T} { : ProperFilter F}.
Context { : realFieldType}.
Implicit Types f g h : T -> R.

Lemma ( : R) : f @ F --> l -> g @ F --> l' ->
(\forall \near F, f a <= g a) -> l <= l'.

Proof.

move=> fl gl; under eq_near do rewrite -subr_ge0; rewrite -subr_ge0.
by apply: cvgr_to_ge; apply: cvgB.
Qed.

Lemma : cvg (f @ F) -> cvg (g @ F) ->
(\forall \near F, f a <= g a) -> lim (f @ F) <= lim (g @ F).

Proof.

exact: ler_cvg_to. Qed.

End TopoProperFilterRealType.

Section FilterERealType.
Context { : Type} { : set_system T} { : Filter F} { : realFieldType}.
Local Open Scope ereal_scope.
Implicit Types f g h : T -> \bar R.

Lemma : (\forall \near F, f a <= g a) ->
f @ F --> +oo -> g @ F --> +oo.

Proof.

move=> uv /cvgeyPge uecvg; apply/cvgeyPge => A.
by near=> x do rewrite (le_trans _ (near uv x _))//.
Unshelve. all: end_near. Qed.

Lemma : (\forall \near F, f a >= g a) ->
f @ F --> -oo -> g @ F --> -oo.

Proof.

move=> uv /cvgeNyPle uecvg; apply/cvgeNyPle => A.
by near=> x do rewrite (le_trans (near uv x _))//.
Unshelve. all: end_near. Qed.

Lemma : (\forall \near F, f a <= g a <= h a) ->
    (\forall \near F, f a \is a fin_num) ->
    (\forall \near F, h a \is a fin_num) ->
  (\forall \near F, g a \is a fin_num).

Proof.

apply: filterS3 => x /andP[fg gh].
rewrite !fin_numElt => /andP[oof _] /andP[_ hoo].
by rewrite (lt_le_trans oof) ?(le_lt_trans gh).
Qed.

Lemma : (\forall \near F, f a <= g a <= h a) ->
forall : \bar R, f @ F --> l -> h @ F --> l -> g @ F --> l.

Proof.

move=> fgh [l||]; last 2 first.
- by move=> + _; apply: gee_cvgy; apply: filterS fgh => ? /andP[].
- by move=> _; apply: lee_cvgNy; apply: filterS fgh => ? /andP[].
move=> /fine_cvgP[Ff fl] /fine_cvgP[Fh hl]; apply/fine_cvgP.
have Fg := squeeze_fin fgh Ff Fh; split=> //.
apply: squeeze_cvgr fl hl; near=> x => /=.
by have /(_ _)/andP[//|fg gh] := near fgh x; rewrite !fine_le//=; near: x.
Unshelve. all: end_near. Qed.

End FilterERealType.
Arguments squeeze_fin {T F FF R} f g h.
Arguments squeeze_cvge {T F FF R} f g h.

Section TopoProperFilterERealType.
Context { : topologicalType} { : set_system T} { : ProperFilter F}
{ : realFieldType}.
Local Open Scope ereal_scope.
Implicit Types f g h : T -> \bar R.

Lemma : f @ F --> l -> g @ F --> l' ->
(\forall \near F, f a <= g a) -> l <= l'.

Proof.

move=> + + fg; move: l' l.
move=> /= [l'||] [l||]//=; rewrite ?leNye ?leey//=; first 1 last.
- by move=> /(gee_cvgy fg) /cvg_lim<-// /cvg_lim<-.
- by move=> /cvg_lim <-// /(lee_cvgNy fg) /cvg_lim<-.
- by move=> /(gee_cvgy fg) /cvg_lim<-// /cvg_lim<-.
move=> /fine_cvgP[Ff fl] /fine_cvgP[Fg gl].
rewrite lee_fin -(cvg_lim _ fl)// -(cvg_lim _ gl)//.
by apply: ler_lim; [apply: cvgP fl|apply: cvgP gl|near do apply: fine_le].
Unshelve. all: end_near. Qed.

Lemma : cvg (f @ F) -> cvg (g @ F) ->
(\forall \near F, f a <= g a) -> lim (f @ F) <= lim (g @ F).

Proof.

exact: lee_cvg_to. Qed.

End TopoProperFilterERealType.

Section Rhull.
Context { : realType}.

Definition ( : 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 : Rhull set0 = `]0, 0[ :> interval R.

Proof.

rewrite /Rhull (asboolT (has_lbound0 R)) (asboolT (has_ubound0 R)) asboolF //.
by rewrite sup0 inf0.
Qed.

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

Proof.

move=> x Xx/=; rewrite in_itv/=.
case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=.
+ by case: asboolP => ?; case: asboolP => ? //=;
     rewrite !(lteifF,lteifT,ub_le_sup,ge_inf,sup_ub_strict,inf_lb_strict).
+ by case: asboolP => XinfX; rewrite !(lteifF, lteifT);
     [rewrite ge_inf | rewrite inf_lb_strict].
+ by case: asboolP => XsupX; rewrite !(lteifF, lteifT);
     [rewrite ub_le_sup | rewrite sup_ub_strict].
Qed.

Lemma ( : set R) : is_interval X <-> X = [set | x \in Rhull X].

Proof.

split=> [iX|->]; last exact: interval_is_interval.
rewrite predeqE => x /=; split; [exact: sub_Rhull | rewrite in_itv/=].
case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=.
- case: asboolP => XinfX; case: asboolP => XsupX;
    rewrite !(lteifF, lteifT).
  + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx].
    rewrite le_eqVlt => /orP[/eqP -> //|xsupX].
    apply: (@interior_subset R).
    by rewrite interval_bounded_interior // /mkset infXx.
  + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx supXx].
    apply: (@interior_subset R).
    by rewrite interval_bounded_interior // /mkset infXx.
  + move=> /andP[infXx]; rewrite le_eqVlt => /orP[/eqP -> //|xsupX].
    apply: (@interior_subset R).
    by rewrite interval_bounded_interior // /mkset infXx.
  + move=> ?; apply: (@interior_subset R).
    by rewrite interval_bounded_interior // /mkset infXx.
- case: asboolP => XinfX; rewrite !(lteifF, lteifT, andbT).
  + rewrite le_eqVlt => /orP[/eqP<-//|infXx].
    apply: (@interior_subset R).
    by rewrite interval_right_unbounded_interior.
  + move=> infXx; apply: (@interior_subset R).
    by rewrite interval_right_unbounded_interior.
- case: asboolP => XsupX /=.
  + rewrite le_eqVlt => /orP[/eqP->//|xsupX].
    apply: (@interior_subset R).
    by rewrite interval_left_unbounded_interior.
  + move=> xsupX; apply: (@interior_subset R).
    by rewrite interval_left_unbounded_interior.
- by move=> _; rewrite (interval_unbounded_setT iX).
Qed.

Lemma ( : set R) : connected E <-> is_interval E.

Proof.

split => [cE x y Ex Ey z /andP[xz zy]|].
- apply: contrapT => Ez.
  pose Az := E `&` [set | x < z]; pose Bz := E `&` [set | z < x].
  apply/connectedPn : cE; exists (fun => if b then Az else Bz); split.
  + move: xz zy Ez.
    rewrite !le_eqVlt => /predU1P[<-//|xz] /predU1P[->//|zy] Ez.
    by case; [exists x | exists y].
  + rewrite /Az /Bz -setIUr; apply/esym/setIidPl => u Eu.
    by apply/orP; rewrite -neq_lt; apply/negP; apply: contraPnot Eu => /eqP <-.
  + split; [|rewrite setIC].
    + apply/disjoints_subset => /= u /closureI[_]; rewrite closure_gt => zu.
      by rewrite /Az setCI; right; apply/negP; rewrite -leNgt.
    + apply/disjoints_subset => /= u /closureI[_]; rewrite closure_lt => zu.
      by rewrite /Bz setCI; right; apply/negP; rewrite -leNgt.
- apply: contraPP => /connectedPn[A [A0 EU sepA]] intE.
  have [/= x A0x] := A0 false; have [/= y A1y] := A0 true.
  wlog xy : A A0 EU sepA x A0x y A1y / x < y.
    move=> /= wlog_hypo; have [xy|yx|{wlog_hypo}yx] := ltgtP x y.
    + exact: (wlog_hypo _ _ _ _ _ A0x _ A1y).
    + apply: (wlog_hypo (A \o negb) _ _ _ y _ x) => //=;
      by [rewrite setUC | rewrite separatedC].
    + move/separated_disjoint : sepA; rewrite predeqE => /(_ x)[] + _; apply.
      by split => //; rewrite yx.
  pose z := sup (A false `&` [set | x <= z <= y]).
  have A1z : ~ (A true) z.
    have cA0z : closure (A false) z.
      suff : closure (A false `&` [set | x <= z <= y]) z by case/closureI.
      apply: closure_sup; last by exists y => u [_] /andP[].
      by exists x; split => //; rewrite /mkset lexx /= (ltW xy).
    by move: sepA; rewrite /separated => -[] /disjoints_subset + _; apply.
  have /andP[xz zy] : x <= z < y.
    rewrite ub_le_sup//=; [by exists y => u [_] /andP[]| |].
    + by split=> //; rewrite /mkset lexx (ltW xy).
    + rewrite lt_neqAle ge_sup ?andbT; [|by move=> u [_] /andP[]|].
      * by exists x; split => //; rewrite /mkset /= lexx /= (ltW xy).
      * by apply/negP; apply: contraPnot A1y => /eqP <-.
  have [A0z|A0z] := pselect ((A false) z); last first.
  have {}xzy : x <= z <= y by rewrite xz ltW.
    have : ~ E z by rewrite EU => -[].
    by apply; apply (intE x y) => //; rewrite EU; [left|right].
  suff [z1 [/andP[zz1 z1y] Ez1]] : exists : R, z <= z1 <= y /\ ~ E z1.
    apply Ez1; apply (intE x y) => //; rewrite ?EU; [by left|by right|].
    by rewrite z1y (le_trans _ zz1).
  have [r zcA1] : {:{posnum R}| ball z r%:num `<=` ~` closure (A true)}.
    have ? : ~ closure (A true) z.
      by move: sepA; rewrite /separated => -[] _ /disjoints_subset; apply.
    have ? : open (~` closure (A true)) by exact/closed_openC/closed_closure.
    exact/nbhsC_ball/open_nbhs_nbhs.
  pose z1 : R := z + r%:num / 2; exists z1.
  have z1y : z1 <= y.
    rewrite leNgt; apply/negP => yz1.
    suff : (~` closure (A true)) y by apply; exact: subset_closure.
    apply zcA1; rewrite /ball /= ltr_distl (lt_le_trans zy) // ?lerDl //.
    rewrite andbT ltrBlDl addrC (lt_trans yz1) // ltrD2l.
    by rewrite ltr_pdivrMr // ltr_pMr // ltr1n.
  rewrite z1y andbT lerDl; split => //.
  have ncA1z1 : (~` closure (A true)) z1.
    apply zcA1; rewrite /ball /= /z1 opprD addNKr normrN.
    by rewrite ger0_norm // ltr_pdivrMr // ltr_pMr // ltr1n.
  have nA0z1 : ~ (A false) z1.
    move=> A0z1; have : z < z1 by rewrite /z1 ltrDl.
    apply/negP; rewrite -leNgt.
     apply: ub_le_sup; first by exists y => u [_] /andP[].
    by split => //; rewrite /mkset /z1 (le_trans xz) /= ?lerDl // (ltW z1y).
  by rewrite EU => -[//|]; apply: contra_not ncA1z1; exact: subset_closure.
Qed.

Lemma : {in neitv, cancel pred_set Rhull}.

Proof.

move=> [[[] x|[]] [[] y|[]]] /neitvP //;
  rewrite /Rhull /= !(in_itv, inE)/= ?bnd_simp => xy.
- rewrite asboolT// inf_itv// lexx/= xy asboolT// asboolT//=.
  by rewrite asboolF//= sup_itv//= ltxx ?andbF.
- by rewrite asboolT// inf_itv// ?asboolT// ?sup_itv// ?lexx ?xy.
- by rewrite asboolT//= inf_itv// lexx asboolT// asboolF.
- rewrite asboolT// inf_itv//= ltxx asboolF// asboolT//.
  by rewrite sup_itv// ltxx andbF asboolF.
  rewrite asboolT // inf_itv // ltxx asboolF // asboolT //.
  by rewrite sup_itv // xy lexx asboolT.
- by rewrite asboolT // inf_itv// ltxx asboolF // asboolF.
- by rewrite asboolF // asboolT // sup_itv// ltxx asboolF.
- by rewrite asboolF // asboolT // sup_itv// lexx asboolT.
- by rewrite asboolF // asboolF.
Qed.

Lemma : Rhull setT = `]-oo, +oo[%R :> interval R.

Proof.

by rewrite /Rhull -set_itvNyy asboolF// asboolF. Qed.

Lemma : {in (@is_interval _ : set_system R), cancel Rhull pred_set}.

Proof.

by move=> X /asboolP iX; exact/esym/is_intervalP. Qed.

Lemma ( : interval R) : [set` i] = setT -> i = `]-oo, +oo[.

Proof.

have [i0 /(congr1 Rhull)|] := boolP (neitv i).
by rewrite set_itvK// => ->; exact: RhullT.
by rewrite negbK => /eqP ->; rewrite predeqE => /(_ 0)[_]/(_ Logic.I).
Qed.

Lemma : [set` Rhull A] = smallest (@is_interval R) A.

Proof.

apply/seteqP; split; last first.
  by apply: smallest_sub; [apply: interval_is_interval | apply: sub_Rhull].
move=> x /= + I [Iitv AI]; rewrite /Rhull.
have [|] := asboolP (has_lbound A) => lA; last first.
  have /forallNP/(_ x)/existsNP[a] := lA.
  move=> /existsNP[Aa /negP]; rewrite -ltNge => ax.
  have [|]:= asboolP (has_ubound A) => uA; last first.
    move=> ?; have /forallNP/(_ x)/existsNP[b] := uA.
    move=> /existsNP[Ab /negP]; rewrite -ltNge => xb.
    have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI.
    by rewrite ax xb.
  have [As|NAs]/= := asboolP (A _) => xA.
    by apply: (Iitv a (sup A)); by [apply: AI | rewrite ltW ?ax].
  have [||b Ab xb] := @sup_gt _ A x; do ?by [exists a | rewrite (itvP xA)].
  have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI.
  by rewrite ax xb.
have [|]:= asboolP (has_ubound A) => uA; last first.
  have /forallNP/(_ x)/existsNP[b] := uA.
  move=> /existsNP[Ab /negP]; rewrite -ltNge => xb.
  have [Ai|NAi]/= := asboolP (A _) => xA.
    by apply: (Iitv (inf A) b); by [apply: AI | rewrite (ltW xb)].
  have [||a Aa ax] := @inf_lt _ A x; do ?by [exists b | rewrite (itvP xA)].
  have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI.
  by rewrite ax xb.
have [Ai|NAi]/= := asboolP (A _); have [As|NAs]/= := asboolP (A _).
- by apply: Iitv; apply: AI.
- move=> xA.
  have [||b Ab xb] := @sup_gt _ A x; do ?by [exists (inf A) | rewrite (itvP xA)].
  have /(_ (inf A) b) := Iitv; apply; do ?by apply: AI.
  by rewrite (itvP xA) (ltW xb).
- move=> xA.
  have [||a Aa ax] := @inf_lt _ A x; do ?by [exists (sup A) | rewrite (itvP xA)].
  have /(_ a (sup A)) := Iitv; apply; do ?by apply: AI.
  by rewrite (itvP xA) (ltW ax).
have [->|/set0P AN0] := eqVneq A set0.
  by rewrite inf0 sup0 itv_ge//= ltBSide/= ltxx.
move=> xA.
have [||a Aa ax] := @inf_lt _ A x; do ?by [|rewrite (itvP xA)].
have [||b Ab xb] := @sup_gt _ A x; do ?by [|rewrite (itvP xA)].
have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI.
by rewrite ax xb.
Qed.

Lemma : {homo Rhull : / (A `<=` B) >-> {subset A <= B}}.

Proof.

move=> A B AB; suff: [set` Rhull A] `<=` [set` Rhull B] by [].
rewrite Rhull_smallest; apply: smallest_sub; first exact: interval_is_interval.
by rewrite Rhull_smallest; apply: sub_smallest.
Qed.

Lemma : ~~ neitv (Rhull A) -> A = set0.

Proof.

move/negPn/eqP => A0; rewrite predeqE => r; split => // /sub_Rhull.
by rewrite A0.
Qed.

Lemma : Rhull [set` Rhull A] = Rhull A.

Proof.

have [A0|/neitv_Rhull] := boolP (neitv (Rhull A)); first by rewrite set_itvK.
by move=> ->; rewrite ?Rhull0 set_itvE Rhull0.
Qed.

Lemma ( : set R) : A `&` B = set0 ->
is_interval A -> is_interval B -> disjoint_itv (Rhull A) (Rhull B).

Proof.

by move=> AB0 iA iB; rewrite /disjoint_itv RhullK ?inE// RhullK ?inE.
Qed.

End Rhull.

properties of segments in $\bar{R}$

Section segment.
Context { : realType}.

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

Proof.

exact/connected_intervalP/interval_is_interval. Qed.

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

Proof.

have [leab|ltba] := lerP a b; last first.
  by move=> F FF /filter_ex [x abx]; move: ltba; rewrite (itvP abx).
rewrite compact_cover => I D f fop sabUf.
set B := [set | exists2 : {fset I}, {subset E <= D} &
  `[a, x] `<=` \bigcup_( in [set` E]) f i /\ (\bigcup_( in [set` E]) f i) x].
set A := `[a, b] `&` B.
suff Aeab : A = `[a, b]%classic.
  suff [_ [E ? []]] : A b by exists E.
  by rewrite Aeab/= inE/=; exact/andP.
apply: segment_connected.
- have aba : a \in `[a, b] by rewrite in_itv /= lexx.
  exists a; split=> //; have /sabUf [i /= Di fia] := aba.
  exists [fset i]%fset; first by move=> ?; rewrite inE inE => /eqP->.
  split; last by exists i => //=; rewrite inE.
  move=> x /= aex; exists i; [by rewrite /= inE|suff /eqP-> : x == a by []].
  by rewrite eq_le !(itvP aex).
- exists B => //; rewrite openE => x [E sD [saxUf [i Di fx]]].
  have : open (f i) by have /sD := Di; rewrite inE => /fop.
  rewrite openE => /(_ _ fx) [e egt0 xe_fi]; exists e => // y xe_y.
  exists E => //; split; last by exists i => //; apply/xe_fi.
  move=> z /= ayz; have [lezx|ltxz] := lerP z x.
    by apply/saxUf; rewrite /= in_itv/= (itvP ayz) lezx.
  exists i => //; apply/xe_fi; rewrite /ball_/= distrC ger0_norm.
    by rewrite subr_ge0; apply/ltW.
  have lezy : z <= y by rewrite (itvP ayz).
  rewrite ltrBlDl; apply: le_lt_trans lezy _; rewrite -ltrBlDr.
  by have := xe_y; rewrite /ball_ => /ltr_distlCBl.
exists A; last by rewrite predeqE => x; split=> [[] | []].
move=> x clAx; have abx : x \in `[a, b].
  by apply: interval_closed; have /closureI [] := clAx.
split=> //; have /sabUf [i Di fx] := abx.
have /fop := Di; rewrite openE => /(_ _ fx) [_ /posnumP[e] xe_fi].
have /clAx [y [[aby [E sD [sayUf _]]] xe_y]] :=
  nbhsx_ballx x e%:num ltac:(by []).
exists (i |` E)%fset; first by move=> j /fset1UP[->|/sD] //; rewrite inE.
split=> [z axz|]; last first.
  exists i; first by rewrite /= !inE eq_refl.
  by apply/xe_fi; rewrite /ball_/= subrr normr0.
have [lezy|ltyz] := lerP z y.
  have /sayUf [j Dj fjz] : z \in `[a, y] by rewrite in_itv /= (itvP axz) lezy.
  by exists j => //=; rewrite inE orbC Dj.
exists i; first by rewrite /= !inE eq_refl.
apply/xe_fi; rewrite /ball_/= ger0_norm; first by rewrite subr_ge0 (itvP axz).
rewrite ltrBlDl -ltrBlDr; apply: lt_trans ltyz.
by apply: ltr_distlCBl; rewrite distrC.
Qed.

End segment.

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

Proof.

move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b ->
    exists2 , c \in `[a, b] & f c = v; last first.
  case: (leP (f a) (f b)) => [] _ fabv /=; first exact: ivt.
  have [| |c cab /oppr_inj] := ivt (- f) (- v); last by exists c.
  - by move=> x /=; apply/continuousN/fcont.
  - by rewrite lerNr opprK lerNr opprK andbC.
move=> favfb; suff: is_interval (f @` `[a,b]).
  apply; last exact: favfb.
  - by exists a => //=; rewrite in_itv/= lexx.
  - by exists b => //=; rewrite in_itv/= leab lexx.
apply/connected_intervalP/connected_continuous_connected => //.
exact: segment_connected.
Qed.

Section prod_normedModType.
Context { : numFieldType} { : normedModType K}.

Let ( : K) ( : U * V) : `| l *: x | = `|l| * `| x |.

Proof.

by rewrite prod_normE /= !normrZ maxr_pMr. Qed.

..Build
  K (U * V)%type prod_norm_scale.

End prod_normedModType.

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

Proof.

by move=> /sub_boundedr AB x Ax; apply: AB; apply: within_nbhsW. Qed.

Section bounded_mul.
Context { : Type} { : realFieldType}.
Implicit Types (f g : T -> R) (A : set T).

Lemma : [bounded f x | in A] -> [bounded g x | in A] ->
[bounded f x * g x | in A].

Proof.

move=> /bounded_ex_gt0[Mf Mf_gt0 Mf_ub] /bounded_ex_gt0[Mg Mg_gt0 Mg_ub].
by apply: (ub_bounded (Mf * Mg)) => t At; rewrite normrM ler_pM// ?Mf_ub ?Mg_ub.
Qed.

Lemma ( : R) : [bounded f x | in A] ->
[bounded c * f x | in A].

Proof.

by move=> bf; apply: boundedM => //; exact: bounded_cst. Qed.

Lemma ( : R) : [bounded f x | in A] ->
[bounded f x * c | in A].

Proof.

by move=> bf; apply: boundedM => //; exact: bounded_cst. Qed.

Lemma : [bounded f x | in A] -> [bounded g x | in A] ->
[bounded Num.max (f x) (g x) | in A].

Proof.

move=> /bounded_ex_gt0[Mf Mf_gt0 Mf_ub] /bounded_ex_gt0[Mg Mg_gt0 Mg_ub].
apply: (ub_bounded (Num.max Mf Mg)) => x Ax /=.
case: (leP (f x) (g x)) => _.
- by rewrite (le_trans (Mg_ub _ _))// le_max lexx orbT.
- by rewrite (le_trans (Mf_ub _ _))// le_max lexx.
Qed.

End bounded_mul.

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

Lemma ( : numFieldType) ( : normedModType K) ( : K)
    ( : V -> W) ( : set_system (V * V)) :
  F `=>` G -> k.-lipschitz_on f G -> k.-lipschitz_on f F.

Proof.

exact. Qed.

Definition ( : numFieldType) ( : normedModType K)
           ( : V -> W) ( : set_system (V * V)) :=
  \forall \near +oo, M.-lipschitz_on f F.

Lemma ( : numFieldType) ( : normedModType K)
    ( : V -> W) ( : set_system (V * V)) :
  F `=>` G -> lipschitz_on f G -> lipschitz_on f F.

Proof.

by move=> FG; rewrite /lipschitz_on; apply: filterS => M; apply: FG. Qed.

Lemma ( : numFieldType) ( : normedModType K) ( : K)
( : V -> W) ( : set_system (V * V)) { : ProperFilter F} :
k.-lipschitz_on f F -> lipschitz_on f F.

Proof.

by move=> f_lip; apply/ex_dom_bound; exists k. Qed.

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

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

Proof.

by apply: nearW; rewrite setX0 => ?; apply: globally0. Qed.

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

Proof.

apply: (@klipschitzW _ _ _ `|f a|).
exact: (@globally_properfilter _ _ (a, a)).
by move=> [x y] /= [] -> ->; rewrite !subrr !normr0 mulr0.
Qed.

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

Proof.

by move=> + x Ax; apply: sub_klipschitz; apply: within_nbhsW. Qed.

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

Proof.

by move=> + x Ax; apply: sub_lipschitz; apply: within_nbhsW. Qed.

Lemma ( : numFieldType) ( : normedModType R) :
1.-lipschitz (@id V).

Proof.

by move=> [/= x y] _; rewrite mul1r. Qed.

Arguments lipschitz_id {R V}.

Section LinearContinuousBounded.
Variables ( : numFieldType) ( : normedModType R).

Lemma ( : {linear V -> W}) : bounded_near f (nbhs 0) <->
\forall \near +oo, forall , `|f x| <= r * `|x|.

Proof.

split=> [|/pinfty_ex_gt0 [r r0 Bf]]; last first.
  apply/ex_bound; exists r; apply/nbhs_norm0P; exists 1 => //= x /=.
  by rewrite -(gtr_pMr _ r0) => /ltW; exact/le_trans/Bf.
rewrite /bounded_near => /pinfty_ex_gt0 [M M0 /nbhs_norm0P [_/posnumP[e] efM]].
near (0 : R)^'+ => d; near=> r => x.
have[->|x0] := eqVneq x 0; first by rewrite raddf0 !normr0 mulr0.
have nd0 : d / `|x| > 0 by rewrite divr_gt0 ?normr_gt0.
have: `|f (d / `|x| *: x)| <= M.
  by apply: efM => /=; rewrite normrZ gtr0_norm// divfK ?normr_eq0//.
rewrite linearZ/= normrZ gtr0_norm// -ler_pdivlMl//; move/le_trans; apply.
rewrite invfM invrK mulrAC ler_wpM2r//; near: r; apply: nbhs_pinfty_ge.
by rewrite rpredM// ?rpredV ?gtr0_real.
Unshelve. all: by end_near. Qed.

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

Proof.

rewrite /prop_for/continuous_at linear0 /bounded_near => f0.
near=> M; apply/nbhs0P.
near do rewrite /= linearD (le_trans (ler_normD _ _))// -lerBrDl.
by apply: cvgr0_norm_le; rewrite // subr_gt0.
Unshelve. all: by end_near. Qed.

Lemma ( : {linear V -> W}) :
bounded_near f (nbhs (0 : V)) -> continuous f.

Proof.

move=> /linear_boundedP [y [yreal fr]] x; near +oo_R => r.
apply/(@cvgrPdist_lt _ _ _ (nbhs x)) => e e_gt0; near=> z; rewrite -linearB.
rewrite (le_lt_trans (fr r _ _))// -?ltr_pdivlMl//.
by near: z; apply: cvgr_dist_lt => //; rewrite mulrC divr_gt0.
Unshelve. all: by end_near. Qed.

Lemma ( : {linear V -> W}) :
bounded_near f (nbhs 0) <-> continuous f.

Proof.

split; first exact: bounded_linear_continuous.
by move=> /(_ 0); exact: continuous_linear_bounded.
Qed.

Lemma ( : {linear V -> W}) :
(forall , exists , forall , `|x| <= r -> `|f x| <= M) <->
bounded_near f (nbhs (0 : V)).

Proof.

split => [/(_ 1) [M Bf]|/linear_boundedP fr y].
apply/ex_bound; exists M; apply/nbhs_normP => /=; exists 1 => //= x /=.
by rewrite sub0r normrN => x1; exact/Bf/ltW.
near +oo_R => r; exists (r * y) => x xe.
rewrite (@le_trans _ _ (r * `|x|)) //; first by move: {xe} x; near: r.
by rewrite ler_pM.
Unshelve. all: by end_near. Qed.

End LinearContinuousBounded.

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

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

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

End contractions.

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

Proof.

Section cvg_seq_bounded.
Context { : numFieldType}.
Local Notation := (@pinfty_nbhs K).

Lemma { : normedModType K} ( : nat -> V) :
cvgn a -> bounded_fun a.

Proof.

move=> /cvg_bounded/ex_bound => -[/= Moo] => -[N _ /(_ _) aM].
have Moo_real : Moo \is Num.real by rewrite ger0_real ?(le_trans _ (aM N _))/=.
rewrite /bounded_near /=; near=> M => n _.
have [nN|nN]/= := leqP N n; first by apply: (le_trans (aM _ _)).
move: n nN; suff /(_ (Ordinal _)) : forall : 'I_N, `|a n| <= M by [].
by near: M; apply: filter_forall => i; apply: nbhs_pinfty_ge.
Unshelve. all: by end_near. Qed.

End cvg_seq_bounded.

Lemma ( : realType) ( : set R) :
A !=set0 -> compact A -> has_sup A.

Proof.

move=> A0 cA; split => //; have [M [_ MA]] := compact_bounded cA.
by exists (M + 1) => y /MA My; rewrite (le_trans _ (My _ _)) ?ler_norm ?ltrDl.
Qed.

Section Closed_Ball_normedModType.

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

Proof.

rewrite /closed_ball_ -/((normr \o (fun => x - y)) @^-1` [set | x <= e]).
apply: (preimage_closed _ (@closed_le _ _)) => y _.
apply: (continuous_comp _ (@norm_continuous _ _ _)).
exact: (continuousB (@cst_continuous _ _ _ _)).
Qed.

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

Proof.

move=> /posnumP[e]; rewrite eqEsubset; split => y.
  rewrite /closed_ball closureE; apply; split; first exact: closed_closed_ball_.
  by move=> z; rewrite -ball_normE; exact: ltW.
have [-> _|xy] := eqVneq x y; first exact: closed_ballxx.
rewrite /closed_ball closureE -ball_normE.
rewrite /closed_ball_ /= le_eqVlt.
move => /orP[/eqP xye B [Bc Be]|xye _ [_ /(_ _ xye)]//].
apply: Bc => B0 /nbhs_ballP[s s0] B0y.
have [es|se] := leP s e%:num; last first.
  exists x; split; first by apply: Be; rewrite ball_normE; apply: ballxx.
  by apply: B0y; rewrite -ball_normE /ball_ /= distrC xye.
exists (y + (s / 2) *: (`|x - y|^-1 *: (x - y))); split; [apply: Be|apply: B0y].
  rewrite /= opprD addrA -[X in `|X - _|](scale1r (x - y)) scalerA -scalerBl.
  rewrite -[X in X - _](@divff _ `|x - y|) ?normr_eq0 ?subr_eq0//.
  rewrite -mulrBl -scalerA normrZ normfZV ?subr_eq0// mulr1.
  rewrite gtr0_norm; last by rewrite ltrBlDl xye ltrDr mulr_gt0.
  by rewrite subr_gt0 xye ltr_pdivrMr // mulr_natr mulr2n ltr_pwDl.
rewrite -ball_normE /ball_ /= opprD addNKr normrN normrZ normfZV ?subr_eq0//.
by rewrite mulr1 normf_div !gtr0_norm// ltr_pdivrMr// ltr_pMr //ltr1n.
Qed.

Lemma ( : realFieldType) ( : R) : 0 < r ->
closed_ball x r = `[x - r, x + r]%classic.

Proof.

by move=> r0; apply/seteqP; split => y;
rewrite closed_ballE// /closed_ball_ /= in_itv/= ler_distlC.
Qed.

Lemma { : realFieldType} ( : R) : 0 < r ->
closed_ball x r = [set x - r] `|` ball x r `|` [set x + r].

Proof.

move=> r0; rewrite closed_ball_itv// -(setUitv_set2 false true).
by rewrite lerD2l ge0_cp// ltW.
by rewrite setUAC setUC ball_itv.
Qed.

Lemma ( : realType) ( : R) : 0 < e ->
compact (closed_ball x e).

Proof.

move=> e_gt0; have : compact `[x - e, x + e] by apply: segment_compact.
by rewrite closed_ballE//; under eq_set do rewrite in_itv -ler_distlC.
Qed.

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

Proof.

move=> r00 r01; rewrite (_ : r0 = (PosNum r00)%:num) // closed_ballE //.
by move=> m xm; rewrite -ball_normE /ball_ /= (le_lt_trans _ r01).
Qed.

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

Proof.

split=> [/nbhs_ballP[_/posnumP[r] xrB]|[e xeB]]; last first.
apply/nbhs_ballP; exists e%:num => //=.
exact: (subset_trans (@subset_closure _ _) xeB).
exists (r%:num / 2)%:itv.
apply: (subset_trans (closed_ball_subset _ _) xrB) => //=.
by rewrite lter_pdivrMr // ltr_pMr // ltr1n.
Qed.

End Closed_Ball_normedModType.

Lemma ( : realFieldType) ( : R) : a < b ->
closure `]a, b[%classic = `[a, b]%classic.

Proof.

move=> ab.
rewrite itv_center_shift// -ball_itv closure_ballE itv_center_shift//.
by rewrite closed_ball_itv// divr_gt0// subr_gt0.
Qed.

Lemma { : numFieldType} { : normedModType R} ( : set M)
( : M) : open A -> A x -> \forall \near 0^'+, ball x e `<=` A.

Proof.

move=> oA Ax; have /nbhsr0P/= : nbhs x A by exact/open_nbhs_nbhs.
apply: filterS => e xeA y exy; apply: xeA.
by rewrite -ball_normE/= in exy; exact: ltW.
Qed.

Lemma { : realType} ( : set R) : open S -> x \in S ->
exists , let : set R := ball (@ratr R c) (ratr r) in x \in B /\ B `<=` S.

Proof.

move=> oS /set_mem/(open_subball oS)[r/= r0 rS].
have [y yxr] : exists , ball x (r / 4) (ratr y).
  suff : ball x (r / 4) `&` range ratr !=set0.
    by move=> [/= _ []] /[swap] -[y _ <-]; exists y.
  apply: dense_rat; last exact: ball_open.
  by exists x; apply: ballxx; rewrite divr_gt0.
have [q /andP[rq qr]] : exists , r / 4 < ratr q < r / 2.
  have : ball (r / 3) (r / 12) `&` range ratr !=set0.
    apply: dense_rat; last exact: ball_open.
    by exists (r / 3); apply: ballxx; rewrite divr_gt0.
  move=> [/= _ []] /[swap] -[z _ <-].
  rewrite ball_itv/= in_itv/= => /andP[rz zr]; exists z; apply/andP; split.
  - rewrite (le_lt_trans _ rz)// -mulrBr ler_pM2l// -(@ler_pM2l _ 12)//.
    rewrite mulrBr divff// (@natrM _ 3 4) -mulrA divff// mulr1.
    by rewrite mulrAC divff// mul1r -lerBlDr opprK natr1.
  - rewrite (lt_le_trans zr)// -mulrDr ler_pM2l// -(@ler_pM2l _ 12)//.
    rewrite mulrDr divff// (@natrM _ 3 4) mulrAC divff// mul1r.
    by rewrite natr1 (@natrM _ 2 2) -!mulrA divff// mulr1 -natrM ler_nat.
have [yqxr xrS] : ball (@ratr R y) (ratr q) `<=` ball x r /\ ball x r `<=` S.
  split => [z yqz|z /rat_in_itvoo[p]].
  - rewrite /ball/= -(subrK (ratr y) x) -(addrA _ (ratr y)).
    rewrite (le_lt_trans (ler_normD _ _))// (splitr r) ltrD//.
      by apply: le_ball yxr; rewrite ler_pM2l// lef_pV2 ?posrE// ler_nat.
    by rewrite (lt_trans yqz).
  - rewrite in_itv/= => /andP[xzp pr]; apply: (rS (ratr p)) => //=.
    + by rewrite sub0r normrN gtr0_norm// (le_lt_trans _ xzp).
    + exact: le_lt_trans xzp.
exists y, q; split; last exact: subset_trans xrS.
exact/mem_set/ball_sym/(le_ball _ yxr)/ltW.
Qed.

Section countable_isolated.
Context { : realType}.
Variable : set R.

Fact ( : R) : isolated S x -> exists ,
let : set R := ball (@ratr R cr.1) (ratr cr.2) in
x \in B /\ (forall : R, isolated S y -> y \in B -> x = y).

Proof.

move=> Sx.
have [e Sxe] : exists : {posnum R},
    forall : R, isolated S y -> y \in (ball x e%:num : set R) -> x = y.
  case: Sx => [xS/= [V xV /seteqP[VSx _]]].
  have [e /= e0 exV] : \forall \near 0^'+, ball x e `<=` V°.
    apply: open_subball; first exact: open_interior.
    by move/nbhs_interior : xV; exact: nbhs_singleton.
  have e20 : 0 < e / 2 by rewrite divr_gt0.
  exists (PosNum e20) => y [Sy [/= U yU USy /set_mem xey]].
  apply/eqP/negPn/negP => xy.
  suff : (V `&` S) y by move/VSx/esym; exact/eqP.
  split => //; last exact/set_mem.
  apply: interior_subset; apply: exV xey => //.
  by rewrite /ball_/= sub0r normrN gtr0_norm// gtr_pMr// invf_lt1// ltr1n.
have [c [r [xcr crxe]]] : exists ,
  let : set R := ball (@ratr R c) (ratr r) in x \in B /\ B `<=` ball x e%:num.
  by apply: open_subball_rat; [exact: ball_open|exact/mem_set/ballxx].
by exists (c, r); split=> //= y /Sxe /[!inE] /[swap] /crxe /[swap] /[apply].
Qed.

Lemma : countable (isolated S).

Proof.

apply/pcard_injP => /=.
pose g := if pselect (isolated S r) is left H then
  sval (cid (isolated_rat_ball H)) else 0.
have /card_bijP[h /bij_inj injh] := card_rat2.
exists (set_val \o h \o to_setT \o g) => x y /set_mem xS /set_mem yS /=.
rewrite /= /g; case: pselect => // xS'; case: pselect => // yS'.
case: cid => //= [ar [xar Nxar]]{xS'}; case: cid => //= [bd [ybd Nybd]]{yS'} ab.
have /injh/(congr1 (fun => \val x)) : h (to_setT ar) = h (to_setT bd).
  move: (h (to_setT ar)) (h (to_setT bd)) ab => [n nT] [m mT].
  by rewrite !set_valE/= => ->; congr exist.
by rewrite -inv_to_setT !funK ?inE// => {}ab; apply: Nxar => //; rewrite ab.
Qed.

End countable_isolated.

Lemma { : realFieldType} { : normedModType R}
( : set M) : closed K -> ~ K z ->
\forall \near 0^'+, closed_ball z d `&` K = set0.

Proof.

rewrite -openC => /open_subball /[apply]; move=> [e /= e0].
move=> /(_ (e / 2)) /= ; rewrite sub0r normrN gtr0_norm ?divr_gt0//.
rewrite ltr_pdivrMr// ltr_pMr// ltr1n => /(_ erefl isT).
move/subsets_disjoint; rewrite setCK => ze2K0.
exists (e / 2); first by rewrite /= divr_gt0.
move=> x /= + x0; rewrite sub0r normrN gtr0_norm// => xe.
by move: ze2K0; apply: subsetI_eq0 => //=; exact: closed_ball_subset.
Qed.

Lemma ( : realType) ( : normedModType R) ( : V)
( : R) : 0 < r -> (closed_ball x r)° = ball x r.

Proof.

move=> r0; rewrite eqEsubset; split; last first.
  by rewrite -open_subsetE; [exact: ball_open | exact: subset_closure].
move=> /= t; rewrite closed_ballE // /interior /= -nbhs_ballE => [[]] s s0.
have [-> _|nxt] := eqVneq t x; first exact: ballxx.
near ((0 : R^o)^') => e; rewrite -ball_normE /closed_ball_ => tsxr.
pose z := t + `|e| *: (t - x); have /tsxr /= : `|t - z| < s.
  rewrite opprD addNKr normrN normrZ normr_id.
  rewrite -ltr_pdivlMr ?(normr_gt0,subr_eq0) //.
  by near: e; apply/dnbhs0_lt; rewrite divr_gt0 // normr_gt0 subr_eq0.
rewrite /z opprD addrA -scalerN -{1}(scale1r (x - t)) opprB -scalerDl normrZ.
apply lt_le_trans; rewrite ltr_pMl; first by rewrite normr_gt0 subr_eq0 eq_sym.
by rewrite ger0_norm // ltrDl normr_gt0; near: e; exists 1 => /=.
Unshelve. all: by end_near. Qed.

Lemma ( : realType) ( : normedModType R) ( : V)
( : R) : 0 < r -> open_nbhs x (closed_ball x r)°.

Proof.

move=> r0; split; first exact: open_interior.
by rewrite interior_closed_ballE //; exact: ballxx.
Qed.

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

Proof.

move=> x _; rewrite withinET; exists (closed_ball x 1).
by apply/nbhs_closedballP; exists 1%:pos.
by split; [apply: closed_ballR_compact | apply: closed_ball_closed].
Qed.

Section bigcup_ointsub_lemmas.
Context { : realType} { : set R}.

Lemma : open U -> U (ratr q) ->
ratr q \in bigcup_ointsub U q.

Proof.

move=> oU Uq.
have [e /= e0 eU] := open_subball oU Uq.
pose B := ball (@ratr R q) (e / 2).
have Bq : B (ratr q) by apply: ballxx; rewrite divr_gt0.
apply/mem_set; exists B => //; split => //; split.
- exact: ball_open.
- by rewrite /B ball_itv; exact: interval_is_interval.
- apply: eU => //; last by rewrite divr_gt0.
rewrite ball_normE/= /ball/= sub0r normrN gtr0_norm ?divr_gt0//.
by rewrite gtr_pMr// invf_lt1// ltr1n.
Qed.

Lemma ( : rat) :
bigcup_ointsub U p `&` bigcup_ointsub U q !=set0 ->
bigcup_ointsub U p = bigcup_ointsub U q.

Proof.

move=> [x /= [[A [[oA itvA AU Ap Ax]]] [B [[oB itvB BU Bq Bx]]]]].
rewrite eqEsubset; split.
- apply: bigcup_ointsub_sup.
  + exact: open_bigcup_ointsub.
  + exact: is_interval_bigcup_ointsub.
  + exact: bigcup_ointsub_sub.
  + exists (A `|` B) => /= ; last by right.
    split; last by left.
    split; [exact: openU| |by rewrite subUset].
    apply/connected_intervalP/connectedU; [|exact/connected_intervalP..].
    by exists x.
- apply: bigcup_ointsub_sup.
  + exact: open_bigcup_ointsub.
  + exact: is_interval_bigcup_ointsub.
  + exact: bigcup_ointsub_sub.
  + exists (A `|` B) => /= ; last by left.
    split; last by right.
    split; [exact: openU| |by rewrite subUset].
    apply/connected_intervalP/connectedU; [|exact/connected_intervalP..].
    by exists x.
Qed.

End bigcup_ointsub_lemmas.

proof that an open set of real numbers can be written as the union of disjoint open intervals

Module .
Section opensetdisjointitvs.
Context { : realType} ( : set R).
Hypothesis : open U.

We first work out a proof where disjoint open intervals are indexed by rational numbers. The "sequence" of open intervals in question is `lt_disjoint_rat_seq`. This is the "sequence" of `bigcup_ointsub U` that are non-overlapping.

Section rat_index.
Context ( : rat -> nat) ( : nat -> rat).
Hypotheses ( : cancel f g) ( : cancel g f).

Definition := [set | forall , U (ratr p) ->
(f p < f q)%N -> bigcup_ointsub U q `&` bigcup_ointsub U p = set0].

Let :
U = \bigcup_( in lt_disjoint) bigcup_ointsub U q.

Proof.

rewrite [LHS]open_bigcup_rat//; apply/seteqP; split => /=; last first.
  by move=> r [q/= ?] Uqr; exists q => //=; exact: bigcup_ointsub_mem Uqr.
move=> r [q/= Uq] Uqr.
suff [p_idx [pUq Up]] : exists ,
    let := g p_idx in ratr p \in bigcup_ointsub U q /\
    forall , ratr q' \in bigcup_ointsub U q -> (f p <= f q')%N.
  have q_p : bigcup_ointsub U q `&` bigcup_ointsub U (g p_idx) !=set0.
    exists (ratr (g p_idx)); split; first exact/set_mem.
    apply/set_mem; rewrite bigcup_ointsubxx//.
    by move/set_mem : pUq; exact: bigcup_ointsub_sub.
  exists (g p_idx).
  - rewrite /= => q' Uq' q'p.
    apply/not_notP => /eqP/set0P[s [ps ts]].
    suff : ratr q' \in bigcup_ointsub U q by move/Up; rewrite leqNgt q'p.
    rewrite (@nondisjoint_bigcup_ointsub _ _ _ (g p_idx))//.
    rewrite (@nondisjoint_bigcup_ointsub _ _ _ q') ?bigcup_ointsubxx//.
    by exists s.
  - by rewrite (@nondisjoint_bigcup_ointsub _ _ _ q)// setIC.
pose P := [pred : 'I_(f q).+1 | ratr (g i) \in bigcup_ointsub U q].
have Pord_max : P ord_max.
  by rewrite /P/= cfg// bigcup_ointsubxx//; exact/set_mem.
pose min : 'I_(f q).+1 := [arg min_( < ord_max | P i) idfun i].
exists min => /=; split.
- by rewrite /min; case: arg_minnP.
- move=> q' pUp; rewrite /min; case: arg_minnP => //= i giq ismall.
  rewrite cgf.
  have [fq'fq|fqfq'] := ltnP (f q') (f q).+1.
    have := ismall (Ordinal fq'fq).
    by rewrite cfg => /(_ pUp).
  by rewrite (leq_trans _ (ltnW fqfq'))// (ismall ord_max).
Qed.

Let : set R :=
if pselect (lt_disjoint q) then bigcup_ointsub U q else set0.

Let : trivIset (U \o ratr) lt_disjoint_rat_seq0.

Proof.

apply/trivIsetP => /= i j Ui Uj.
wlog : i j Ui Uj / i < j.
  move=> wlg; rewrite neq_lt => /orP[|] ij.
    by rewrite wlg// lt_eqF.
  by rewrite setIC wlg// lt_eqF.
move=> ij _.
rewrite /lt_disjoint_rat_seq0/=.
case: pselect => disj_i; case: pselect => disj_j; rewrite ?(setI0,set0I)//.
have [?|fjfi] := ltnP (f i) (f j); first by rewrite setIC disj_j.
rewrite disj_i// ltn_neqAle fjfi andbT.
have : i != j by rewrite lt_eqF.
apply: contra => /eqP.
by move/can_inj : cfg => /[apply] => /esym/eqP.
Qed.

Let :
trivIset (U \o ratr \o g) (lt_disjoint_rat_seq0 \o g).

Proof.

apply/trivIsetP => i j/= Ugi Ugj ij.
move/trivIsetP : lt_disjoint_rat_seq0_trivIset => /(_ (g i) (g j)) /=.
by apply => //; apply: contra ij; move/eqP/(can_inj cgf)/eqP.
Qed.

Let :
ratr q \notin U -> lt_disjoint_rat_seq0 q = set0.

Proof.

move=> qU.
rewrite /lt_disjoint_rat_seq0; case: pselect => //= disj_q.
rewrite /bigcup_ointsub bigcup0// => B/=[[]oB iB].
by move=> /[apply] /mem_set; rewrite (negPf qU).
Qed.

Let :
open (lt_disjoint_rat_seq0 q) /\ is_interval (lt_disjoint_rat_seq0 q).

Proof.

split.
- rewrite /lt_disjoint_rat_seq0; case: pselect => //= _.
  + exact: open_bigcup_ointsub.
  + exact: open0.
- rewrite /lt_disjoint_rat_seq0; case: pselect => //= _.
  + exact: is_interval_bigcup_ointsub.
  + by [].
Qed.

Let : U = \bigcup_ lt_disjoint_rat_seq0 q.

Proof.

rewrite bigcup_lt_disjoint bigcup_mkcond; apply: eq_bigcup => // q _.
rewrite /lt_disjoint_rat_seq0; case: pselect => //= Icondq.
- by rewrite mem_set.
- by rewrite memNset.
Qed.

Let :
U = \bigcup_( in [set | U (ratr n)]) lt_disjoint_rat_seq0 q.

Proof.

rewrite [LHS]bigcup_lt_disjoint_rat_seq0 [RHS]bigcup_mkcond.
apply: eq_bigcupr => q _; case: ifPn => //.
rewrite notin_setE/= => Uq.
by rewrite lt_disjoint_rat_seq0_set0// memNset.
Qed.

Definition : set R :=
if ratr q \in U then lt_disjoint_rat_seq0 q else set0.

Lemma :
open (lt_disjoint_rat_seq q) /\ is_interval (lt_disjoint_rat_seq q).

Proof.

by rewrite /lt_disjoint_rat_seq; case: ifPn => qU//; split. Qed.

Lemma : trivIset setT (lt_disjoint_rat_seq \o g).

Proof.

move/trivIset_mkcond: lt_disjoint_rat_seq0_trivIset => // /trivIsetP H.
apply/trivIsetP => i j/= _ _ ij.
rewrite /lt_disjoint_rat_seq; case: ifPn => //; rewrite ?(setI0,set0I)//.
rewrite /lt_disjoint_rat_seq0; case: pselect => /=; rewrite ?(setI0,set0I)//.
case: ifPn => //; rewrite ?(setI0,set0I)//.
case: pselect => /=; rewrite ?(setI0,set0I)//.
move=> disj_gj gjU K3 K4.
have := H (g i) (g j) Logic.I Logic.I.
rewrite !ifT//.
rewrite /lt_disjoint_rat_seq0/=; case: pselect => //=; case: pselect => //= _ _.
apply.
by apply: contra ij => /eqP/(can_inj cgf)/eqP.
Qed.

Lemma : U = \bigcup_ lt_disjoint_rat_seq q.

Proof.

rewrite [LHS]bigcup_U_lt_disjoint_rat_seq.
rewrite [in LHS]bigcup_mkcond [in RHS]bigcup_mkcond.
apply: eq_bigcupr => q _.
by rewrite [in RHS]mem_set.
Qed.

End rat_index.

now the proof where disjoint open intervals are indexed by natural numbers

Lemma : exists : nat -> set R,
[/\ forall , open (I q) /\ is_interval (I q),
trivIset setT I & U = \bigcup_ I q].

Proof.

have /card_set_bijP[/= f] := card_rat.
rewrite setTT_bijective => -[g cfg cgf].
exists (lt_disjoint_rat_seq f \o g); split.
- by move=> n; exact: lt_disjoint_rat_seq_open_itv.
- exact: lt_disjoint_rat_seq_trivIset.
- rewrite (bigcup_lt_disjoint_rat_seq cfg cgf) [LHS](reindex_bigcup g setT)//.
by move=> q/= _; exists (f q).
Qed.

End opensetdisjointitvs.
End OpenSetDisjointItvs.

Section open_set_disjoint_real_intervals.
Context { : realType} ( : set R).
Hypothesis : open U.

Definition : nat -> set R :=
sval (cid (OpenSetDisjointItvs.open_disjoint_itv oU)).

Lemma : open (open_disjoint_itv i).

Proof.

by rewrite /open_disjoint_itv; case: cid => //= I [/(_ i)[]]. Qed.

Lemma : is_interval (open_disjoint_itv i).

Proof.

by rewrite /open_disjoint_itv; case: cid => //= I [/(_ i)[]]. Qed.

Lemma : trivIset [set: nat] open_disjoint_itv.

Proof.

by rewrite /open_disjoint_itv; case: cid => //= I [_]. Qed.

Lemma : U = \bigcup_ open_disjoint_itv q.

Proof.

by rewrite /open_disjoint_itv; case: cid => //= I [_]. Qed.

End open_set_disjoint_real_intervals.

Section EquivalenceNorms.
Context { : realType}.

Let ( : vectType R) : R :=
\big[Order.max/0]_( < \dim (@fullv _ V)) `|coord (vbasis fullv) i x|.

Definition ( : vectType R) : Type := V.

. ( R) := Vector.on (max_space V).

. ( R) := Pointed.copy (max_space V) V^o.

Let ( : vectType R) ( : V) : 0 <= max_norm x.

Proof.

rewrite /max_norm.
by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP.
Qed.

Let ( : vectType R) ( : V) :
`|coord (vbasis fullv) i x| <= max_norm x :> R.

Proof.

rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl.
rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl];
case: ifP => [/ltW|]// /negbT.
set b := (X in _ < X).
have bR : b \is Num.real by apply: bigmax_real => // a _; apply: normr_real.
have /comparable_leNgt <- :=
real_comparable bR (normr_real (coord (vbasis fullv) j x)).
by move=> /(le_trans IHl).
Qed.

Let ( : vectType R) : @max_norm V 0 = 0.

Proof.

apply: le_anti; rewrite max_norm_ge0 andbT.
apply: bigmax_le => // i _.
have <-: \sum_( < \dim (@fullv _ V)) 0 *: (vbasis (@fullv _ V))`_i = 0.
under eq_bigr do rewrite scale0r.
by rewrite sumr_const mul0rn.
by rewrite coord_sum_free ?normr0// (basis_free (vbasisP _)).
Qed.

Let ( : vectType R) ( : V) :
max_norm (x + y) <= max_norm x + max_norm y.

Proof.

apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0.
by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm.
Qed.

Let ( : vectType R) ( : V) : max_norm x = 0 -> x = 0.

Proof.

move=> x0; rewrite (coord_vbasis (memvf x)).
suff: forall , coord (vbasis fullv) i x = 0.
by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r.
by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm.
Qed.

Let ( : vectType R) ( : V) : max_norm (r *: x) = `|r| * max_norm x.

Proof.

rewrite /max_norm.
under eq_bigr do rewrite linearZ/= normrM.
elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0.
by rewrite !big_cons IHl maxr_pMr.
Qed.

. ( R) := Norm.isSemiNorm.Build R V
  (@max_norm V) (max_norm0 V) (@max_norm_ge0 V) (@ler_max_normD V)
  (@max_normZ V).

. ( R) := Norm.SemiNorm_isNorm.Build R V
  (@max_norm V) (@max_norm0_eq0 V).

Let ( : vectType R) ( : V) : max_norm (x *+ n) = max_norm x *+ n.

Proof.

exact: (Norm.Theory.normMn (@normed_module_max_norm__canonical__Norm_Norm V)).
Qed.

Let ( : vectType R) ( : V) : max_norm (- x) = max_norm x.

Proof.

exact: (Norm.Theory.normN (@normed_module_max_norm__canonical__Norm_Norm V)).
Qed.

. ( R) := Num.Zmodule_isNormed.Build R
  (max_space V) (@ler_max_normD V) (@max_norm0_eq0 V) (@max_normMn V)
  (@max_normN V).

. ( R) :=
  PseudoMetric.copy (max_space V) (pseudoMetric_normed (max_space V)).

. ( R) :=
  NormedZmod_PseudoMetric_eq.Build R (max_space V) erefl.

. ( R) :=
  isPseudoMetricNormedZmodule.Build _ (max_space V).

. ( R) :=
    PreUniformNmodule_isUniformNmodule.Build (max_space V)
  (@PseudoMetricNormedZmodule_add_unif_continuous _ (max_space V)).

. ( R) :=
    UniformNmodule_isUniformZmodule.Build (max_space V)
  (@PseudoMetricNormedZmodule_opp_unif_continuous _ (max_space V)).

. ( R) :=
  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V)
    (@Norm.normZ _ _ (@max_norm V)).

Lemma ( : vectType R) :
  compact (closed_ball (0 : max_space V) 1).

Proof.

rewrite closed_ballE// /closed_ball_.
under eq_set do rewrite sub0r normrN.
rewrite -[forall , _]/(compact _).
pose f ( : {ptws 'I_(\dim (@fullv _ V)) -> R}) : V :=
  \sum_( < \dim (@fullv _ V)) X i *: (vbasis fullv)`_i.
have -> : [set : max_space V | `|x| <= 1] =
          f @` [set | forall , `[-1, 1]%classic (X i)].
  apply/seteqP; split=> [x/= x1|x/= [X X1 <-]].
  (* FIXME: The type annotation on x is mandatory, otherwise we try to unify V
     with its eta-expansion. *)
  - exists (coord (vbasis fullv) ^~ (x : V)); last first.
      exact/esym/coord_vbasis/memvf.
    by move=> i; rewrite in_itv/= -ler_norml (le_trans _ x1) ?le_coord_max_norm.
  - rewrite /normr/= /max_norm bigmax_le => //= i _.
    by rewrite coord_sum_free ?ler_norml; [exact/basis_free/vbasisP|exact: X1].
apply: (@continuous_compact _ _ (f : _ -> max_space V)).
- apply/continuous_subspaceT/sum_continuous => /= i _ x.
  exact/continuousZr_tmp/proj_continuous.
- apply: (@tychonoff 'I_(\dim (@fullv _ V)) (fun=> R^o)
    (fun=> `[-1, 1]%classic)) => _.
  exact: segment_compact.
Qed.

Lemma ( : vectType R) ( : Norm.Norm.type V) :
exists2 , 0 < M & forall : max_space V, N' x <= M * N x /\ N x <= M * N' x.

Proof.

suff: forall ( : Norm.Norm.type V), exists2 ,
    0 < M & forall : max_space V, `|x| <= M * N x /\ N x <= M * `|x|.
  move=> /[dup] /(_ N) []/= M M0 Noo /(_ N') []/= M' M'0 N'oo.
  exists (M * M') => [|x]; first exact: mulr_gt0.
  move: Noo N'oo => /(_ x) [] Nge Nle /(_ x) [] N'ge N'le.
  split; first by apply: (le_trans N'le); rewrite mulrAC mulrC ler_pM2r.
  by rewrite (le_trans Nle)// -mulrA ler_pM2l.
move=> {N'}N.
set M0 := 1 + \sum_( < \dim (@fullv _ V)) N (vbasis fullv)`_i.
have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0// => ? _; exact: Norm.norm_ge0.
have leNoo ( : max_space V) : N x <= M0 * `|x|.
  rewrite [in leLHS](coord_vbasis (memvf (x : V))).
  rewrite (le_trans (Norm.Theory.ler_norm_sum _ _ _))//.
  rewrite mulrDl mul1r mulr_suml ler_wpDl// ler_sum => //= i _.
  by rewrite Norm.normZ mulrC ler_pM// ?le_coord_max_norm// Norm.norm_ge0.
have NC0 : continuous (N : max_space V -> R).
  move=> /= x; rewrite /continuous_at.
  apply: cvg_zero.
  apply/cvgr0Pnorm_le.
  move=> /= e e0.
  near=> y.
  rewrite -[_ y]/(N y - N x) (@le_trans _ _ (N (y - x)))//.
    apply/ler_normlP.
    have NB a b : N a <= N b + N (a - b).
      by rewrite (le_trans _ (Norm.ler_normD _ _))// subrKC.
    by rewrite opprB !lerBlDl NB -opprB Norm.Theory.normN NB.
  rewrite (le_trans (leNoo _))// mulrC -ler_pdivlMr// -opprB normrN.
  by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0].
have: compact [set : max_space V | `|x| = 1].
  apply: (subclosed_compact _ (@sup_closed_ball_compact V)).
  - apply: (@preimage_closed _ _ _ [set 1 : R]); last exact: closed_eq.
    by move=> *; exact: norm_continuous.
  - by move => x/=; rewrite closed_ballE// /closed_ball_/= sub0r normrN => ->.
move=> /(@continuous_compact _ _ (N : max_space V -> R)) -/(_ _)/wrap[].
  exact: continuous_subspaceT.
move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[].
  move=> /= x; rewrite /continuous_at.
  apply: (@continuous_in_subspaceT _ _
    [set N x | in [set : max_space V | `|x| = 1]] (@GRing.inv R)).
  move=> /= r /set_mem/= [y y1 <-].
  apply: inv_continuous.
  apply: contra_eq_neq y1 => /Norm.norm0_eq0 ->.
  by rewrite normr0 eq_sym oner_eq0.
move=> /compact_bounded[M1 [M1R /(_ (1 + M1))]] /(_ (ltr_pwDl ltr01 (lexx _))).
rewrite /globally/= => M1N.
exists (maxr M0 (1 + M1)) => [|x]; first by rewrite lt_max M00.
split; last by rewrite (le_trans (leNoo x))// ler_wpM2r// le_max lexx.
have [->|x0] := eqVneq x 0; first by rewrite normr0 Norm.norm0 mulr0.
have Nx0 : 0 < N x.
  rewrite lt0r Norm.norm_ge0 andbT.
  by move: x0; apply: contra_neq => /Norm.norm0_eq0.
have normx0 : 0 < `|x| by rewrite normr_gt0.
move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[].
  exists (N x / `|x|); last by rewrite invf_div.
  exists (`|x|^-1 *: x); last by rewrite Norm.normZ mulrC ger0_norm.
  by rewrite normrZ normfV normr_id mulVf// gt_eqF.
rewrite ger0_norm; first by rewrite divr_ge0// Norm.norm_ge0.
rewrite ler_pdivrMr// => /le_trans; apply.
by rewrite ler_pM2r// le_max lexx orbT.
Unshelve. all: by end_near. Qed.

Lemma ( : normedVectType R) ( : normedModType R)
( : {linear V -> W}) : continuous f.

Proof.

set V' := @fullv _ V.
set B := vbasis V'.
move=> /= x; rewrite /continuous_at.
rewrite [x in f x](coord_vbasis (memvf x)) raddf_sum.
rewrite (@eq_cvg _ _ _ _ (fun => \sum_( < \dim V') coord B i y *: f B`_i)).
move=> y; rewrite [y in LHS](coord_vbasis (memvf y)) raddf_sum.
by apply: eq_big => // i _; apply: linearZ.
apply: cvg_sum => i _.
rewrite [X in _ --> X]linearZ/= -/B.
apply: cvgZr_tmp.
move: x; apply/linear_bounded_continuous/bounded_funP => r/=.
have [M M0 MP] := equivalence_norms (@Num.norm _ V) (@max_norm V).
exists (M * r) => x.
move: MP => /(_ x) [Mx _] xr.
by rewrite (le_trans (le_coord_max_norm _ _))// (le_trans Mx) ?ler_wpM2l// ltW.
Qed.

End EquivalenceNorms.

Files

Module mathcomp.analysis.normedtype_theory.normed_module