Module mathcomp.analysis.normedtype_theory.ereal_normedtype

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum interval.
From mathcomp Require Import interval_inference.
From mathcomp Require Import boolp classical_sets ereal reals topology.
From mathcomp Require Import real_interval num_normedtype.

# Preliminaries for norm-related notions This file contains various definitions and lemmas about topological notions for extended numeric types that are useful to develop the theory of normed modules in this directory. ## Limit superior and inferior ``` limf_esup f F, limf_einf f F == limit sup/inferior of f at "filter" F f has type X -> \bar R. F has type set_system X. ``` ## Lower semicontinuous ``` lower_semicontinuous f == the extended real-valued function f is lower-semicontinuous. The type of f is X -> \bar R with X : topologicalType and R : realType ```

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.

Section limf_esup_einf.
Variables ( : choiceType) ( : filteredType T) ( : realFieldType).
Implicit Types (f : X -> \bar R) (F : set_system X).
Local Open Scope ereal_scope.

Definition := ereal_inf [set ereal_sup (f @` V) | in F].

Definition := - limf_esup (\- f) F.

Lemma :
limf_esup f F = ereal_inf [set ereal_sup (f @` V) | in F].

Proof.

by []. Qed.

Lemma :
limf_einf f F = ereal_sup [set ereal_inf (f @` V) | in F].

Proof.

rewrite /limf_einf limf_esupE /ereal_inf oppeK -[in RHS]image_comp /=.
congr (ereal_sup [set _ | _ in [set ereal_sup _ | _ in _]]).
by under eq_fun do rewrite -image_comp.
Qed.

Lemma : limf_esup (\- f) F = - limf_einf f F.

Proof.

by rewrite /limf_einf oppeK. Qed.

Lemma : limf_einf (\- f) F = - limf_esup f F.

Proof.

by rewrite /limf_einf; under eq_fun do rewrite oppeK. Qed.

End limf_esup_einf.

Section limf_esup_einf_realType.
Variables ( : choiceType) ( : filteredType T) ( : realType).
Implicit Types (f : X -> \bar R) (F : set_system X).
Local Open Scope ereal_scope.

Lemma : ~ F set0 ->
(forall , 0 <= f x) -> 0 <= limf_esup f F.

Proof.

move=> F0 f0; rewrite limf_esupE; apply: le_ereal_inf_tmp => /= x [A].
have [-> /F0//|/set0P[y Ay FA] <-{x}] := eqVneq A set0.
by apply: le_ereal_sup_tmp; exists (f y).
Qed.

End limf_esup_einf_realType.

Section lower_semicontinuous.
Context { : topologicalType} { : numFieldType}.
Implicit Types f : X -> \bar R.
Local Open Scope ereal_scope.

Definition := forall , a%:E < f x ->
exists2 , nbhs x V & forall , V y -> a%:E < f y.

Lemma :
lower_semicontinuous f <-> forall , open [set | f x > a%:E].

Proof.

split=> [sci a|openf x a afx].
  rewrite openE /= => x /= /sci[A + Aaf]; rewrite nbhsE /= => -[B xB BA].
  apply: nbhs_singleton; apply: nbhs_interior.
  by rewrite nbhsE /=; exists B => // y /BA /=; exact: Aaf.
exists [set | a%:E < f x] => //.
by rewrite nbhsE/=; exists [set | a%:E < f x].
Qed.

End lower_semicontinuous.

#[global] Hint Extern 0 (is_true (_ < ?x)%E) => match goal with
  H : x \is_near _ |- _ => solve[near: x; apply: ereal_nbhs_pinfty_gt] end : core.
#[global] Hint Extern 0 (is_true (_ <= ?x)%E) => match goal with
  H : x \is_near _ |- _ => solve[near: x; apply: ereal_nbhs_pinfty_ge] end : core.
#[global] Hint Extern 0 (is_true (_ > ?x)%E) => match goal with
  H : x \is_near _ |- _ => solve[near: x; apply: ereal_nbhs_ninfty_lt] end : core.
#[global] Hint Extern 0 (is_true (_ >= ?x)%E) => match goal with
  H : x \is_near _ |- _ => solve[near: x; apply: ereal_nbhs_ninfty_le] end : core.
#[global] Hint Extern 0 (is_true (fine ?x \is Num.real)) => match goal with
  H : x \is_near _ |- _ => solve[near: x; apply: ereal_nbhs_pinfty_real] end : core.
#[global] Hint Extern 0 (is_true (fine ?x \is Num.real)) => match goal with
  H : x \is_near _ |- _ => solve[near: x; apply: ereal_nbhs_ninfty_real] end : core.

Section ecvg_infty_numField.
Local Open Scope ereal_scope.
Context { : numFieldType}.

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

Proof.

tfae; first by move=> Foo A Areal; apply: Foo; apply: ereal_nbhs_pinfty_ge.
- move=> AF A Areal; near +oo_R => B.
by near do rewrite (@lt_le_trans _ _ B%:E) ?lte_fin//; 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; rewrite (@lt_le_trans _ _ B%:E) ?lte_fin//]; apply: AF.
Unshelve. all: end_near. Qed.

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

Proof.

tfae; first by move=> Foo A Areal; apply: Foo; apply: ereal_nbhs_ninfty_le.
- move=> AF A Areal; near -oo_R => B.
by near do rewrite (@le_lt_trans _ _ B%:E) ?lte_fin//; 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; rewrite (@le_lt_trans _ _ B%:E) ?lte_fin//]; apply: AF.
Unshelve. all: end_near. Qed.

Context {} { : set_system T} { : Filter F}.
Implicit Types (f : T -> \bar R) (u : T -> R).

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite cvgeyPger. Qed.

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

Proof.

by rewrite cvgeyPgtr. Qed.

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

Proof.

by rewrite cvgeNyPler. Qed.

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

Proof.

by rewrite cvgeNyPltr. Qed.

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

Proof.

rewrite cvgeNyPler cvgeyPger; split=> Foo A Areal;
by near do rewrite -leeN2 ?oppeK; apply: Foo; rewrite rpredN.
Unshelve. all: end_near. Qed.

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

Proof.

by rewrite -cvgNey (_ : \- \- f = f)//; apply/funeqP => x /=; rewrite oppeK.
Qed.

Lemma : ((u x)%:E @[ --> F] --> +oo) <-> (u @ F --> +oo%R).

Proof.

split=> [/cvgeyPger|/cvgryPger] Foo.
by apply/cvgryPger => A Ar; near do rewrite -lee_fin; apply: Foo.
by apply/cvgeyPger => A Ar; near do rewrite lee_fin; apply: Foo.
Unshelve. all: end_near. Qed.

Lemma : ((u x)%:E @[ --> F] --> -oo) <-> (u @ F --> -oo%R).

Proof.

split=> [/cvgeNyPler|/cvgrNyPler] Foo.
by apply/cvgrNyPler => A Ar; near do rewrite -lee_fin; apply: Foo.
by apply/cvgeNyPler => A Ar; near do rewrite lee_fin; apply: Foo.
Unshelve. all: end_near. Qed.

End ecvg_infty_numField.

Section ecvg_infty_realField.
Local Open Scope ereal_scope.
Context { : realFieldType}.
Context {} { : set_system T} { : Filter F} ( : T -> \bar R).

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite cvgeyPge. Qed.

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

Proof.

by rewrite cvgeyPgt. Qed.

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

Proof.

by rewrite cvgeNyPle. Qed.

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

Proof.

by rewrite cvgeNyPlt. Qed.

End ecvg_infty_realField.

Section open_closed_sets_ereal.
Variable : realFieldType .
Local Open Scope ereal_scope.
Implicit Types x y : \bar R.
Implicit Types r : R.

Lemma : open [set : R | r%:E < y].

Proof.

case: y => [y||] /=; first exact: open_lt.
- rewrite (_ : [set _ | _] = setT); last exact: openT.
by rewrite funeqE => ? /=; rewrite ltry trueE.
- rewrite (_ : [set _ | _] = set0); last exact: open0.
by rewrite funeqE => ? /=; rewrite falseE.
Qed.

Lemma : open [set : R | y < r%:E].

Proof.

case: y => [y||] /=; first exact: open_gt.
- rewrite (_ : [set _ | _] = set0); last exact: open0.
by rewrite funeqE => ? /=; rewrite falseE.
- rewrite (_ : [set _ | _] = setT); last exact: openT.
by rewrite funeqE => ? /=; rewrite ltNyr trueE.
Qed.

Lemma : x < y -> ereal_nbhs x (fun => u < y).

Proof.

case: x => [x|//|] xy; first exact: open_ereal_lt.
- case: y => [y||//] /= in xy *; last by exists 0%R.
  by exists y; rewrite num_real; split => //= x ?.
- case: y => [y||//] /= in xy *.
  + by exists y; rewrite num_real; split => //= x ?.
  + by exists 0%R; split => // x /lt_le_trans; apply; rewrite leey.
Qed.

Lemma : y < x -> ereal_nbhs x (fun => y < u).

Proof.

case: x => [x||] //=; do ?[exact: open_ereal_gt];
case: y => [y||] //=; do ?by exists 0.
- by exists y; rewrite num_real.
- by move=> _; exists 0%R; split => // x; apply/le_lt_trans; rewrite leNye.
Qed.

Lemma : open [set | y < x].

Proof.

have openr r : open [set : \bar R | x < r%:E].
  (* BUG: why doesn't case work? *)
  move=> [? | // | ?]; [rewrite /= lte_fin => xy | by exists r].
  by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin.
move: x => [ // | | ]; last by move=> []. (* same BUG *)
suff -> : [set | y < +oo] = \bigcup_ [set : \bar R | y < r%:E].
  exact: bigcup_open.
rewrite predeqE => -[r | | ]/=.
- rewrite ltry; split => // _.
  by exists (r + 1)%R => //=; rewrite lte_fin ltrDl.
- by rewrite ltxx; split => // -[] x /=; rewrite ltNge leey.
- by split => // _; exists 0%R => //=; rewrite ltNye.
Qed.

Lemma : open [set | x < y].

Proof.

have openr r : open [set | r%:E < x].
  move=> [? | ? | //]; [rewrite /= lte_fin => xy | by exists r].
  by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin.
case: x => [ // | | ]; first by move=> [].
suff -> : [set | -oo < y] = \bigcup_ [set : \bar R | r%:E < y].
  exact: bigcup_open.
rewrite predeqE => -[r | | ]/=.
- rewrite ltNyr; split => // _.
  by exists (r - 1)%R => //=; rewrite lte_fin ltrBlDr ltrDl.
- by split => // _; exists 0%R => //=; rewrite ltey.
- by rewrite ltxx; split => // -[] x _ /=; rewrite ltNge leNye.
Qed.

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

Proof.

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

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

Proof.

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

End open_closed_sets_ereal.

Section ereal_is_hausdorff.
Variable : realFieldType.
Implicit Types r : R.

Lemma ( : set R) :
nbhs r X -> nbhs r%:E ((fun => r%:E) @` X).

Proof.

case => _/posnumP[e] xeX; exists e%:num => //= s res.
by exists s => //; exact: xeX.
Qed.

Lemma ( : R -> R) : r < f r ->
nbhs r%:E [set | y < (f r)%:E]%E.

Proof.

move=> xfx; rewrite nbhsE /=; eexists; last by move=> y; exact.
by split; [apply open_ereal_lt_ereal | rewrite /= lte_fin].
Qed.

Lemma ( : R -> R) : f r < r ->
nbhs r%:E [set | (f r)%:E < y]%E.

Proof.

move=> xfx; rewrite nbhsE /=; eexists; last by move=> y; exact.
by split; [apply open_ereal_gt_ereal | rewrite /= lte_fin].
Qed.

Lemma : (nbhs +oo [set | r%:E < y])%E.

Proof.

rewrite nbhsE /=; eexists; last by move=> y; exact.
by split; [apply open_ereal_gt_ereal | rewrite /= ltry].
Qed.

Lemma : (nbhs -oo [set | y < r%:E])%E.

Proof.

rewrite nbhsE /=; eexists; last by move=> y; exact.
by split; [apply open_ereal_lt_ereal | rewrite /= ltNyr].
Qed.

Lemma : hausdorff_space (\bar R).

Proof.

move=> -[r| |] // [r' | |] //=.
- move=> rr'; congr (_%:E); apply Rhausdorff => /= A B rA r'B.
  have [/= z [[r0 ? r0z] [r1 ?]]] :=
    rr' _ _ (nbhs_image_EFin rA) (nbhs_image_EFin r'B).
  by rewrite -r0z => -[r1r0]; exists r0; split => //; rewrite -r1r0.
- have /(@nbhs_open_ereal_lt _ (fun => x + 1)) loc_r : r < r + 1.
    by rewrite ltrDl.
  move/(_ _ _ loc_r (nbhs_open_ereal_pinfty (r + 1))) => -[z [zr rz]].
  by move: (lt_trans rz zr); rewrite lte_fin ltxx.
- have /(@nbhs_open_ereal_gt _ (fun => x - 1)) loc_r : r - 1 < r.
    by rewrite ltrBlDr ltrDl.
  move/(_ _ _ loc_r (nbhs_open_ereal_ninfty (r - 1))) => -[z [rz zr]].
  by move: (lt_trans zr rz); rewrite ltxx.
- have /(@nbhs_open_ereal_lt _ (fun => x + 1)) loc_r' : r' < r' + 1.
    by rewrite ltrDl.
  move/(_ _ _ (nbhs_open_ereal_pinfty (r' + 1)) loc_r') => -[z [r'z zr']].
  by move: (lt_trans zr' r'z); rewrite ltxx.
- move/(_ _ _ (nbhs_open_ereal_pinfty 0) (nbhs_open_ereal_ninfty 0)).
  by move=> -[z [zx xz]]; move: (lt_trans xz zx); rewrite ltxx.
- have /(@nbhs_open_ereal_gt _ (fun => x - 1)) yB : r' - 1 < r'.
    by rewrite ltrBlDr ltrDl.
  move/(_ _ _ (nbhs_open_ereal_ninfty (r' - 1)) yB) => -[z [zr' r'z]].
  by move: (lt_trans r'z zr'); rewrite ltxx.
- move/(_ _ _ (nbhs_open_ereal_ninfty 0) (nbhs_open_ereal_pinfty 0)).
  by move=> -[z [zO Oz]]; move: (lt_trans Oz zO); rewrite ltxx.
Qed.

End ereal_is_hausdorff.

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

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

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

Proof.

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

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

Proof.

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

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

Proof.

exact: cvge_to_ge. Qed.

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

Proof.

exact: cvge_to_le. Qed.

End ProperFilterERealType.

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

Proof.

by rewrite cvgeryP cvgrnyP. Qed.

Section nbhs_ereal.
Context { : numFieldType} ( : \bar R -> Prop).

Lemma ( : R) : (\forall \near x%:E, P y) <-> \near , P x%:E.

Proof.

done. Qed.

Lemma :
(\forall \near +oo%E, P x) <-> [/\ P +oo%E & \forall \near +oo, P x%:E].

Proof.

split=> [|[Py]] [x [xr Px]]; last by exists x; split=> // -[y||]//; apply: Px.
by split; [|exists x; split=> // y xy]; apply: Px.
Qed.

Lemma :
(\forall \near -oo%E, P x) <-> [/\ P -oo%E & \forall \near -oo, P x%:E].

Proof.

split=> [|[Py]] [x [xr Px]]; last by exists x; split=> // -[y||]//; apply: Px.
by split; [|exists x; split=> // y xy]; apply: Px.
Qed.

End nbhs_ereal.

Section ereal_OrderNbhs.
Variable : realFieldType.

Let ( : \bar R) :
nbhs x = filter_from (fun => itv_open_ends i /\ x \in i)
(fun => [set` i]).

Proof.

apply/seteqP; split=> A.
- rewrite /nbhs/= /ereal_nbhs/=; move: x => [r [e/= e0 reA]||].
  + exists `](r - e)%:E, (r + e)%:E[ => [|[y|/andP[]//|//]]; rewrite ?in_itv/=.
    * by rewrite !lte_fin ltrBlDr andbb ltrDl; split => //; right.
    * by move/subset_ball_prop_in_itv : reA => /(_ y); rewrite /= !in_itv.
  + case=> M [Mreal MA].
    exists `]M%:E, +oo[ => [|y/=]; rewrite in_itv/= andbT ?ltry; last exact: MA.
    by split => //; left.
  + case=> M [Mreal MA].
    exists `]-oo, M%:E[ => [|y/=]; rewrite in_itv/= ?ltNyr; last exact: MA.
    by split => //; left.
- move=> [[ [[]/= r|[]] [[]/= s|[]] ]][]// _.
  + move=> /[dup]/ltgte_fin_num/fineK <-; rewrite in_itv/=.
    move=> /andP[rx sx] rsA; apply: (nbhs_interval rx sx) => z rz zs.
    by apply: rsA =>/=; rewrite in_itv/= rz.
  + rewrite nbhsE/= => rx rA; exists `]r, +oo[%classic => //.
    by split => //; rewrite set_itvE; exact: open_ereal_gt_ereal.
  + rewrite nbhsE/= => xs ?; exists `]-oo, s[%classic => //.
    by split => //; rewrite set_itvE; exact: open_ereal_lt_ereal.
  + by rewrite set_itvE/= subTset => _ ->; exact: filter_nbhsT.
Qed.

..Build _ (\bar R) ereal_order_nbhsE.

End ereal_OrderNbhs.

Files

Module mathcomp.analysis.normedtype_theory.ereal_normedtype