Module mathcomp.analysis.normedtype_theory.normed_module

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


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

HBSource code

.

mixinSource code

RecordSource code

PseudoMetricNormedZmod_Tvs_isNormedModuleSource code

KSource code

VSource code

    

&Source code

PseudoMetricNormedZmodSource code

K V & Tvs K V := {
  normrZ : forall (

lSource code

: K) (

xSource code

: V), `| l *: x | = `| l | * `| x |;
}.

#[shortUsed by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

(

type=Used by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

"normedModType"Used by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

)

]Used by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

HBUsed by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

.

structureUsed by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

DefinitionUsed by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

NormedModuleUsed by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

 (

KUsed by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

:Used by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

numDomainTypeUsed by

• mathcomp.analysis.normedtype_theory.complete_normed_module

---

Source code

) :=
  {

TSource code

of PseudoMetricNormedZmod K T & Tvs K T
   & PseudoMetricNormedZmod_Tvs_isNormedModule K T}.

HBSource code

.

factorySource code

RecordSource code

PseudoMetricNormedZmod_Lmodule_isNormedModuleSource code

 (

KSource code

:Source code

numFieldTypeSource code

) V
    & PseudoMetricNormedZmod K V & GRing.Lmodule K V := {
 normrZ : forall (

lSource code

: K) (

xSource code

: V), `| l *: x | = `| l | * `| x |;
}.

HBSource code

.

buildersSource code

ContextSource code

KSource code

VSource code

&Source code

PseudoMetricNormedZmod_Lmodule_isNormedModuleSource code

K V.

Let

add_continuousSource code

: continuous (fun

xSource code

: V * V => x.1 + x.2).

Proof.

exact: add_continuous. Qed.

Let

scale_continuousSource code

: continuous (fun

zSource code

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

Let

ball_convex_setSource code

 (

xSource code

: convex_lmodType V) (

rSource code

: 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 _)); last first.
  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.

Let

locally_convex_setSource code

:
  exists2

BSource code

: set_system (convex_lmodType V),
    (forall

bSource code

, b \in B -> convex_set b) & basis B.

Proof.

exists [set

BSource code

| exists (

xSource code

: convex_lmodType V)

rSource code

, B = ball x r].
  by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex_set.
split; first by move=> B [x] [r] ->; exact: ball_open.
move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
Qed.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

  PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

  TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

Uniform_isTvsSource code

.Build K V locally_convex_set.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

  PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ.

HBSource code

.

endSource code

.

Section standard_topology_normedMod.
Variable

RSource code

: numFieldType.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

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

End standard_topology_normedMod.

Module

numFieldNormedTypeSource code

.

Section realType.
Variable (

RSource code

: realType).

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

GRingSource code

.ComAlgebra.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

VectorSource code

.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NormedModuleSource code

.copy R R^o.
End realType.

Section rcfType.
Variable (

RSource code

: rcfType).

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

GRingSource code

.ComAlgebra.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

VectorSource code

.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NormedModuleSource code

.copy R R^o.
End rcfType.

Section archiFieldType.
Variable (

RSource code

: archiRealFieldType).

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

GRingSource code

.ComAlgebra.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

VectorSource code

.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NormedModuleSource code

.copy R R^o.
End archiFieldType.

Section realFieldType.
Variable (

RSource code

: realFieldType).

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

GRingSource code

.ComAlgebra.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

VectorSource code

.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NormedModuleSource code

.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NumSource code

.RealField.on R.
End realFieldType.

Section numClosedFieldType.
Variable (

RSource code

: numClosedFieldType).

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

GRingSource code

.ComAlgebra.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

VectorSource code

.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NormedModuleSource code

.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NumSource code

.ClosedField.on R.
End numClosedFieldType.

Section numFieldType.
Variable (

RSource code

: numFieldType).

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

GRingSource code

.ComAlgebra.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

VectorSource code

.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NormedModuleSource code

.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NumSource code

.NumField.on R.
End numFieldType.

Module

ExportsUsed by

• mathcomp.analysis.esum
• mathcomp.analysis.hoelder

---

Source code

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

End numFieldNormedType.
Import numFieldNormedType.Exports.

Lemma

within_continuous_compNSource code

{

RSource code

: realFieldType} {

KSource code

: numDomainType}
    {

USource code

: pseudoMetricNormedZmodType K} (

fSource code

: R -> U) (

aSource code

bSource code

: 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_itvP; rewrite ltrN2 => /(_ ab)[cf fb fa].
apply/(continuous_within_itvP _ 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

pseudoMetric_normed

pseudoMetric_normed : Type -> Type pseudoMetric_normed is not universe polymorphic Arguments pseudoMetric_normed M%type_scope pseudoMetric_normed is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.pseudoMetric_normed Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 250, characters 11-30

---

Source code

 (

MSource code

: Type) : Type := M.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

KSource code

:Source code

numFieldTypeSource code

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

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

KSource code

:Source code

numFieldTypeSource code

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

Module

pseudoMetric_from_normedZmodTypeSource code

.
Section pseudoMetric_from_normedZmodType.
Variables (

KSource code

: numFieldType) (

MSource code

: normedZmodType K).

Notation

TSource code

:= (pseudoMetric_normed M).

Definition

ball

pseudoMetric_from_normedZmodType.ball : forall [K : numFieldType] [M : normedZmodType K], pseudoMetric_normed M -> K -> set (pseudoMetric_normed M) pseudoMetric_from_normedZmodType.ball is not universe polymorphic Arguments pseudoMetric_from_normedZmodType.ball [K M] x r%ring_scope _ pseudoMetric_from_normedZmodType.ball is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.pseudoMetric_from_normedZmodType.ball Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 263, characters 11-15

---

Source code

 (

xSource code

: T) (

rSource code

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

Definition

ent

pseudoMetric_from_normedZmodType.ent : forall [K : numFieldType] [M : normedZmodType K], set_system (pseudoMetric_normed M * pseudoMetric_normed M) pseudoMetric_from_normedZmodType.ent is not universe polymorphic Arguments pseudoMetric_from_normedZmodType.ent [K M] _ pseudoMetric_from_normedZmodType.ent is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.pseudoMetric_from_normedZmodType.ent Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 265, characters 11-14

---

Source code

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

Definition

nbhs

pseudoMetric_from_normedZmodType.nbhs : forall [K : numFieldType] [M : normedZmodType K], pseudoMetric_normed M -> set_system (pseudoMetric_normed M) pseudoMetric_from_normedZmodType.nbhs is not universe polymorphic Arguments pseudoMetric_from_normedZmodType.nbhs [K M] x _ pseudoMetric_from_normedZmodType.nbhs is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.pseudoMetric_from_normedZmodType.nbhs Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 267, characters 11-15

---

Source code

 (

xSource code

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

Lemma

nbhsESource code

: nbhs = nbhs_ ent

Proof.

by []. Qed.

#[export]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

hasNbhsSource code

.Build T nbhs.

Lemma

ball_centerSource code

xSource code

 (

eSource code

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

Proof.

by rewrite /ball/= subrr normr0. Qed.

Lemma

ball_symSource code

xSource code

ySource code

 (

eSource code

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

Proof.

by rewrite /ball /= distrC. Qed.

Lemma

ball_triangleSource code

xSource code

ySource code

zSource code

e1Source code

e2Source code

: 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

entourageESource code

: ent = entourage_ ball.

Proof.

by []. Qed.

#[export]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

@Nbhs_isPseudoMetricSource code

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

End pseudoMetric_from_normedZmodType.
Module

ExportsSource code

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

HBSource code

.

factorySource code

RecordSource code

Lmodule_isNormedSource code

 (

RSource code

:Source code

numFieldTypeSource code

) M
    & GRing.Lmodule R M := {
 norm : M -> R;
 ler_normD : forall

xSource code

ySource code

, norm (x + y) <= norm x + norm y ;
 normrZ : forall (

lSource code

: R) (

xSource code

: M), norm (l *: x) = `|l| * norm x ;
 normr0_eq0 : forall

xSource code

: M, norm x = 0 -> x = 0
}.

HBSource code

.

buildersSource code

ContextSource code

RSource code

MSource code

&Source code

Lmodule_isNormedSource code

R M.

Lemma

normrMnSource code

xSource code

nSource code

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

Proof.

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

Lemma

normrNSource code

xSource code

: norm (- x) = norm x.

Proof.

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

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NumSource code

.Zmodule_isNormed.Build
  R M ler_normD normr0_eq0 normrMn normrN.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

PseudoMetricSource code

.copy M (pseudoMetric_normed M).

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

isPointedSource code

.Build M 0.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

NormedZmod_PseudoMetric_eqSource code

.Build R M erefl.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ.

HBSource code

.

endSource code

.

Lemma

scaler1Used by

• mathcomp.analysis.derive
• mathcomp.analysis.hoelder
• mathcomp.analysis.gauss_integral
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
• mathcomp.analysis.probability_theory.normal_distribution
• mathcomp.analysis.probability_theory.beta_distribution
• mathcomp.analysis.realfun

---

Source code

{

RSource code

: numFieldType}

hSource code

: h%:A = h :> R.

Proof.

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

Lemma

limf_esup_dnbhsNUsed by

• mathcomp.analysis.realfun

---

Source code

{

RSource code

: realType} (

fSource code

: R -> \bar R) (

aSource code

: R) :
  limf_esup f a^' = limf_esup (fun

xSource code

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

cvg_patchUsed by

• mathcomp.analysis.ftc

---

Source code

{

RSource code

: realType} (

fSource code

: R -> R^o) (

aSource code

bSource code

: R) (

xSource code

: R) : (a < b)%R ->
  x \in `]a, b[ ->
  f @ (x : subspace `[a, b]) --> f x ->
  (f \_ `[a, b] x) @[

xSource code

--> 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//; last first.
  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; last first.
  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

normrZVSource code

 (

KSource code

: numDomainType) (

VSource code

: normedModType K) (

xSource code

: V) :
  `|x| \in GRing.unit -> `| `| x |^-1 *: x | = 1.

Proof.

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

Definition

self_sub

self_sub : forall {K : numDomainType} {V W : normedModType K}, (V -> W) -> V * V -> W self_sub is not universe polymorphic Arguments self_sub {K V W} f%function_scope x / The reduction tactics unfold self_sub when applied to 5 arguments self_sub is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.self_sub Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 368, characters 11-19

---

Source code

 (

KSource code

: numDomainType) (

VSource code

WSource code

: normedModType K)
  (

fSource code

: V -> W) (

xSource code

: V * V) : W := f x.1 - f x.2.
Arguments self_sub {K V W} f x /.

Section NormedModule_numFieldType.
Variables (

KSource code

: numFieldType) (

VSource code

: normedModType K).

Lemma

normfZVSource code

 (

xSource code

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

Proof.

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

Lemma

cvg_at_rightESource code

 (

fSource code

: K -> V)

xSource code

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

Proof.

move=> cvfx; apply/Logic.eq_sym.
apply: (@cvg_lim _ _ _ (at_right _)) => // 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

cvg_at_leftESource code

 (

fSource code

: K -> V)

xSource code

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

Proof.

move=> cvfx; apply/Logic.eq_sym.
apply: (@cvg_lim _ _ _ (at_left _)) => // 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

scaler_continuousUsed by

• mathcomp.analysis.derive

---

Source code

kSource code

: continuous (fun

xSource code

: V => k *: x).

Proof.

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

Lemma

scalel_continuousUsed by

• mathcomp.analysis.derive

---

Source code

 (

xSource code

: V) : continuous (fun

kSource code

: K => k *: x).

Proof.

by move=> k; apply: (cvg_comp2 cvg_id (cvg_cst _) (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 (

KSource code

: numFieldType) (

USource code

VSource code

: normedModType K).

Lemma

continuous_shiftSource code

 (

fSource code

: U -> V)

uSource code

:
  {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

continuous_withinNshiftxUsed by

• mathcomp.analysis.realfun

---

Source code

 (

fSource code

: U -> V)

uSource code

:
  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

near0ZUsed by

• mathcomp.analysis.derive

---

Source code

{

RSource code

: numFieldType} {

VSource code

: normedModType R} (

ySource code

: V) (

PSource code

: set V) :
  (\forall

xSource code

\near 0, P x) -> (\forall

kSource code

\near 0, P (k *: y)).

Proof.

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

Section NVS_continuity_mul.
Context {

KSource code

: numFieldType}.

Lemma

mul_continuousUsed by

• mathcomp.analysis.derive

---

Source code

: continuous (fun

zSource code

: K * K => z.1 * z.2).

Proof.

exact: scale_continuous. Qed.

Lemma

mulrl_continuousUsed by

• mathcomp.analysis.measurable_realfun

---

Source code

 (

xSource code

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

Proof.

exact: scaler_continuous. Qed.

Lemma

mulrr_continuousUsed by

• mathcomp.analysis.measurable_realfun

---

Source code

 (

ySource code

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

Proof.

exact: scalel_continuous. Qed.

Lemma

inv_continuousUsed by

• mathcomp.analysis.kernel

---

Source code

 (

xSource code

: 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 {

KSource code

: numFieldType} {

VSource code

: normedModType K} {

TSource code

: Type}.
Context (

FSource code

: set_system T) {

FFSource code

: Filter F}.
Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a b : V).

Lemma

cvgZUsed by

• mathcomp.analysis.derive

---

Source code

sSource code

fSource code

kSource code

aSource code

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

xSource code

--> F] --> k *: a.

Proof.

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

Lemma

is_cvgZSource code

sSource code

fSource code

: cvg (s @ F) ->
  cvg (f @ F) -> cvg ((fun

xSource code

=> s x *: f x) @ F).

Proof.

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

Lemma

cvgZr_tmpUsed by

• mathcomp.analysis.derive

---

Source code

sSource code

kSource code

aSource code

: s @ F --> k -> s x *: a @[

xSource code

--> F] --> k *: a.

Proof.

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

Lemma

is_cvgZr_tmpSource code

sSource code

aSource code

: cvg (s @ F) -> cvg ((fun

xSource code

=> s x *: a) @ F).

Proof.

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

Lemma

cvgZl_tmpUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.derive

---

Source code

kSource code

fSource code

aSource code

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

Proof.

by apply: cvgZ => //; exact: cvg_cst. Qed.

Lemma

is_cvgZl_tmpUsed by

• mathcomp.analysis.sequences

---

Source code

kSource code

fSource code

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

Proof.

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

Lemma

is_cvgZlESource code

kSource code

fSource code

: 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//; apply: cvgP.
Qed.

End cvg_composition_normed.
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgZr_tmp`")]
Notation

cvgZlSource code

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

is_cvgZlSource code

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

cvgZrSource code

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

is_cvgZrSource code

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

is_cvgZrESource code

:= is_cvgZlE (only parsing).

Section cvg_composition_field.
Context {

KSource code

: numFieldType}  {

TSource code

: Type}.
Context (

FSource code

: set_system T) {

FFSource code

: Filter F}.
Implicit Types (f g : T -> K) (a b : K).

Lemma

cvgVUsed by

• mathcomp.analysis.derive
• mathcomp.analysis.trigo
• mathcomp.analysis.realfun

---

Source code

fSource code

aSource code

: 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

cvgVPSource code

fSource code

aSource code

: 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

is_cvgVSource code

fSource code

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

Proof.

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

Lemma

cvgMUsed by

• mathcomp.analysis.pi_irrational
• mathcomp.analysis.ftc
• mathcomp.analysis.derive
• mathcomp.analysis.gauss_integral
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.probability_theory.normal_distribution
• mathcomp.analysis.probability_theory.beta_distribution
• mathcomp.analysis.realfun
• mathcomp.analysis.normedtype_theory.urysohn

---

Source code

fSource code

gSource code

aSource code

bSource code

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

Proof.

exact: cvgZ. Qed.

Lemma

cvgMr_tmpUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.gauss_integral

---

Source code

fSource code

aSource code

bSource code

: f @ F --> a -> f x * b @[

xSource code

--> F] --> a * b.

Proof.

exact: cvgZr_tmp. Qed.

Lemma

cvgMl_tmpUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.pi_irrational
• mathcomp.analysis.gauss_integral

---

Source code

gSource code

aSource code

bSource code

: g @ F --> b -> a * g x @[

xSource code

--> F] --> a * b.

Proof.

exact: cvgZl_tmp. Qed.

Lemma

is_cvgMSource code

fSource code

gSource code

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

Proof.

exact: is_cvgZ. Qed.

Lemma

is_cvgMl_tmpSource code

gSource code

aSource code

 (

fSource code

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

Proof.

exact: is_cvgZl_tmp. Qed.

Lemma

is_cvgMlE_tmpSource code

gSource code

aSource code

 (

fSource code

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

Proof.

exact: is_cvgZlE. Qed.

Lemma

is_cvgMr_tmpSource code

fSource code

aSource code

 (

gSource code

:= 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

is_cvgMrE_tmpSource code

fSource code

aSource code

 (

gSource code

:= 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

cvgMlSource code

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

cvgMrSource code

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

is_cvgMrSource code

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

is_cvgMlSource code

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

is_cvgMlESource code

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

is_cvgMrESource code

:= is_cvgMlE_tmp (only parsing).

Section limit_composition_normed.
Context {

KSource code

: numFieldType} {

VSource code

: normedModType K} {

TSource code

: Type}.
Context (

FSource code

: set_system T) {

FFSource code

: ProperFilter F}.
Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a : V).

Lemma

limZSource code

sSource code

fSource code

: cvg (s @ F) -> cvg (f @ F) ->
  lim ((fun

xSource code

=> s x *: f x) @ F) = lim (s @ F) *: lim (f @ F).

Proof.

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

Lemma

limZr_tmpSource code

sSource code

aSource code

: cvg (s @ F) ->
  lim ((fun

xSource code

=> s x *: a) @ F) = lim (s @ F) *: a.

Proof.

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

Lemma

limZl_tmpUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.exp

---

Source code

kSource code

fSource code

: 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

limZlSource code

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

limZrSource code

:= limZl_tmp (only parsing).

Section limit_composition_field.
Context {

KSource code

: numFieldType} {

TSource code

: Type}.
Context (

FSource code

: set_system T) {

FFSource code

: ProperFilter F}.
Implicit Types (f g : T -> K).

Lemma

limMSource code

fSource code

gSource code

: 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 {

KSource code

: numFieldType}  {

TSource code

: Type}.
Context (

FSource code

: set_system T) {

FFSource code

: ProperFilter F}.
Implicit Types (f g : T -> K) (a b : K).

Lemma

limVSource code

fSource code

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

Proof.

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

Lemma

is_cvgVESource code

fSource code

: 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 {

TSource code

: Type} {

FSource code

: set_system T} {

FFSource code

: ProperFilter F} {

RSource code

: realFieldType}.
Implicit Types (f g h : T -> R) (a b : R).

Lemma

cvgr_to_geSource code

fSource code

aSource code

bSource code

: f @ F --> a -> (\near

FSource code

, b <= f F) -> b <= a.

Proof.

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

Lemma

cvgr_to_leSource code

fSource code

aSource code

bSource code

: f @ F --> a -> (\near

FSource code

, f F <= b) -> a <= b.

Proof.

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

Lemma

limr_geUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.derive
• mathcomp.analysis.realfun

---

Source code

xSource code

fSource code

: cvg (f @ F) -> (\near

FSource code

, x <= f F) -> x <= lim (f @ F).

Proof.

exact: cvgr_to_ge. Qed.

Lemma

limr_leUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.derive
• mathcomp.analysis.realfun

---

Source code

xSource code

fSource code

: cvg (f @ F) -> (\near

FSource code

, x >= f F) -> x >= lim (f @ F).

Proof.

exact: cvgr_to_le. Qed.

End ProperFilterRealType.

Section local_continuity.
Context {

KSource code

: numFieldType} {

VSource code

: normedModType K} {

TSource code

: topologicalType}.
Implicit Types (f g : T -> V) (s t : T -> K) (x : T) (k : K) (a : V).

Lemma

continuousNUsed by

• mathcomp.analysis.ftc
• mathcomp.analysis.derive
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.probability_theory.exponential_distribution
• mathcomp.analysis.realfun

---

Source code

 (

fSource code

: T -> V)

xSource code

:
  {for x, continuous f} -> {for x, continuous (fun

xSource code

=> - f x)}.

Proof.

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

Lemma

continuousDUsed by

• mathcomp.analysis.derive
• mathcomp.analysis.numfun
• mathcomp.analysis.gauss_integral

---

Source code

fSource code

gSource code

xSource code

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

Proof.

by move=> f_cont g_cont; apply: cvgD. Qed.

Lemma

continuousBUsed by

• mathcomp.analysis.ftc
• mathcomp.analysis.trigo
• mathcomp.analysis.numfun
• mathcomp.analysis.exp

---

Source code

fSource code

gSource code

xSource code

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

Proof.

by move=> f_cont g_cont; apply: cvgB. Qed.

Lemma

continuousZSource code

sSource code

fSource code

xSource code

:
  {for x, continuous s} -> {for x, continuous f} ->
  {for x, continuous (fun

xSource code

=> s x *: f x)}.

Proof.

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

Lemma

continuousZl_tmpUsed by

• mathcomp.analysis.derive

---

Source code

fSource code

kSource code

xSource code

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

Proof.

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

Lemma

continuousZr_tmpUsed by

• mathcomp.analysis.derive

---

Source code

sSource code

aSource code

xSource code

:
  {for x, continuous s} -> {for x, continuous (fun

zSource code

=> s z *: a)}.

Proof.

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

Lemma

continuousMUsed by

• mathcomp.analysis.ftc
• mathcomp.analysis.trigo
• mathcomp.analysis.numfun
• mathcomp.analysis.probability_theory.exponential_distribution
• mathcomp.analysis.realfun

---

Source code

sSource code

tSource code

xSource code

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

Proof.

by move=> f_cont g_cont; exact: cvgM. Qed.

Lemma

continuousVUsed by

• mathcomp.analysis.trigo
• mathcomp.analysis.realfun

---

Source code

sSource code

xSource code

: s x != 0 ->
  {for x, continuous s} -> {for x, continuous (fun

xSource code

=> (s x)^-1%R)}.

Proof.

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

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

continuousZrSource code

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

continuousZlSource code

:= continuousZr_tmp (only parsing).

Section cvg_fin.
Context {

RSource code

: numFieldType}.

Section filter.
Context {

FSource code

: set_system \bar R} {

FFSource code

: Filter F}.

Lemma

fine_fcvgUsed by

• mathcomp.analysis.lebesgue_measure
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation

---

Source code

aSource code

: F --> a%:E -> fine @ F --> a.

Proof.

move=> /(_ _)/= Fa; apply/cvgrPdist_lt=> // _/posnumP[e]; rewrite near_simpl.
by apply: Fa; apply/nbhs_EFin => /=; apply: (@cvgr_dist_lt _ _ _ (nbhs a)).
(* BUG: using cvgr_dist_lt without (nbhs _) expands the definition of nbhs, *)
(*    so that it is not recognized as a filter anymore *)
Qed.

Lemma

fcvg_is_fineUsed by

• mathcomp.analysis.realfun

---

Source code

aSource code

: F --> a%:E -> \near

FSource code

, F \is a fin_num.

Proof.

by apply; apply/nbhs_EFin; near=> x. Unshelve. all: by end_near. Qed.

End filter.

Section limit.
Context {

ISource code

: Type} {

FSource code

: set_system I} {

FFSource code

: Filter F} (

fSource code

: I -> \bar R).

Lemma

fine_cvgUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_measure
• mathcomp.analysis.measurable_realfun
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
• mathcomp.analysis.probability_theory.random_variable
• mathcomp.analysis.realfun
• mathcomp.analysis.normedtype_theory.urysohn

---

Source code

aSource code

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

Proof.

exact: fine_fcvg. Qed.

Lemma

cvg_is_fineSource code

aSource code

: f @ F --> a%:E -> \near

FSource code

, f F \is a fin_num.

Proof.

exact: fcvg_is_fine. Qed.

Lemma

cvg_EFinUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.ftc
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
• mathcomp.analysis.normedtype_theory.urysohn

---

Source code

aSource code

: (\near

FSource code

, f F \is a fin_num) -> fine \o f @ F --> a ->
  f @ F --> a%:E.

Proof.

move=> Ffin Fa P/= /nbhs_EFin /Fa; rewrite !near_simpl.
by apply: filterS2 Ffin => x /fineK->.
Qed.

Lemma

fine_cvgPUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_measure
• mathcomp.analysis.charge
• mathcomp.analysis.esum
• mathcomp.analysis.ftc
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.realfun
• mathcomp.analysis.normedtype_theory.urysohn

---

Source code

aSource code

:
   f @ F --> a%:E <-> (\near

FSource code

, f F \is a fin_num) /\ fine \o f @ F --> a.

Proof.

by split;[split;[exact: (@cvg_is_fine a)|exact: fine_cvg]|case; apply: cvg_EFin].
Qed.

Lemma

neq0_fine_cvgPUsed by

• mathcomp.analysis.gauss_integral

---

Source code

aSource code

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

End cvg_fin.

Section ecvg_realFieldType.
Context {

ISource code

} {

FSource code

: set_system I} {

FFSource code

: Filter F} {

RSource code

: realFieldType}.
Implicit Types f g u v : I -> \bar R.
Local Open Scope ereal_scope.

Lemma

cvgeDUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.charge
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
• mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation

---

Source code

fSource code

gSource code

aSource code

bSource code

:
  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

cvgeNUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.charge
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation
• mathcomp.analysis.realfun

---

Source code

fSource code

xSource code

: f @ F --> x -> - f x @[

xSource code

--> F] --> - x.

Proof.

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

Lemma

cvgeNPUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
• mathcomp.analysis.realfun

---

Source code

fSource code

aSource code

: - f x @[

xSource code

--> F] --> - a <-> f @ F --> a.

Proof.

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

Lemma

cvgeBUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.charge
• mathcomp.analysis.measure_theory.measure_function
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence
• mathcomp.analysis.probability_theory.random_variable
• mathcomp.analysis.realfun

---

Source code

fSource code

gSource code

aSource code

bSource code

:
  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

sube_cvg0Used by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation

---

Source code

fSource code

 (

kSource code

: \bar R) :
  k \is a fin_num -> (fun

xSource code

=> 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)//.
by apply: cvgeB => //; exact: cvg_cst.
Qed.

Lemma

abse_continuousSource code

: 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

cvg_abseUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence

---

Source code

fSource code

 (

aSource code

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

xSource code

--> F] --> `|a|%E.

Proof.

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

Lemma

is_cvg_abseUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence

---

Source code

 (

fSource code

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

xSource code

--> F]).

Proof.

by move/cvg_abse/cvgP. Qed.

Lemma

is_cvgeNUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence

---

Source code

fSource code

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

Proof.

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

Lemma

is_cvgeNESource code

fSource code

: 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

mule_continuousSource code

 (

rSource code

: 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 => //=; apply: cvg_cst.
- 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

cvgeZlUsed by

• mathcomp.analysis.charge
• mathcomp.analysis.measure_theory.measure_function
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition

---

Source code

fSource code

xSource code

ySource code

: y \is a fin_num ->
  f @ F --> x -> (fun

nSource code

=> y * f n) @ F --> y * x.

Proof.

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

Lemma

is_cvgeZlUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition

---

Source code

fSource code

ySource code

: y \is a fin_num ->
  cvg (f @ F) -> cvg ((fun

nSource code

=> y * f n) @ F).

Proof.

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

Lemma

cvgeZrUsed by

• mathcomp.analysis.charge
• mathcomp.analysis.measure_theory.probability_measure
• mathcomp.analysis.realfun

---

Source code

fSource code

xSource code

ySource code

: y \is a fin_num ->
  f @ F --> x -> (fun

nSource code

=> f n * y) @ F --> x * y.

Proof.

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

Lemma

is_cvgeZrSource code

fSource code

ySource code

: y \is a fin_num ->
  cvg (f @ F) -> cvg ((fun

nSource code

=> f n * y) @ F).

Proof.

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

Lemma

cvg_abse0PUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation

---

Source code

fSource code

: 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

cvgeM_gt0_pinftySource code

fSource code

gSource code

bSource code

:
  (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; last by near: n; exact: gfin.
by near: n; apply: (cvgr_ge b).
Unshelve. all: end_near. Qed.

Let

cvgeM_lt0_pinftySource code

  

fSource code

gSource code

bSource code

:
  (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; last 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

cvgeM_gt0_ninftySource code

fSource code

gSource code

bSource code

:
  (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

cvgeM_lt0_ninftySource code

fSource code

gSource code

bSource code

:
  (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

cvgeMUsed by

• mathcomp.analysis.charge
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation

---

Source code

fSource code

gSource code

 (

aSource code

bSource code

: \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)); last 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.
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sube_cvg0`")]
Notation

cvge_sub0Source code

:= sube_cvg0 (only parsing).
#[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `cvgeZl`")]
Notation

cvgeMlSource code

:= cvgeZl (only parsing).
#[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `is_cvgeZl`")]
Notation

is_cvgeMlSource code

:= is_cvgeZl (only parsing).
#[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `cvgeZr`")]
Notation

cvgeMrSource code

:= cvgeZr (only parsing).
#[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `is_cvgeZr`")]
Notation

is_cvgeMrSource code

:= is_cvgeZr (only parsing).

Section max_cts.
Context {

RSource code

: realType} {

TSource code

: topologicalType}.

Lemma

continuous_minUsed by

• mathcomp.analysis.normedtype_theory.urysohn

---

Source code

 (

fSource code

gSource code

: T -> R^o)

xSource code

:
  {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; [|exact: cvg_cst]; apply: cvgD; first exact: cvgD.
by apply: cvgN; apply: cvg_norm; apply: cvgB.
Qed.

Lemma

continuous_maxSource code

 (

fSource code

gSource code

: T -> R^o)

xSource code

:
  {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; [|exact: cvg_cst]; apply: cvgD; first exact: cvgD.
by apply: cvg_norm; apply: cvgB.
Qed.

End max_cts.

Lemma

limit_pointPUsed by

• mathcomp.analysis.sequences

---

Source code

 (

TSource code

: archiRealFieldType) (

ASource code

: set T) (

xSource code

: T) :
  limit_point A x <-> exists

a_Source code

: nat -> T,
    [/\ a_ @` setT `<=` A, forall

nSource code

, 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

nSource code

: nat => [set

zSource code

: T | `|x - z| < n.+1%:R^-1].
suff /(_ _)/cid-/all_sig[a_ anx] : forall

nSource code

, exists

aSource code

, 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

limit_point_infinite_setPUsed by

• mathcomp.analysis.sequences

---

Source code

{

RSource code

: archiRealFieldType} (

ESource code

: set R) (

aSource code

: R) :
  limit_point E a <-> (forall

USource code

, 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 (

arSource code

: 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 := {

arSource code

: R * R | elt_prop ar}.
pose a_ (

xSource code

: elt_type) := (proj1_sig x).2.
pose r_ (

xSource code

: elt_type) := (proj1_sig x).1.
(* two successive (a_i, r_i) and (a_j, r_j) satisfy the relation: *)
pose elt_rel

iSource code

jSource code

:= `|a - r_ i| = a_ j /\ ball a (a_ j) `<=` ball a (a_ i) /\
  `|a - r_ j| < `|a - r_ i| /\ r_ i != r_ 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

a0Source code

, [/\ 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]] : {

vSource code

: nat -> elt_type |
    v 0 = exist _ (a0, r0) (And5 ar0V a0E a0V0 r0_gt0 a0a) /\
    forall

nSource code

, 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 /a_ /r_/=.
    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 (r_ \o v).
  move=> n _; rewrite /r_ /=.
  by case: (v n) => -[ai ri] [/= ariV /set_mem Eai /set_mem/ariV aiari _ _].
have arv q p : (p < q)%N -> `|a - r_ (v q)| < `|a - r_ (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

limit_point_setDUsed by

• mathcomp.analysis.sequences

---

Source code

{

RSource code

: archiRealFieldType} (

ASource code

VSource code

: set R)

aSource code

:
  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

EFin_limUsed by

• mathcomp.analysis.esum
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence
• mathcomp.analysis.probability_theory.poisson_distribution

---

Source code

 (

RSource code

: realFieldType) (

fSource code

: 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 {

ISource code

} {

FSource code

: set_system I} {

FFSource code

: ProperFilter F} {

RSource code

: realFieldType}.
Implicit Types (f g : I -> \bar R) (u v : I -> R) (x : \bar R) (r : R).
Local Open Scope ereal_scope.

Lemma

is_cvgeDSource code

fSource code

gSource code

:
  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

limeDUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.measure_theory.measure_extension
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
• mathcomp.analysis.realfun

---

Source code

fSource code

gSource code

:
  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

limeMlUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition
• mathcomp.analysis.probability_theory.uniform_distribution

---

Source code

fSource code

ySource code

: y \is a fin_num -> cvg (f @ F) ->
  lim ((fun

nSource code

=> y * f n) @ F) = y * lim (f @ F).

Proof.

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

Lemma

limeMrSource code

fSource code

ySource code

: y \is a fin_num -> cvg (f @ F) ->
  lim ((fun

nSource code

=> f n * y) @ F) = lim (f @ F) * y.

Proof.

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

Lemma

is_cvgeMSource code

fSource code

gSource code

:
  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

limeMSource code

fSource code

gSource code

:
  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

limeNUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.realfun

---

Source code

fSource code

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

Proof.

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

Lemma

cvge_geSource code

fSource code

aSource code

bSource code

: (\forall

xSource code

\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

cvge_leSource code

fSource code

aSource code

bSource code

: (\forall

xSource code

\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

cvg_nnesumUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition

---

Source code

 (

JSource code

: Type) (

rSource code

: seq J) (

fSource code

: J -> I -> \bar R)
   (

lSource code

: J -> \bar R) (

PSource code

: pred J) :
  (forall

jSource code

, P j -> \near

FSource code

, 0 <= f j F) ->
  (forall

jSource code

, P j -> f j @ F --> l j) ->
  \sum_(

jSource code

<- r | P j) f j i @[

iSource code

--> F] --> \sum_(

jSource code

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

lim_nnesumSource code

 (

JSource code

: Type) (

rSource code

: seq J) (

fSource code

: J -> I -> \bar R)
   (

lSource code

: J -> \bar R) (

PSource code

: pred J) :
  (forall

jSource code

, P j -> \near

FSource code

, 0 <= f j F) ->
  (forall

jSource code

, P j -> cvg (f j @ F)) ->
  lim (\sum_(

jSource code

<- r | P j) f j i @[

iSource code

--> F]) = \sum_(

jSource code

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

RSource code

: realFieldType} {

ISource code

: Type} {

aSource code

: set_system I} {

FFSource code

: Filter a}.
Implicit Types f : I -> R.

Lemma

gtr0_cvgV0Used by

• mathcomp.analysis.charge
• mathcomp.analysis.probability_theory.random_variable

---

Source code

fSource code

: (\near

aSource code

, 0 < f a) -> f\^-1 @ a --> 0 <-> f @ a --> +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//=; last 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

cvgrVySource code

fSource code

: (\near

aSource code

, 0 < f a) -> f\^-1 @ a --> +oo <-> f @ a --> 0.

Proof.

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

Lemma

ltr0_cvgV0Source code

fSource code

: (\near

aSource code

, 0 > f a) -> f\^-1 @ a --> 0 <-> f @ a --> -oo.

Proof.

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

Lemma

cvgrVNySource code

fSource code

: (\near

aSource code

, 0 > f a) -> f\^-1 @ a --> -oo <-> f @ a --> 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 {

TSource code

: Type} {

aSource code

: set_system T} {

FaSource code

: Filter a} {

RSource code

: realFieldType}.
Implicit Types f g h : T -> R.

Lemma

squeeze_cvgrUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.gauss_integral
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under

---

Source code

fSource code

hSource code

gSource code

: (\near

aSource code

, f a <= g a <= h a) ->
  forall (

lSource code

: R), f @ a --> l -> h @ a --> l -> g @ a --> l.

Proof.

move=> fgh l lfa lga; apply/cvgrPdist_lt => e e_gt0.
near=> x; have /(_ _)/andP[//|fg gh] := near fgh x.
rewrite distrC ltr_distl (lt_le_trans _ fg) ?(le_lt_trans gh)//=.
  by near: x; apply: (cvgr_lt l); rewrite // ltrDl.
by near: x; apply: (cvgr_gt l); rewrite // gtrDl oppr_lt0.
Unshelve. all: end_near. Qed.

Lemma

ger_cvgySource code

fSource code

gSource code

: (\near

aSource code

, f a <= g a) ->
  f @ a --> +oo -> g @ a --> +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

ler_cvgNySource code

fSource code

gSource code

: (\near

aSource code

, f a >= g a) ->
  f @ a --> -oo -> g @ a --> -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 {

TSource code

: topologicalType} {

aSource code

: set_system T} {

FaSource code

: ProperFilter a}.
Context {

RSource code

: realFieldType}.
Implicit Types f g h : T -> R.

Lemma

ler_cvg_toSource code

fSource code

gSource code

 (

lSource code

l'Source code

: R) : f @ a --> l -> g @ a --> l' ->
  (\near

aSource code

, 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

ler_limUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.exp

---

Source code

fSource code

gSource code

: cvg (f @ a) -> cvg (g @ a) ->
  (\near

aSource code

, f a <= g a) -> lim (f @ a) <= lim (g @ a).

Proof.

exact: ler_cvg_to. Qed.

End TopoProperFilterRealType.

Section FilterERealType.
Context {

TSource code

: Type} {

aSource code

: set_system T} {

FaSource code

: Filter a} {

RSource code

: realFieldType}.
Local Open Scope ereal_scope.
Implicit Types f g h : T -> \bar R.

Lemma

gee_cvgySource code

fSource code

gSource code

: (\near

aSource code

, f a <= g a) ->
  f @ a --> +oo -> g @ a --> +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

lee_cvgNySource code

fSource code

gSource code

: (\near

aSource code

, f a >= g a) ->
  f @ a --> -oo -> g @ a --> -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

squeeze_finSource code

fSource code

gSource code

hSource code

: (\near

aSource code

, f a <= g a <= h a) ->
    (\near

aSource code

, f a \is a fin_num) -> (\near

aSource code

, h a \is a fin_num) ->
  (\near

aSource code

, 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

squeeze_cvgeUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.charge
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation

---

Source code

fSource code

gSource code

hSource code

: (\near

aSource code

, f a <= g a <= h a) ->
  forall (

lSource code

: \bar R), f @ a --> l -> h @ a --> l -> g @ a --> 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.

Section TopoProperFilterERealType.
Context {

TSource code

: topologicalType} {

aSource code

: set_system T} {

FaSource code

: ProperFilter a}.
Context {

RSource code

: realFieldType}.
Local Open Scope ereal_scope.
Implicit Types f g h : T -> \bar R.

Lemma

lee_cvg_toSource code

fSource code

gSource code

lSource code

l'Source code

: f @ a --> l -> g @ a --> l' ->
  (\near

aSource code

, 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

lee_limUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.charge
• mathcomp.analysis.measure_theory.measure_function
• mathcomp.analysis.measure_theory.measure_extension
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition
• mathcomp.analysis.realfun

---

Source code

fSource code

gSource code

: cvg (f @ a) -> cvg (g @ a) ->
  (\near

aSource code

, f a <= g a) -> lim (f @ a) <= lim (g @ a).

Proof.

exact: lee_cvg_to. Qed.

End TopoProperFilterERealType.

Section Rhull.
Variable

RSource code

: realType.

Definition

Rhull

Rhull : forall [R : realType], set R -> interval R Rhull is not universe polymorphic Arguments Rhull [R] X%classical_set_scope Rhull is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.Rhull Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 1320, characters 11-16

---

Used by

• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.lebesgue_measure

---

Source code

 (

XSource code

: 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

Rhull0Used by

• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.lebesgue_measure

---

Source code

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

Proof.

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

Lemma

sub_RhullUsed by

• mathcomp.analysis.lebesgue_measure

---

Source code

 (

XSource code

: set R) : X `<=` [set

xSource code

| 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

is_intervalPUsed by

• mathcomp.analysis.measurable_realfun

---

Source code

 (

XSource code

: set R) : is_interval X <-> X = [set

xSource code

| 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

connected_intervalPSource code

 (

ESource code

: 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

xSource code

| x < z]; pose Bz := E `&` [set

xSource code

| z < x].
  apply/connectedPn : cE; exists (fun

bSource code

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

zSource code

| x <= z <= y]).
  have A1z : ~ (A true) z.
    have cA0z : closure (A false) z.
      suff : closure (A false `&` [set

zSource code

| 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[]|].
    + rewrite lt_neqAle ge_sup ?andbT; last by move=> u [_] /andP[].
      * by apply/negP; apply: contraPnot A1y => /eqP <-.
      * by exists x; split => //; rewrite /mkset /= lexx /= (ltW xy).
    + by split=> //; rewrite /mkset lexx (ltW xy).
  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

z1Source code

: 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] : {

rSource code

:{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

set_itvKUsed by

• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.lebesgue_measure

---

Source code

: {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

RhullTUsed by

• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.lebesgue_measure

---

Source code

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

Proof.

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

Lemma

RhullKSource code

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

Proof.

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

Lemma

set_itv_setTSource code

 (

iSource code

: 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

Rhull_smallestSource code

ASource code

: [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

le_RhullUsed by

• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.lebesgue_measure

---

Source code

: {homo Rhull :

ASource code

BSource code

/ (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_RhullSource code

ASource code

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

Proof.

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

Lemma

Rhull_involutiveUsed by

• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.lebesgue_measure

---

Source code

ASource code

: 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

disj_itv_RhullSource code

 (

ASource code

BSource code

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

Section segment.
Context {

RSource code

: realType}.

Lemma

segment_connectedSource code

 (

aSource code

bSource code

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

Proof.

exact/connected_intervalP/interval_is_interval. Qed.

Lemma

segment_compactUsed by

• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.pi_irrational
• mathcomp.analysis.lebesgue_measure
• mathcomp.analysis.ftc
• mathcomp.analysis.derive
• mathcomp.analysis.gauss_integral
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.probability_theory.beta_distribution
• mathcomp.analysis.normedtype_theory.matrix_normedtype

---

Source code

 (

aSource code

bSource code

: 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

xSource code

| exists2

ESource code

: {fset I}, {subset E <= D} &
  `[a, x] `<=` \bigcup_(

iSource code

in [set` E]) f i /\ (\bigcup_(

iSource code

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.
    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.
  by rewrite subr_ge0; apply/ltW.
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; last by rewrite subr_ge0 (itvP axz).
rewrite ltrBlDl -ltrBlDr; apply: lt_trans ltyz.
by apply: ltr_distlCBl; rewrite distrC.
Qed.

End segment.

Lemma

IVTUsed by

• mathcomp.analysis.trigo
• mathcomp.analysis.exp
• mathcomp.analysis.realfun

---

Source code

 (

RSource code

: realType) (

fSource code

: R -> R) (

aSource code

bSource code

vSource code

: R) :
  a <= b -> {within `[a, b], continuous f} ->
  minr (f a) (f b) <= v <= maxr (f a) (f b) ->
  exists2

cSource code

, c \in `[a, b] & f c = v.

Proof.

move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b ->
    exists2

cSource code

, 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_NormedModule.
Context {

KSource code

: numFieldType} {

USource code

VSource code

: normedModType K}.

Lemma

prod_norm_scaleSource code

 (

lSource code

: K) (

xSource code

: U * V) : `| l *: x | = `|l| * `| x |.

Proof.

by rewrite prod_normE /= !normrZ maxr_pMr. Qed.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

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

End prod_NormedModule.

Section prod_NormedModule_lemmas.
Context {

TSource code

: Type} {

KSource code

: numDomainType} {

USource code

VSource code

: normedModType K}.

Lemma

fcvgr2dist_ltPSource code

{

FSource code

: set_system U} {

GSource code

: set_system V}
  {

FFSource code

: Filter F} {

FGSource code

: Filter G} (

ySource code

: U) (

zSource code

: V) :
  (F, G) --> (y, z) <->
  forall

epsSource code

, 0 < eps ->
   \forall

y'Source code

\near F &

z'Source code

\near G, `| (y, z) - (y', z') | < eps.

Proof.

exact: fcvgrPdist_lt. Qed.

Lemma

cvgr2dist_ltPSource code

{

ISource code

JSource code

} {

FSource code

: set_system I} {

GSource code

: set_system J}
  {

FFSource code

: Filter F} {

FGSource code

: Filter G} (

fSource code

: I -> U) (

gSource code

: J -> V) (

ySource code

: U) (

zSource code

: V) :
  (f @ F, g @ G) --> (y, z) <->
  forall

epsSource code

, 0 < eps ->
   \forall

iSource code

\near F &

jSource code

\near G, `| (y, z) - (f i, g j) | < eps.

Proof.

rewrite fcvgr2dist_ltP; split=> + e e0 => /(_ e e0);
  by rewrite !near_simpl// => ?; rewrite !near_simpl.
Qed.

Lemma

cvgr2dist_ltSource code

{

ISource code

JSource code

} {

FSource code

: set_system I} {

GSource code

: set_system J}
  {

FFSource code

: Filter F} {

FGSource code

: Filter G} (

fSource code

: I -> U) (

gSource code

: J -> V) (

ySource code

: U) (

zSource code

: V) :
  (f @ F, g @ G) --> (y, z) ->
  forall

epsSource code

, 0 < eps ->
   \forall

iSource code

\near F &

jSource code

\near G, `| (y, z) - (f i, g j) | < eps.

Proof.

by rewrite cvgr2dist_ltP. Qed.

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









Lemma

bounded_locallySource code

 (

TSource code

: topologicalType)
    (

RSource code

: numFieldType) (

VSource code

: normedModType R) (

ASource code

: set T) (

fSource code

: T -> V) :
  [bounded f x |

xSource code

in A] -> [locally [bounded f x |

xSource code

in A]].

Proof.

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

Notation 

"k .-lipschitz_on f"Source code

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

Lemma

sub_klipschitzSource code

 (

KSource code

: numFieldType) (

VSource code

WSource code

: normedModType K) (

kSource code

: K)
    (

fSource code

: V -> W) (

FSource code

GSource code

: set_system (V * V)) :
  F `=>` G -> k.-lipschitz_on f G -> k.-lipschitz_on f F.

Proof.

exact. Qed.

Definition

lipschitz_on

lipschitz_on : forall [K : numFieldType] [V W : normedModType K], (V -> W) -> set_system (V * V) -> Prop lipschitz_on is not universe polymorphic Arguments lipschitz_on [K V W] f%function_scope F lipschitz_on is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.lipschitz_on Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 1833, characters 11-23

---

Source code

 (

KSource code

: numFieldType) (

VSource code

WSource code

: normedModType K)
           (

fSource code

: V -> W) (

FSource code

: set_system (V * V)) :=
  \forall

MSource code

\near +oo, M.-lipschitz_on f F.

Lemma

sub_lipschitzSource code

 (

KSource code

: numFieldType) (

VSource code

WSource code

: normedModType K)
    (

fSource code

: V -> W) (

FSource code

GSource code

: 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

klipschitzWSource code

 (

KSource code

: numFieldType) (

VSource code

WSource code

: normedModType K) (

kSource code

: K)
      (

fSource code

: V -> W) (

FSource code

: set_system (V * V)) {

PFSource code

: 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_ A f"Source code

:=
  (k.-lipschitz_on f (globally (A `*` A))) : type_scope.
Notation 

"k .-lipschitz f"Source code

:= (k.-lipschitz_setT f) : type_scope.
Notation 

"[ 'lipschitz' E | x 'in' A ]"Source code

:=
  (lipschitz_on (fun

xSource code

=> E) (globally (A `*` A))) : type_scope.
Notation

lipschitzSource code

f := [lipschitz f x |

xSource code

in setT].

Lemma

lipschitz_set0Source code

 (

KSource code

: numFieldType) (

VSource code

WSource code

: normedModType K)
  (

fSource code

: V -> W) : [lipschitz f x |

xSource code

in set0].

Proof.

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

Lemma

lipschitz_set1Source code

 (

KSource code

: numFieldType) (

VSource code

WSource code

: normedModType K)
  (

fSource code

: V -> W) (

aSource code

: V) : [lipschitz f x |

xSource code

in [set a]].

Proof.

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

Lemma

klipschitz_locallySource code

 (

RSource code

: numFieldType) (

VSource code

WSource code

: normedModType R) (

kSource code

: R)
    (

fSource code

: V -> W) (

ASource code

: set V) :
  k.-lipschitz_A f -> [locally k.-lipschitz_A f].

Proof.

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

Lemma

lipschitz_locallySource code

 (

RSource code

: numFieldType) (

VSource code

WSource code

: normedModType R)
    (

ASource code

: set V) (

fSource code

: V -> W) :
  [lipschitz f x |

xSource code

in A] -> [locally [lipschitz f x |

xSource code

in A]].

Proof.

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

Lemma

lipschitz_idSource code

 (

RSource code

: numFieldType) (

VSource code

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

Proof.

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

Arguments lipschitz_id {R V}.

Section LinearContinuousBounded.
Variables (

RSource code

: numFieldType) (

VSource code

WSource code

: normedModType R).

Lemma

linear_boundedPSource code

 (

fSource code

: {linear V -> W}) : bounded_near f (nbhs 0) <->
  \forall

rSource code

\near +oo, forall

xSource code

, `|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

continuous_linear_boundedSource code

 (

xSource code

: V) (

fSource code

: {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

bounded_linear_continuousSource code

 (

fSource code

: {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

continuousfor0_continuousSource code

 (

fSource code

: {linear V -> W}) :
  {for 0, continuous f} -> continuous f.

Proof.

by move=> /continuous_linear_bounded/bounded_linear_continuous. Qed.

Lemma

linear_bounded_continuousSource code

 (

fSource code

: {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

bounded_funPUsed by

• mathcomp.analysis.sequences

---

Source code

 (

fSource code

: {linear V -> W}) :
  (forall

rSource code

, exists

MSource code

, forall

xSource code

, `|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 {

RSource code

: numDomainType} {

XSource code

YSource code

: normedModType R} {

USource code

: set X} {

VSource code

: set Y}.

Definition

contraction

contraction : forall {R : numDomainType} {X Y : normedModType R} {U : set X} {V : set Y}, {nonneg R}%R -> {fun U >-> V} -> Prop contraction is not universe polymorphic Arguments contraction {R X Y} {U V}%classical_set_scope q f contraction is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.contraction Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 1947, characters 11-22

---

Used by

• mathcomp.analysis.sequences

---

Source code

 (

qSource code

: {nonneg R}) (

fSource code

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

Definition

is_contraction

is_contraction : forall {R : numDomainType} {X Y : normedModType R} {U : set X} {V : set Y}, {fun U >-> V} -> Prop is_contraction is not universe polymorphic Arguments is_contraction {R X Y} {U V}%classical_set_scope f is_contraction is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.is_contraction Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 1950, characters 11-25

---

Used by

• mathcomp.analysis.sequences

---

Source code

 (

fSource code

: {fun U >-> V}) := exists

qSource code

, contraction q f.

End contractions.

Lemma

contraction_fixpoint_uniqueSource code

{

RSource code

: realDomainType}
    {

XSource code

: normedModType R} (

USource code

: set X) (

fSource code

: {fun U >-> U}) (

xSource code

ySource code

: X) :
  is_contraction f -> U x -> U y -> x = f x -> y = f y -> x = y.

Proof.

case => q [q1 ctrfq] Ux Uy fixx fixy; apply/subr0_eq/normr0_eq0/eqP.
have [->|xyneq] := eqVneq x y; first by rewrite subrr normr0.
have xypos : 0 < `|x - y| by rewrite normr_gt0 subr_eq0.
suff : `|x - y| <= q%:num * `|x - y| by rewrite ler_pMl // leNgt q1.
by rewrite [in leLHS]fixx [in leLHS]fixy; exact: (ctrfq (_, _)).
Qed.

Section cvg_seq_bounded.
Context {

KSource code

: numFieldType}.
Local Notation 

"'+oo'"Source code

:= (@pinfty_nbhs K).

Lemma

cvg_seq_boundedUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.measurable_realfun

---

Source code

{

VSource code

: normedModType K} (

aSource code

: 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

nSource code

: '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

compact_boundedUsed by

• mathcomp.analysis.lebesgue_measure
• mathcomp.analysis.derive
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation

---

Source code

 (

KSource code

: realType) (

VSource code

: normedModType K) (

ASource code

: set V) :
  compact A -> bounded_set A.

Proof.

rewrite compact_cover => Aco.
have covA : A `<=` \bigcup_(

nSource code

: int) [set

pSource code

| `|p| < n%:~R].
  by move=> p _; exists (truncn `|p|).+1; rewrite //= truncnS_gt.
have /Aco [] := covA.
  move=> n _; rewrite openE => p; rewrite /= -subr_gt0 => ltpn.
  apply/nbhs_ballP; exists (n%:~R - `|p|) => // q.
  rewrite -ball_normE /= ltrBrDr distrC; apply: le_lt_trans.
  by rewrite -{1}(subrK p q) ler_normD.
move=> D _ DcovA.
exists (\big[maxr/0]_(

iSource code

: D) (fsval i)%:~R).
rewrite bigmax_real//; split=> // x ltmaxx p /DcovA [n Dn /lt_trans /(_ _)/ltW].
apply; apply: le_lt_trans ltmaxx.
have : n \in enum_fset D by [].
by rewrite enum_fsetE => /mapP[/= i iD ->]; exact/le_bigmax.
Qed.

Lemma

compact_has_supUsed by

• mathcomp.analysis.derive

---

Source code

 (

RSource code

: realType) (

ASource code

: 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

closed_closed_ball_Source code

 (

RSource code

: realFieldType) (

VSource code

: normedModType R)
  (

xSource code

: V) (

eSource code

: R) : closed (closed_ball_ normr x e).

Proof.

rewrite /closed_ball_ -/((normr \o (fun

ySource code

=> x - y)) @^-1` [set

xSource code

| x <= e]).
apply: (preimage_closed _ (@closed_le _ _)) => y _.
apply: (continuous_comp _ (@norm_continuous _ _ _)).
exact: (continuousB (@cst_continuous _ _ _ _)).
Qed.

Lemma

closed_ballEUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_measure
• mathcomp.analysis.normedtype_theory.vitali_lemma

---

Source code

 (

RSource code

: realFieldType) (

VSource code

: normedModType R) (

xSource code

: V)
  (

rSource code

: 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; first 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

closed_ball_itvUsed by

• mathcomp.analysis.pi_irrational
• mathcomp.analysis.lebesgue_measure
• mathcomp.analysis.measurable_realfun

---

Source code

 (

RSource code

: realFieldType) (

xSource code

rSource code

: 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

closed_ball_ballUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg

---

Source code

{

RSource code

: realFieldType} (

xSource code

rSource code

: 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 setUAC setUC ball_itv.
by rewrite lerD2l ge0_cp// ltW.
Qed.

Lemma

closed_ballR_compactUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation

---

Source code

 (

RSource code

: realType) (

xSource code

eSource code

: 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

closed_ball_subsetSource code

 (

RSource code

: realFieldType) (

MSource code

: normedModType R) (

xSource code

: M)
  (

r0Source code

r1Source code

: 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

nbhs_closedballPUsed by

• mathcomp.analysis.sequences

---

Source code

 (

RSource code

: realFieldType) (

MSource code

: normedModType R) (

BSource code

: set M)
  (

xSource code

: M) : nbhs x B <-> exists

rSource code

: {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

open_subballUsed by

• mathcomp.analysis.lebesgue_measure
• mathcomp.analysis.derive
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation

---

Source code

{

RSource code

: numFieldType} {

MSource code

: normedModType R} (

ASource code

: set M)
  (

xSource code

: M) : open A -> A x -> \forall

eSource code

\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

open_subball_ratSource code

{

RSource code

: realType} (

SSource code

: set R)

xSource code

: open S -> x \in S ->
  exists

cSource code

rSource code

, let

BSource code

: 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

ySource code

, 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

qSource code

, 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 {

RSource code

: realType}.
Variable

SSource code

: set R.

Fact

isolated_rat_ballSource code

 (

xSource code

: R) : isolated S x -> exists

crSource code

,
  let

BSource code

: set R := ball (@ratr R cr.1) (ratr cr.2) in
  x \in B /\ (forall

ySource code

: R, isolated S y -> y \in B -> x = y).

Proof.

move=> Sx.
have [e Sxe] : exists

eSource code

: {posnum R},
    forall

ySource code

: 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

eSource code

\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

cSource code

rSource code

,
  let

BSource code

: 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_isolatedSource code

: countable (isolated S).

Proof.

apply/pcard_injP => /=.
pose g

rSource code

:= 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

xSource code

=> \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

closed_disjoint_closed_ballUsed by

• mathcomp.analysis.lebesgue_measure

---

Source code

{

RSource code

: realFieldType} {

MSource code

: normedModType R}
    (

KSource code

: set M)

zSource code

: closed K -> ~ K z ->
  \forall

dSource code

\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

interior_closed_ballESource code

 (

RSource code

: realType) (

VSource code

: normedModType R) (

xSource code

: V)
  (

rSource code

: R) : 0 < r -> (closed_ball x r)° = ball x r.

Proof.

move=> r0; rewrite eqEsubset; split; last first.
  by rewrite -open_subsetE; [exact: subset_closure | exact: ball_open].
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; last 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

open_nbhs_closed_ballUsed by

• mathcomp.analysis.sequences

---

Source code

 (

RSource code

: realType) (

VSource code

: normedModType R) (

xSource code

: V)
  (

rSource code

: 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

locally_compactRSource code

 (

RSource code

: 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 {

RSource code

: realType} {

USource code

: set R}.

Lemma

bigcup_ointsubxxSource code

qSource code

: 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

nondisjoint_bigcup_ointsubSource code

 (

pSource code

qSource code

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

Module

OpenSetDisjointItvsSource code

.
Section opensetdisjointitvs.
Context {

RSource code

: realType}.
Variable

USource code

: set R.
Hypothesis

oUSource code

: open U.

Section rat_index.
Variables (

fSource code

: rat -> nat) (

gSource code

: nat -> rat).
Hypotheses (

cfgSource code

: cancel f g) (

cgfSource code

: cancel g f).

Definition

lt_disjoint

OpenSetDisjointItvs.lt_disjoint : forall {R : realType}, set R -> (rat -> nat) -> set rat OpenSetDisjointItvs.lt_disjoint is not universe polymorphic Arguments OpenSetDisjointItvs.lt_disjoint {R} U%classical_set_scope f%function_scope _ OpenSetDisjointItvs.lt_disjoint is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.OpenSetDisjointItvs.lt_disjoint Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 2278, characters 11-22

---

Source code

:= [set

qSource code

| forall

pSource code

, U (ratr p) ->
  (f p < f q)%N -> bigcup_ointsub U q `&` bigcup_ointsub U p = set0].

Let

bigcup_lt_disjointSource code

:
  U = \bigcup_(

qSource code

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

p_idxSource code

,
    let

pSource code

:= g p_idx in ratr p \in bigcup_ointsub U q /\
    forall

q'Source code

, 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

iSource code

: '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_(

iSource code

< 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

lt_disjoint_rat_seq0Source code

qSource code

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

Let

lt_disjoint_rat_seq0_trivIsetSource code

: 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

lt_disjoint_rat_seq0_comp_trivIsetSource code

:
  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

lt_disjoint_rat_seq0_set0Source code

qSource code

:
  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

lt_disjoint_rat_seq0_open_itvSource code

qSource code

:
  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

bigcup_lt_disjoint_rat_seq0Source code

: U = \bigcup_

qSource code

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

bigcup_U_lt_disjoint_rat_seqSource code

:
  U = \bigcup_(

qSource code

in [set

nSource code

| 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

lt_disjoint_rat_seq

OpenSetDisjointItvs.lt_disjoint_rat_seq : forall {R : realType}, set R -> (rat -> nat) -> rat -> set R OpenSetDisjointItvs.lt_disjoint_rat_seq is not universe polymorphic Arguments OpenSetDisjointItvs.lt_disjoint_rat_seq {R} U%classical_set_scope f%function_scope q%ring_scope _ OpenSetDisjointItvs.lt_disjoint_rat_seq is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.OpenSetDisjointItvs.lt_disjoint_rat_seq Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 2382, characters 11-30

---

Source code

qSource code

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

Lemma

lt_disjoint_rat_seq_open_itvSource code

qSource code

:
  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

lt_disjoint_rat_seq_trivIsetSource code

: 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

bigcup_lt_disjoint_rat_seqSource code

: U = \bigcup_

qSource code

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.

Lemma

open_disjoint_itvSource code

: exists

ISource code

: nat -> set R,
  [/\ forall

qSource code

, open (I q) /\ is_interval (I q),
      trivIset setT I & U = \bigcup_

qSource code

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 {

RSource code

: realType}.
Variable

USource code

: set R.
Hypothesis

oUSource code

: open U.

Definition

open_disjoint_itv

open_disjoint_itv : forall {R : realType} [U : set R], open U -> nat -> set R open_disjoint_itv is not universe polymorphic Arguments open_disjoint_itv {R} [U]%classical_set_scope oU _%nat_scope _ open_disjoint_itv is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.normed_module.open_disjoint_itv Declared in library mathcomp.analysis.normedtype_theory.normed_module, line 2441, characters 11-28

---

Source code

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

Lemma

open_disjoint_itv_openSource code

iSource code

: open (open_disjoint_itv i).

Proof.

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

Lemma

open_disjoint_itv_is_intervalSource code

iSource code

: is_interval (open_disjoint_itv i).

Proof.

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

Lemma

open_disjoint_itv_trivIsetSource code

: trivIset [set: nat] open_disjoint_itv.

Proof.

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

Lemma

open_disjoint_itv_bigcupSource code

: U = \bigcup_

qSource code

open_disjoint_itv q.

Proof.

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

End open_set_disjoint_real_intervals.