Module mathcomp.analysis.normedtype_theory.num_normedtype

From mathcomp Require Import boot order finmap ssralg ssrnum ssrint.
From mathcomp Require Import interval interval_inference archimedean rat.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import cardinality set_interval reals real_interval.
From mathcomp Require Import topology prodnormedzmodule.

# Preliminaries for norm-related notions This file contains various definitions and lemmas about topological notions of numeric types that are useful to develop the theory of normed modules in this directory. ``` pinfty_nbhs == filter for +oo (for a numFieldType) Notation: +oo (ring_scope) ninfty_nbhs == filter for -oo (for a numFieldType) Notation: -oo (ring_scope) is_interval E == the set E is an interval bigcup_ointsub U q == union of open real intervals included in U and that contain the rational number q ``` ``` f @`[ a , b ], f @`] a , b [ == notations for images of intervals, intended for continuous, monotonous functions, defined in ring_scope and classical_set_scope respectively as: f @`[ a , b ] := `[minr (f a) (f b), maxr (f a) (f b)]%O f @`] a , b [ := `]minr (f a) (f b), maxr (f a) (f b)[%O f @`[ a , b ] := `[minr (f a) (f b), maxr (f a) (f b)]%classic f @`] a , b [ := `]minr (f a) (f b), maxr (f a) (f b)[%classic ```

Reserved Notation "f @`[ a , b ]" (format "f @`[ a , b ]").
Reserved Notation "f @`] a , b [" (format "f @`] a , b [").
Reserved Notation "+oo_ R" (at level 3, left associativity, format "+oo_ R").
Reserved Notation "-oo_ R" (at level 3, left associativity, format "-oo_ R").

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

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

Proof.

by rewrite !(boundr_in_itv, boundl_in_itv). Qed.

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

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

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

Proof.

move=> [fle|fge] x xab; have leab : a <= b by rewrite (itvP xab).
have: f a <= f b by rewrite fle ?bound_itvE.
by case: leP => // fafb _; rewrite in_itv/= !fle ?(itvP xab).
have: f a >= f b by rewrite fge ?bound_itvE.
by case: leP => // fafb _; rewrite in_itv/= !fge ?(itvP xab).
Qed.

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

Proof.

move=> []/[dup] => [/le_mono_in|/le_nmono_in] flt fle x xab;
    have ltab : a < b by rewrite (itvP xab).
  have: f a <= f b by rewrite flt ?bound_itvE ltW.
  by case: leP => // fafb _; rewrite in_itv/= !fle ?in_itv/= ?(itvP xab, lexx).
have: f a >= f b by rewrite flt ?bound_itvE ?ltW.
by case: leP => // fafb _; rewrite in_itv/= !fle ?in_itv/= ?(itvP xab, lexx).
Qed.

Lemma : a <= b ->
monotonic `[a, b] f -> set_surj `[a, b] (f @`[a, b]) f ->
(f @` `[a, b] = f @`[a, b])%classic.

Proof.

move=> leab fmono; apply: surj_image_eq => _ /= [x xab <-].
exact: mono_mem_image_segment.
Qed.

Lemma : f a <= f b -> f @`[a, b] = `[f a, f b].

Proof.

by case: ltrP. Qed.

Lemma : f b <= f a -> f @`[a, b] = `[f b, f a].

Proof.

by case: ltrP. Qed.

Lemma : a <= b ->
    {in `[a, b] &, {homo f : / x <= y}} ->
    set_surj `[a, b] `[f a, f b] f ->
  f @` `[a, b] = `[f a, f b]%classic.

Proof.

move=> leab fle f_surj; have fafb : f a <= f b by rewrite fle ?bound_itvE.
by rewrite mono_surj_image_segment ?inc_segment_image//; left.
Qed.

Lemma : a <= b ->
    {in `[a, b] &, {homo f : /~ x <= y}} ->
    set_surj `[a, b] `[f b, f a] f ->
  f @` `[a, b] = `[f b, f a]%classic.

Proof.

move=> leab fge f_surj; have fafb : f b <= f a by rewrite fge ?bound_itvE.
by rewrite mono_surj_image_segment ?dec_segment_image//; right.
Qed.

Lemma : a <= b ->
    {in `[a, b] &, {homo f : / x <= y}} ->
    set_surj `[a, b] `[f a, f b] f ->
  forall , reflect (exists2 , x \in `[a, b] & f x = y) (y \in `[f a, f b]).

Proof.

move=> /inc_surj_image_segment/[apply]/[apply]/predeqP + y => /(_ y) fab.
by apply/(equivP idP); symmetry.
Qed.

Lemma : a <= b ->
    {in `[a, b] &, {homo f : /~ x <= y}} ->
    set_surj `[a, b] `[f b, f a] f ->
  forall , reflect (exists2 , x \in `[a, b] & f x = y) (y \in `[f b, f a]).

Proof.

move=> /dec_surj_image_segment/[apply]/[apply]/predeqP + y => /(_ y) fab.
by apply/(equivP idP); symmetry.
Qed.

Lemma : a <= b ->
monotonic `[a, b] f -> set_surj `[a, b] (f @`[a, b]) f ->
forall , reflect (exists2 , x \in `[a, b] & f x = y) (y \in f @`[a, b]).

Proof.

move=> /mono_surj_image_segment/[apply]/[apply]/predeqP + y => /(_ y) fab.
by apply/(equivP idP); symmetry.
Qed.

End image_interval.

Lemma { : realType} : \bigcup_ ball (0%R : R) n%:R = setT.

Proof.

rewrite -[RHS](bigcup_itvT false true); apply: eq_bigcup => //= n _.
by apply/seteqP; split=> [?|?]; rewrite /ball/= sub0r normrN in_itv/= ltr_norml.
Qed.

Section nbhs_pseudoMetricType.
Context { : numDomainType} { : pseudoMetricType R}.

Lemma ( : T) ( : set T) :
~ (forall : {posnum R}, ~ (ball x eps%:num `<=` ~` P)) ->
{ : {posnum R} | ball x d%:num `<=` ~` P}.

Proof.

rewrite forallNE notK => exNP.
pose D := [set : R^o | d > 0 /\ ball x d `<=` ~` P].
have [|d_gt0] := @getPex _ D; last by exists (PosNum d_gt0).
by move: exNP => [e eP]; exists e%:num.
Qed.

Lemma ( : T) ( : set T) :
~ (forall : {posnum R}, ~ (ball x eps%:num `<=` ~` P)) ->
nbhs x (~` P).

Proof.

by move=> /ex_ball_sig [e] ?; apply/nbhs_ballP; exists e%:num => /=. Qed.

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

Proof.

move=> /nbhs_ballP xNP; apply: ex_ball_sig.
by have [_ /posnumP[e] eP /(_ _ eP)] := xNP.
Qed.

Lemma ( : T) ( : T -> Prop) : nbhs x P ->
{ : {posnum R} | forall , ball x d%:num y -> P y}.

Proof.

move=> /nbhs_ballP xP.
pose D := [set : R^o | d > 0 /\ forall , ball x d y -> P y].
have [|d_gt0 dP] := @getPex _ D; last by exists (PosNum d_gt0).
by move: xP => [e bP]; exists (e : R).
Qed.

End nbhs_pseudoMetricType.

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

Proof.

apply: Build_ProperFilter_ex => A /nbhs_ballP[_/posnumP[e] Ae].
exists (x + e%:num / 2); apply: Ae; last by rewrite addrC -subr_eq0 addrK.
rewrite /ball /= opprD addNKr normrN ger0_norm //.
by rewrite {2}(splitr e%:num) ltr_pwDl.
Qed.

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

Definition ( : numFieldType) : set_system R :=
  fun => exists , M \is Num.real /\ forall , M < x -> P x.
Arguments pinfty_nbhs R : clear implicits.
Definition ( : numFieldType) : set_system R :=
  fun => exists , M \is Num.real /\ forall , x < M -> P x.
Arguments ninfty_nbhs R : clear implicits.

Notation := (pinfty_nbhs R) (only parsing) : ring_scope.
Notation := (ninfty_nbhs R) (only parsing) : ring_scope.

Notation := (pinfty_nbhs _) : ring_scope.
Notation := (ninfty_nbhs _) : ring_scope.

Lemma { : numFieldType} : (- x : R)%R @[ --> -oo] = +oo.

Proof.

apply/seteqP; split => [A [M [Mreal MA]]|A [M [Mreal MA]]].
exists (- M); rewrite realN; split => // x.
by rewrite ltrNl => /MA/=; rewrite opprK.
by exists (- M); rewrite ?realN; split=> // x; rewrite ltrNr => /MA.
Qed.

Lemma { : numFieldType} : (- x : R)%R @[ --> +oo] = -oo.

Proof.

apply/seteqP; split => [A [M [Mreal MA]]|A [M [Mreal MA]]].
exists (- M); rewrite realN; split => // x.
by rewrite -ltrNr => /MA/=; rewrite opprK.
by exists (- M); rewrite ?realN; split=> // x; rewrite ltrNl => /MA.
Qed.

Section infty_nbhs_instances.
Context { : numFieldType}.
Implicit Types r : R.

Global Instance : ProperFilter (pinfty_nbhs R).

Proof.

apply Build_ProperFilter_ex.
by move=> P [M [Mreal MP]]; exists (M + 1); apply MP; rewrite ltrDl.
split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
- by exists 0.
- exists (maxr MP MQ); split=> [|x]; first exact: max_real.
by rewrite comparable_gt_max ?real_comparable // => /andP[/gtMP ? /gtMQ].
- by exists M; split => // ? /gtM /sPQ.
Qed.

Global Instance : ProperFilter (ninfty_nbhs R).

Proof.

apply Build_ProperFilter_ex.
  move=> P [M [Mr ltMP]]; exists (M - 1).
  by apply: ltMP; rewrite gtrDl oppr_lt0.
split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
- by exists 0.
- exists (minr MP MQ); split=> [|x]; first exact: min_real.
  by rewrite comparable_lt_min ?real_comparable // => /andP[/ltMP ? /ltMQ].
- by exists M; split => // x /ltM /sPQ.
Qed.

Lemma : r \is Num.real -> \forall \near +oo, r < x.

Proof.

by exists r. Qed.

Lemma : r \is Num.real -> \forall \near +oo, r <= x.

Proof.

by exists r; split => //; apply: ltW. Qed.

Lemma : r \is Num.real -> \forall \near -oo, r > x.

Proof.

by exists r. Qed.

Lemma : r \is Num.real -> \forall \near -oo, r >= x.

Proof.

by exists r; split => // ?; apply: ltW. Qed.

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

Proof.

by apply: filterS (nbhs_pinfty_gt (@real0 _)); apply: gtr0_real. Qed.

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

Proof.

by apply: filterS (nbhs_ninfty_lt (@real0 _)); apply: ltr0_real. Qed.

Lemma ( : R) ( : set R) : m \is Num.real ->
(\forall \near +oo, A k) -> exists2 , m < M & A M.

Proof.

move=> m_real Agt; near (pinfty_nbhs R) => M.
by exists M; near: M => //; apply: nbhs_pinfty_gt.
Unshelve. all: by end_near. Qed.

Lemma ( : R) ( : set R) : m \is Num.real ->
(\forall \near +oo, A k) -> exists2 , m <= M & A M.

Proof.

move=> m_real Agt; near (pinfty_nbhs R) => M.
by exists M; near: M => //; apply: nbhs_pinfty_ge.
Unshelve. all: by end_near. Qed.

Lemma ( : set R) :
(\forall \near +oo, A k) -> exists2 , M > 0 & A M.

Proof.

exact: pinfty_ex_gt. Qed.

Lemma ( : set R) :
(\forall \near +oo, A k) -> (\forall \near +oo, A (k / 2)).

Proof.

move=> [M [Mreal AM]]; exists (M * 2); split; first by rewrite realM.
by move=> x; rewrite -ltr_pdivlMr //; exact: AM.
Qed.

Lemma ( : pred R) :
~ (\forall \near +oo, P x) <->
forall : R, M \is Num.real -> exists2 , M < x & ~ P x.

Proof.

rewrite nearE -forallNP -propeqE; apply: eq_forall => M.
by rewrite propeqE -implypN existsPNP.
Qed.

Lemma ( : pred R):
~ (\forall \near -oo, P x) <->
forall : R, M \is Num.real -> exists2 , x < M & ~ P x.

Proof.

rewrite -filterN ninftyN not_near_inftyP/=; split => PN M; rewrite -realN;
by move=> /PN[x Mx PNx]; exists (- x) => //; rewrite 1?(ltrNl,ltrNr,opprK).
Qed.

End infty_nbhs_instances.

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

Section cvg_infty_numField.
Context { : numFieldType}.

Let { : set_system R} { : Filter F} : [<->
F --> +oo;
forall , A \is Num.real -> \forall \near F, A <= x;
forall , A \is Num.real -> \forall \near F, A < x;
\forall \near +oo, \forall \near F, A < x;
\forall \near +oo, \forall \near F, A <= x ].

Proof.

tfae; first by move=> Foo A Areal; apply: Foo; apply: nbhs_pinfty_ge.
- move=> AF A Areal; near +oo_R => B.
by near do apply: (@lt_le_trans _ _ B) => //=; apply: AF.
- by move=> Foo; near do apply: Foo => //.
- by apply: filterS => ?; apply: filterS => ?; apply: ltW.
case=> [A [AR AF]] P [x [xR Px]]; near +oo_R => B.
by near do [apply: Px; apply: (@lt_le_trans _ _ B) => //]; apply: AF.
Unshelve. all: by end_near. Qed.

Let { : set_system R} { : Filter F} : [<->
F --> -oo;
forall , A \is Num.real -> \forall \near F, A >= x;
forall , A \is Num.real -> \forall \near F, A > x;
\forall \near -oo, \forall \near F, A > x;
\forall \near -oo, \forall \near F, A >= x ].

Proof.

tfae; first by move=> Foo A Areal; apply: Foo; apply: nbhs_ninfty_le.
- move=> AF A Areal; near -oo_R => B.
by near do apply: (@le_lt_trans _ _ B) => //; apply: AF.
- by move=> Foo; near do apply: Foo => //.
- by apply: filterS => ?; apply: filterS => ?; apply: ltW.
case=> [A [AR AF]] P [x [xR Px]]; near -oo_R => B.
by near do [apply: Px; apply: (@le_lt_trans _ _ B) => //]; apply: AF.
Unshelve. all: end_near. Qed.

Context {} { : set_system T} { : Filter F}.
Implicit Types f : T -> R.

Lemma :
f @ F --> +oo <-> forall , A \is Num.real -> \forall \near F, A <= f x.

Proof.

exact: (cvgryPnum 0%N 1%N). Qed.

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

Proof.

exact: (cvgryPnum 0%N 2%N). Qed.

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

Proof.

exact: (cvgryPnum 0%N 3%N). Qed.

Lemma :
f @ F --> +oo <-> \forall \near +oo, \forall \near F, A <= f x.

Proof.

exact: (cvgryPnum 0%N 4%N). Qed.

Lemma :
f @ F --> -oo <-> forall , A \is Num.real -> \forall \near F, A >= f x.

Proof.

exact: (cvgrNyPnum 0%N 1%N). Qed.

Lemma :
f @ F --> -oo <-> forall , A \is Num.real -> \forall \near F, A > f x.

Proof.

exact: (cvgrNyPnum 0%N 2%N). Qed.

Lemma :
f @ F --> -oo <-> \forall \near -oo, \forall \near F, A > f x.

Proof.

exact: (cvgrNyPnum 0%N 3%N). Qed.

Lemma :
f @ F --> -oo <-> \forall \near -oo, \forall \near F, A >= f x.

Proof.

exact: (cvgrNyPnum 0%N 4%N). Qed.

Lemma :
f @ F --> +oo -> forall , A \is Num.real -> \forall \near F, A <= f x.

Proof.

by rewrite cvgryPger. Qed.

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

Proof.

by rewrite cvgryPgtr. Qed.

Lemma :
f @ F --> -oo -> forall , A \is Num.real -> \forall \near F, A >= f x.

Proof.

by rewrite cvgrNyPler. Qed.

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

Proof.

by rewrite cvgrNyPltr. Qed.

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

Proof.

rewrite cvgrNyPler cvgryPger; split=> Foo A Areal;
by near do rewrite -lerN2 ?opprK; apply: Foo; rewrite rpredN.
Unshelve. all: end_near. Qed.

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

Proof.

by rewrite -cvgNry opprK. Qed.

End cvg_infty_numField.

Section cvg_infty_realField.
Context { : realFieldType}.
Context {} { : set_system T} { : Filter F} ( : T -> R).

Lemma : f @ F --> +oo <-> forall , \forall \near F, A <= f x.

Proof.

by rewrite cvgryPger; under eq_forall do rewrite num_real; split=> + *; apply.
Qed.

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

Proof.

by rewrite cvgryPgtr; under eq_forall do rewrite num_real; split=> + *; apply.
Qed.

Lemma : f @ F --> -oo <-> forall , \forall \near F, A >= f x.

Proof.

by rewrite cvgrNyPler; under eq_forall do rewrite num_real; split=> + *; apply.
Qed.

Lemma : f @ F --> -oo <-> forall , \forall \near F, A > f x.

Proof.

by rewrite cvgrNyPltr; under eq_forall do rewrite num_real; split=> + *; apply.
Qed.

Lemma : f @ F --> +oo -> forall , \forall \near F, A <= f x.

Proof.

by rewrite cvgryPge. Qed.

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

Proof.

by rewrite cvgryPgt. Qed.

Lemma : f @ F --> -oo -> forall , \forall \near F, A >= f x.

Proof.

by rewrite cvgrNyPle. Qed.

Lemma : f @ F --> -oo -> forall , \forall \near F, A > f x.

Proof.

by rewrite cvgrNyPlt. Qed.

End cvg_infty_realField.

Lemma { : realFieldType} : (x ^+ 2 : R) @[ --> +oo] --> +oo.

Proof.

by apply/cvgryPge => M; near=> x; rewrite (@le_trans _ _ x)// expr2 ler_peMl.
Unshelve. all: end_near. Qed.

Lemma { : realType} : (n%:R : R) @[ --> \oo] --> +oo.

Proof.

by apply/cvgryPge => M; exact: nbhs_infty_ger.
Unshelve. all: end_near. Qed.

Lemma { : realType} {} { : set_system T} { : Filter F} ( : T -> nat) :
(((f n)%:R : R) @[ --> F] --> +oo) <-> (f @ F --> \oo).

Proof.

split=> [/cvgryPge|/cvgnyPge] Foo.
by apply/cvgnyPge => A; near do rewrite -(@ler_nat R); apply: Foo.
apply/cvgryPgey; near=> A; near=> n.
rewrite pmulrn -ceil_le_int [ceil _]intEsign.
by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo.
Unshelve. all: by end_near. Qed.

Section gt0_cvg.
Context { : realFieldType} { : set_system R} { : Filter F}.
Variables ( : R) ( : R -> R).
Hypothesis : 0 < M.

Lemma : (f r) @[ --> F] --> -oo -> (f r * M)%R @[ --> F] --> -oo.

Proof.

move=> /cvgrNyPle fy; apply/cvgrNyPle => A.
by apply: filterS (fy (A / M)) => x; rewrite ler_pdivlMr.
Qed.

Lemma : (f r) @[ --> F] --> -oo -> (M * f r)%R @[ --> F] --> -oo.

Proof.

by move=> fy; under eq_fun do rewrite mulrC; exact: gt0_cvgMlNy. Qed.

Lemma : f r @[ --> F] --> +oo -> (f r * M)%R @[ --> F] --> +oo.

Proof.

move=> /cvgryPge fy; apply/cvgryPge => A.
by apply: filterS (fy (A / M)) => x; rewrite ler_pdivrMr.
Qed.

Lemma : f r @[ --> F] --> +oo -> (M * f r)%R @[ --> F] --> +oo.

Proof.

by move=> fy; under eq_fun do rewrite mulrC; exact: gt0_cvgMly. Qed.

End gt0_cvg.

Lemma { : topologicalType} { : numFieldType} ( : R -> T)
( : set_system T) :
f x @[ --> -oo] --> l <-> (f \o -%R) x @[ --> +oo] --> l.

Proof.

have f_opp : f =1 (fun => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
by rewrite (eq_cvg -oo _ f_opp) [in X in X <-> _]fmap_comp ninftyN.
Qed.

Lemma { : topologicalType} { : numFieldType} ( : R -> T)
( : set_system T) :
f x @[ --> +oo] --> l <-> (f \o -%R) x @[ --> -oo] --> l.

Proof.

have f_opp : f =1 (fun => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
by rewrite (eq_cvg +oo _ f_opp) [in X in X <-> _]fmap_comp ninfty.
Qed.

Section monotonic_itv_bigcup.
Context { : realType}.
Implicit Types (F : R -> R) (a : R).

Lemma :
  {in `[a, +oo[ &, {homo F : /~ x < y}} ->
  F x @[ --> +oo] --> -oo ->
  (`]-oo, F a[ = \bigcup_ `]F (a + i.+1%:R), F a[)%classic.

Proof.

move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split.
- move=> y/= [n _]/=; rewrite in_itv/= => /andP[Fany yFa].
  have [i iFan] : exists , F (a + i.+1%:R) < F a - n%:R.
    move/cvgrNy_lt : nyF.
    move/(_ (F a - n%:R)) => [z [zreal zFan]].
    by exists (truncn (z - a)); rewrite zFan// -ltrBlDl truncnS_gt.
  by exists i => //=; rewrite in_itv/= yFa (lt_le_trans _ Fany).
- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa].
  exists (truncn (F a - F (a + n.+1%:R))).+1 => //=.
  rewrite in_itv/= zFa andbT lerBlDr -lerBlDl ltW//.
  by rewrite -truncn_le_nat le_truncn// lerB// ltW.
Qed.

Lemma :
{in `[a, +oo[ &, {homo F : /~ x < y}} ->
(`]F (a + n%:R), F a[ = \bigcup_( < n) `]F (a + i.+1%:R), F a[)%classic.

Proof.

move=> decrF; rewrite eqEsubset; split.
- move: n => [|n]; first by rewrite addr0 set_itvoo0.
  by apply: (@bigcup_sup _ _ n) => /=.
- apply: bigcup_sub => k/= kn; apply: subset_itvr; rewrite bnd_simp.
  move: kn; rewrite leq_eqVlt => /predU1P[<-//|kn].
  by rewrite ltW// decrF ?in_itv/= ?andbT ?lerDl//= ltrD2l ltr_nat.
Qed.

Lemma :
{in `]-oo, a] &, {homo F : / x < y}} ->
F x @[ --> -oo] --> -oo ->
(`]-oo, F a] = \bigcup_ `]F (a - i.+1%:R), F a])%classic.

Proof.

move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split.
- move=> y/= [n _]/=; rewrite in_itv/= => /andP[Fany yFa].
  have [i iFan] : exists , F (a - i.+1%:R) < F a - n%:R.
    move/cvgrNy_lt : nyF => /(_ (F a - n%:R))[z [zreal zFan]].
    exists (truncn (a - z)).
    by rewrite zFan// ltrBlDr -ltrBlDl -truncn_le_nat.
  by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany).
- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa].
  exists (truncn (F a - F (a - n.+1%:R))).+1 => //=.
  rewrite in_itv/= zFa andbT lerBlDr -lerBlDl ltW//.
  by rewrite -truncn_le_nat le_truncn// lerB// ltW.
Qed.

Lemma :
{in `]-oo, a] &, {homo F : / x < y}} ->
(`]F (a - n%:R), F a] = \bigcup_( < n) `]F (a - i.+1%:R), F a])%classic.

Proof.

move=> incrF; rewrite eqEsubset; split.
- move: n => [|n]; first by rewrite subr0 set_itvoc0.
  by apply: (@bigcup_sup _ _ n) => /=.
- apply: bigcup_sub => k/= kn; apply: subset_itvr; rewrite bnd_simp.
  move: kn; rewrite leq_eqVlt => /predU1P[<-//|kn].
  by rewrite ltW// incrF ?in_itv/= ?andbT ?gerBl ?ler_ltB ?ltr_nat.
Qed.

End monotonic_itv_bigcup.

Section open_closed_sets.
Context { : realFieldType}.
Implicit Types x y : R.

Lemma : open [set | x < y].

Proof.

move=> x /=; rewrite -subr_gt0 => yDx_gt0. exists (y - x) => // z.
by rewrite /= ltr_distlC subrKC => /andP[].
Qed.

Hint Resolve open_lt : core.

Lemma : open [set | x > y].

Proof.

move=> x /=; rewrite -subr_gt0 => xDy_gt0; exists (x - y) => // z.
by rewrite /= ltr_distlC subKr => /andP[].
Qed.

Hint Resolve open_gt : core.

Lemma : open [set | x != y].

Proof.

rewrite (_ : mkset _ = [set | x < y] `|` [set | x > y]); last exact: openU.
by rewrite predeqE => x /=; rewrite neq_lt; symmetry; apply: (rwP orP).
Qed.

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

Proof.

move: a b => [[]a|[]] [[]b|[]]// _ _.
- have -> : [set | a < x < b] = [set | a < x] `&` [set | x < b].
by rewrite predeqE => r; rewrite /mkset; split => [/andP[? ?] //|[-> ->]].
by apply openI; [exact: open_gt | exact: open_lt].
- by under eq_set do rewrite itv_ge// inE.
- by under eq_set do rewrite in_itv andbT/=; exact: open_gt.
- exact: open_lt.
- by rewrite (_ : mkset _ = setT); [rewrite predeqE | exact: openT].
Qed.

Lemma : closed [set | x <= y].

Proof.

rewrite (_ : mkset _ = ~` [set | x > y]); last exact: open_closedC.
by rewrite predeqE => x /=; rewrite leNgt; split => /negP.
Qed.

Lemma : closed [set | y <= x].

Proof.

rewrite (_ : mkset _ = ~` [set | x < y]); last exact: open_closedC.
by rewrite predeqE => x /=; rewrite leNgt; split => /negP.
Qed.

Lemma : closed [set | x = y].

Proof.

rewrite [X in closed X](_ : (eq^~ _) = ~` (xpredC (eq_op^~ y))).
by rewrite predeqE /setC => x /=; rewrite (rwP eqP); case: eqP; split.
by apply: open_closedC; exact: open_neq.
Qed.

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

Proof.

move: a b => [[]a|[]] [[]b|[]]// _ _;
  do ?by under eq_set do rewrite itv_ge// inE falseE; apply: closed0.
- have -> : `[a, b]%classic = [set | x >= a] `&` [set | x <= b].
    by rewrite predeqE => ?; rewrite /= in_itv/=; split=> [/andP[]|[->]].
  by apply closedI; [exact: closed_ge | exact: closed_le].
- by under eq_set do rewrite in_itv andbT/=; exact: closed_ge.
- exact: closed_le.
Qed.

End open_closed_sets.
#[global] Hint Extern 0 (open _) => now apply: open_gt : core.
#[global] Hint Extern 0 (open _) => now apply: open_lt : core.
#[global] Hint Extern 0 (open _) => now apply: open_neq : core.
#[global] Hint Extern 0 (closed _) => now apply: closed_ge : core.
#[global] Hint Extern 0 (closed _) => now apply: closed_le : core.
#[global] Hint Extern 0 (closed _) => now apply: closed_eq : core.
#[global] Hint Extern 0 (open _) => now apply: interval_open : core.

Section near_in_itv.
Context { : realFieldType} ( : R).

Lemma :
{in `]a, b[, forall , \forall \near y, z \in `]a, b[}.

Proof.

exact: interval_open. Qed.

Lemma :
{in `]a, +oo[, forall , \forall \near y, z \in `]a, +oo[}.

Proof.

exact: interval_open. Qed.

Lemma :
{in `]-oo, b[, forall , \forall \near y, z \in `]-oo, b[}.

Proof.

exact: interval_open. Qed.

End near_in_itv.

Lemma { : archiRealFieldType} ( : R) :
\forall \near \oo, r < n%:R.

Proof.

exists (Num.bound r) => // n /=.
by rewrite truncn_lt_nat//; apply/le_lt_trans/ler_norm.
Qed.

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

Proof.

near=> n; rewrite invf_plt ?unfold_in//= -truncn_le_nat.
by near: n; exists (Num.truncn e%:num^-1).
Unshelve. all: by end_near. Qed.

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

Proof.

near=> n.
rewrite mul1r invf_plt ?unfold_in//=; apply: upper_nthrootP.
near: n; eexists; last by move=> m; exact.
by [].
Unshelve. all: by end_near. Qed.

Section interval.
Variable : numDomainType.

Definition ( : set R) :=
forall , E x -> E y -> forall , x <= z <= y -> E z.

Lemma ( : set R) :
is_interval E <-> forall , E x -> E y -> forall , x < z < y -> E z.

Proof.

split=> iE x y Ex Ey z /andP[].
by move=> xz zy; apply: (iE x y); rewrite ?ltW.
rewrite !le_eqVlt => /predU1P[<-//|xz] /predU1P[->//|zy].
by apply: (iE x y); rewrite ?xz.
Qed.

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

Proof.

by case: i => -[[]a|[]] [[]b|[]] // x y /=; do ?[by rewrite ?itv_ge//];
move=> xi yi z; rewrite -[x <= z <= y]/(z \in `[x, y]); apply/subitvP;
rewrite subitvE /Order.le/= ?(itvP xi, itvP yi).
Qed.

End interval.

Lemma { : realFieldType} ( : set R) : is_interval X ->
~ has_lbound X -> ~ has_ubound X -> X = setT.

Proof.

move=> iX lX uX; rewrite predeqE => x; split => // _.
move/has_lbPn : lX => /(_ x) [y Xy xy].
move/has_ubPn : uX => /(_ x) [z Xz xz].
by apply: (iX y z); rewrite ?ltW.
Qed.

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

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

Let := [set | ointsub A U /\ A (ratr q)].

Let : ointsub_rat set0 q = set0.

Proof.

by apply/seteqP; split => // A [[_ _]]; rewrite subset0 => ->. Qed.

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

Lemma : bigcup_ointsub set0 q = set0.

Proof.

by rewrite /bigcup_ointsub ointsub_rat0 bigcup_set0. Qed.

Lemma : open (bigcup_ointsub U q).

Proof.

by apply: bigcup_open => i [[]]. Qed.

Lemma : is_interval (bigcup_ointsub U q).

Proof.

move=> /= a b [A [[oA iA AU] Aq] Aa] [B [[oB iB BU] Bq] Bb] c /andP[ac cb].
have [cq|cq|->] := ltgtP c (ratr q); last by exists A.
- by exists A => //; apply: (iA a (ratr q)) => //; rewrite ac (ltW cq).
- by exists B => //; apply: (iB (ratr q) b) => //; rewrite cb (ltW cq).
Qed.

Lemma : bigcup_ointsub U q `<=` U.

Proof.

by move=> y [A [[oA _ +] _ Ay]]; exact. Qed.

Lemma :
open A -> is_interval A -> A `<=` U -> A (ratr q) ->
A `<=` bigcup_ointsub U q.

Proof.

by move=> oA itvA AU Aq x Ax; exists A. Qed.

Lemma : bigcup_ointsub U q r -> ratr q \in U.

Proof.

by case => /= V [[oV Vitv VU] Vq Vr]; exact/mem_set/VU. Qed.

see `open_disjoint_itv` in `normed_module.v` for a cover of disjoint open intervals

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

Proof.

move=> oU; have [->|U0] := eqVneq U set0.
  by rewrite bigcup0// => q _; rewrite bigcup_ointsub0.
apply/seteqP; split=> [x Ux|x [p _ Ipx]]; last exact: bigcup_ointsub_sub Ipx.
suff [q Iqx] : exists , bigcup_ointsub U q x.
  by exists q => //=; rewrite in_setE; case: Iqx => A [[_ _ +] ? _]; exact.
have : nbhs x U by rewrite nbhsE /=; exists U.
rewrite -nbhs_ballE /nbhs_ball /nbhs_ball_ => -[_/posnumP[r] xrU].
have /rat_in_itvoo[q qxxr] : (x - r%:num < x + r%:num)%R.
  by rewrite ltrBlDr -addrA ltrDl.
exists q, `](x - r%:num)%R, (x + r%:num)%R[%classic; last first.
  by rewrite /= in_itv/= ltrBlDl ltrDr// ltrDl//; apply/andP.
split=> //; split; [exact: interval_open|exact: interval_is_interval|].
move=> y /=; rewrite in_itv/= => /andP[xy yxr]; apply xrU => /=.
rewrite /ball /= /ball_ /= in xrU *; have [yx|yx] := leP x y.
  by rewrite ler0_norm ?subr_le0// opprB ltrBlDl.
by rewrite gtr0_norm ?subr_gt0// ltrBlDr -ltrBlDl.
Qed.

End open_union_rat.

Section ball_realFieldType.
Variables ( : realFieldType).

Lemma ( : R) : ball a r = set0 <-> r <= 0.

Proof.

split.
move=> /seteqP[+ _] => H; rewrite leNgt; apply/negP => r0.
by have /(_ (ballxx _ r0)) := H a.
move=> r0; apply/seteqP; split => // y; rewrite /ball/=.
by move/lt_le_trans => /(_ _ r0); rewrite normr_lt0.
Qed.

End ball_realFieldType.

Section interval_realType.
Variable : realType.

Lemma ( : set R) : is_interval X ->
~ has_lbound X -> has_ubound X -> X° = [set | r < sup X].

Proof.

move=> iX lX uX; rewrite eqEsubset; split; first exact: right_bounded_interior.
rewrite -(open_subsetE _ (@open_lt _ _)) => r rsupX.
move/has_lbPn : lX => /(_ r)[y Xy yr].
have hsX : has_sup X by split => //; exists y.
have /sup_adherent/(_ hsX)[e Xe] : 0 < sup X - r by rewrite subr_gt0.
by rewrite subKr => re; apply: (iX y e); rewrite ?ltW.
Qed.

Lemma ( : set R) : is_interval X ->
has_lbound X -> ~ has_ubound X -> X° = [set | inf X < r].

Proof.

move=> iX lX uX; rewrite eqEsubset; split; first exact: left_bounded_interior.
rewrite -(open_subsetE _ (@open_gt _ _)) => r infXr.
move/has_ubPn : uX => /(_ r)[y Xy yr].
have hiX : has_inf X by split => //; exists y.
have /inf_adherent/(_ hiX)[e Xe] : 0 < r - inf X by rewrite subr_gt0.
by rewrite addrC subrK => er; apply: (iX e y); rewrite ?ltW.
Qed.

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

Proof.

move=> iX bX aX; rewrite eqEsubset; split=> [r Xr|].
  apply/andP; split;
    [exact: left_bounded_interior|exact: right_bounded_interior].
rewrite -open_subsetE; first exact: (@interval_open _ (BRight _) (BLeft _)).
move=> r /andP[iXr rsX].
have [X0|/set0P X0] := eqVneq X set0.
  by move: (lt_trans iXr rsX); rewrite X0 inf_out ?sup_out ?ltxx // => - [[]].
have hiX : has_inf X by split.
have /inf_adherent/(_ hiX)[e Xe] : 0 < r - inf X by rewrite subr_gt0.
rewrite addrC subrK => er.
have hsX : has_sup X by split.
have /sup_adherent/(_ hsX)[f Xf] : 0 < sup X - r by rewrite subr_gt0.
by rewrite subKr => rf; apply: (iX e f); rewrite ?ltW.
Qed.

Lemma ( : R) : [set a]° = set0.

Proof.

rewrite interval_bounded_interior.
- by move=> ? ?/= -> -> r; rewrite -eq_le; move/eqP <-.
- by exists a => [?]/= ->; apply: lexx.
- by exists a => [?]/= ->; apply: lexx.
- rewrite inf1 sup1 eqEsubset; split => // => x/=.
by rewrite ltNge => /andP[/negP + ?]; apply; apply/ltW.
Qed.

Lemma ( : R) ( : bool) :
[set` Interval (BSide a x) (BSide b y)]° = `]x, y[%classic.

Proof.

have [|xy] := leP y x.
  rewrite le_eqVlt => /predU1P[-> |yx].
    by case: a; case: b; rewrite set_itvoo0 ?set_itvE ?interior_set1 ?interior0.
  rewrite !set_itv_ge ?interior0//.
  - by case: a; case: b; rewrite bnd_simp -?leNgt -?ltNge ?ltW.
  - by rewrite bnd_simp -leNgt ltW.
rewrite interval_bounded_interior//; first exact: interval_is_interval.
rewrite inf_itv; first by case: a; case b; rewrite bnd_simp ?ltW.
rewrite sup_itv; first by case: a; case b; rewrite bnd_simp ?ltW.
exact: set_itvoo.
Qed.

Lemma ( : R) ( : bool) :
[set` Interval (BSide b x) (BInfty _ false)]° = `]x, +oo[%classic.

Proof.

rewrite interval_right_unbounded_interior//.
- exact: interval_is_interval.
- by apply: hasNubound_itv; rewrite lt_eqF.
- rewrite inf_itv; first by case: b; rewrite bnd_simp ?ltW.
by rewrite set_itvoy.
Qed.

Lemma ( : R) ( : bool) :
[set` Interval (BInfty _ true) (BSide b y)]° = `]-oo, y[%classic.

Proof.

rewrite interval_left_unbounded_interior//.
- exact: interval_is_interval.
- by apply: hasNlbound_itv; rewrite gt_eqF.
- rewrite sup_itv; first by case b; rewrite bnd_simp ?ltW.
exact: set_itvNyo.
Qed.

Lemma :
[set` Interval (BInfty R true) (BInfty _ false)]° = `]-oo, +oo[%classic.

Proof.

by rewrite set_itvNyy; exact: interiorT. Qed.

Definition :=
(interior_itv_bnd, interior_itv_bndy, interior_itv_Nybnd, interior_itv_Nyy).

End interval_realType.

Files

Module mathcomp.analysis.normedtype_theory.num_normedtype