Files

Module mathcomp.analysis.normedtype_theory.ereal_normedtype

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum interval
  interval_inference.
From mathcomp Require Import boolp classical_sets ereal reals real_interval.
From mathcomp Require Import topology ereal 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 ```

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.
Context {TSource code : choiceType} {XSource code : filteredType T} {RSource code : realFieldType}.
Implicit Types (f : X -> \bar R) (F : set_system X).
Local Open Scope ereal_scope.

Definition limf_esup

limf_esup : forall {T : choiceType} {X : filteredType T} {R : realFieldType}, (X -> \bar R) -> set_system X -> \bar R limf_esup is not universe polymorphic Arguments limf_esup {T X R} f%_function_scope F limf_esup is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.ereal_normedtype.limf_esup Declared in library mathcomp.analysis.normedtype_theory.ereal_normedtype, line 47, characters 11-20

Used by
  • mathcomp.analysis.realfun
  • mathcomp.analysis.sequences
  • mathcomp.analysis.normedtype_theory.normed_module
Source code fSource code FSource code := ereal_inf [set ereal_sup (f @` V) | VSource code in F].

Definition limf_einf

limf_einf : forall {T : choiceType} {X : filteredType T} {R : realFieldType}, (X -> \bar R) -> set_system X -> \bar R limf_einf is not universe polymorphic Arguments limf_einf {T X R} f%_function_scope F limf_einf is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.ereal_normedtype.limf_einf Declared in library mathcomp.analysis.normedtype_theory.ereal_normedtype, line 49, characters 11-20

Source code fSource code FSource code := - limf_esup (\- f) F.

Lemma limf_esupESource code fSource code FSource code :
  limf_esup f F = ereal_inf [set ereal_sup (f @` V) | VSource code in F].
Proof.
by []. Qed.

Lemma limf_einfESource code fSource code FSource code :
  limf_einf f F = ereal_sup [set ereal_inf (f @` V) | VSource code 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_esupNUsed by
  • mathcomp.analysis.realfun
Source code fSource code FSource code : limf_esup (\- f) F = - limf_einf f F.
Proof.
by rewrite /limf_einf oppeK. Qed.

Lemma limf_einfNUsed by
  • mathcomp.analysis.realfun
  • mathcomp.analysis.sequences
Source code fSource code FSource code : 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.
Context {TSource code : choiceType} {XSource code : filteredType T} {RSource code : realType}.
Implicit Types (f : X -> \bar R) (F : set_system X).
Local Open Scope ereal_scope.

Lemma limf_esup_ge0Used by
  • mathcomp.analysis.realfun
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
Source code fSource code FSource code : ~ F set0 ->
  (forall xSource code, 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 {XSource code : topologicalType} {RSource code : numFieldType}.
Implicit Types f : X -> \bar R.
Local Open Scope ereal_scope.

Definition lower_semicontinuous

lower_semicontinuous : forall {X : topologicalType} {R : numFieldType}, (X -> \bar R) -> Prop lower_semicontinuous is not universe polymorphic Arguments lower_semicontinuous {X R} f%_function_scope lower_semicontinuous is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.ereal_normedtype.lower_semicontinuous Declared in library mathcomp.analysis.normedtype_theory.ereal_normedtype, line 91, characters 11-31

Used by
  • mathcomp.analysis.real_measure.measurable_realfun
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
Source code fSource code := forall xSource code aSource code, a%:E < f x ->
  exists2 VSource code, nbhs x V & forall ySource code, V y -> a%:E < f y.

Lemma lower_semicontinuousPUsed by
  • mathcomp.analysis.real_measure.measurable_realfun
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
Source code fSource code :
  lower_semicontinuous f <-> forall aSource code, open [set xSource code | 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 xSource code | a%:E < f x] => //.
by rewrite nbhsE/=; exists [set xSource code | 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 {RSource code : numFieldType}.

Let cvgeyPnumSource code {FSource code : set_system \bar R} {FFSource code : Filter F} : [<->
F --> +oo;
forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E <= x;
forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E < x;
\forall ASource code \near +oo%R, \forall xSource code \near F, A%:E < x;
\forall ASource code \near +oo%R, \forall xSource code \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 cvgeNyPnumSource code {FSource code : set_system \bar R} {FFSource code : Filter F} : [<->
F --> -oo;
forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E >= x;
forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E > x;
\forall ASource code \near -oo%R, \forall xSource code \near F, A%:E > x;
\forall ASource code \near -oo%R, \forall xSource code \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 {TSource code} {FSource code : set_system T} {FFSource code : Filter F}.
Implicit Types (f : T -> \bar R) (u : T -> R).

Lemma cvgeyPgerSource code fSource code :
  f @ F --> +oo <-> forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E <= f x.
Proof.
exact: (cvgeyPnum 0%N 1%N). Qed.

Lemma cvgeyPgtrSource code fSource code :
  f @ F --> +oo <-> forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E < f x.
Proof.
exact: (cvgeyPnum 0%N 2%N). Qed.

Lemma cvgeyPgtySource code fSource code :
  f @ F --> +oo <-> \forall ASource code \near +oo%R, \forall xSource code \near F, A%:E < f x.
Proof.
exact: (cvgeyPnum 0%N 3%N). Qed.

Lemma cvgeyPgeyUsed by
  • mathcomp.analysis.realfun
  • mathcomp.analysis.normedtype_theory.normed_module
Source code fSource code :
  f @ F --> +oo <-> \forall ASource code \near +oo%R, \forall xSource code \near F, A%:E <= f x.
Proof.
exact: (cvgeyPnum 0%N 4%N). Qed.

Lemma cvgeNyPlerSource code fSource code :
  f @ F --> -oo <-> forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E >= f x.
Proof.
exact: (cvgeNyPnum 0%N 1%N). Qed.

Lemma cvgeNyPltrSource code fSource code :
  f @ F --> -oo <-> forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E > f x.
Proof.
exact: (cvgeNyPnum 0%N 2%N). Qed.

Lemma cvgeNyPltNySource code fSource code :
  f @ F --> -oo <-> \forall ASource code \near -oo%R, \forall xSource code \near F, A%:E > f x.
Proof.
exact: (cvgeNyPnum 0%N 3%N). Qed.

Lemma cvgeNyPleNyUsed by
  • mathcomp.analysis.normedtype_theory.normed_module
Source code fSource code :
  f @ F --> -oo <-> \forall ASource code \near -oo%R, \forall xSource code \near F, A%:E >= f x.
Proof.
exact: (cvgeNyPnum 0%N 4%N). Qed.

Lemma cvgey_gerSource code fSource code :
  f @ F --> +oo -> forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E <= f x.
Proof.
by rewrite cvgeyPger. Qed.

Lemma cvgey_gtrSource code fSource code :
  f @ F --> +oo -> forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E < f x.
Proof.
by rewrite cvgeyPgtr. Qed.

Lemma cvgeNy_lerSource code fSource code :
  f @ F --> -oo -> forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E >= f x.
Proof.
by rewrite cvgeNyPler. Qed.

Lemma cvgeNy_ltrSource code fSource code :
  f @ F --> -oo -> forall ASource code, A \is Num.real -> \forall xSource code \near F, A%:E > f x.
Proof.
by rewrite cvgeNyPltr. Qed.

Lemma cvgNeyUsed by
  • mathcomp.analysis.sequences
Source code fSource code : (\- 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 cvgNeNySource code fSource code : (\- f @ F --> -oo) <-> (f @ F --> +oo).
Proof.
by rewrite -cvgNey (_ : \- \- f = f)//; apply/funeqP => x /=; rewrite oppeK.
Qed.

Lemma cvgeryPUsed by
  • mathcomp.analysis.sequences
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence
  • mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation
Source code uSource code : ((u x)%:E @[xSource code --> 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 cvgerNyPSource code uSource code : ((u x)%:E @[xSource code --> 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 {RSource code : realFieldType}.
Context {TSource code} {FSource code : set_system T} {FFSource code : Filter F} (fSource code : T -> \bar R).

Lemma cvgeyPgeUsed by
  • mathcomp.analysis.measure_theory.counting_measure
  • mathcomp.analysis.realfun
  • mathcomp.analysis.sequences
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence
  • mathcomp.analysis.normedtype_theory.normed_module
Source code : f @ F --> +oo <-> forall ASource code, \forall xSource code \near F, A%:E <= f x.
Proof.
by rewrite cvgeyPger; under eq_forall do rewrite num_real; split=> + *; apply.
Qed.

Lemma cvgeyPgtSource code : f @ F --> +oo <-> forall ASource code, \forall xSource code \near F, A%:E < f x.
Proof.
by rewrite cvgeyPgtr; under eq_forall do rewrite num_real; split=> + *; apply.
Qed.

Lemma cvgeNyPleUsed by
  • mathcomp.analysis.realfun
  • mathcomp.analysis.sequences
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence
  • mathcomp.analysis.normedtype_theory.normed_module
Source code : f @ F --> -oo <-> forall ASource code, \forall xSource code \near F, A%:E >= f x.
Proof.
by rewrite cvgeNyPler; under eq_forall do rewrite num_real; split=> + *; apply.
Qed.

Lemma cvgeNyPltSource code : f @ F --> -oo <-> forall ASource code, \forall xSource code \near F, A%:E > f x.
Proof.
by rewrite cvgeNyPltr; under eq_forall do rewrite num_real; split=> + *; apply.
Qed.

Lemma cvgey_geUsed by
  • mathcomp.analysis.real_measure.lebesgue_measure
Source code : f @ F --> +oo -> forall ASource code, \forall xSource code \near F, A%:E <= f x.
Proof.
by rewrite cvgeyPge. Qed.

Lemma cvgey_gtSource code : f @ F --> +oo -> forall ASource code, \forall xSource code \near F, A%:E < f x.
Proof.
by rewrite cvgeyPgt. Qed.

Lemma cvgeNy_leSource code : f @ F --> -oo -> forall ASource code, \forall xSource code \near F, A%:E >= f x.
Proof.
by rewrite cvgeNyPle. Qed.

Lemma cvgeNy_ltSource code : f @ F --> -oo -> forall ASource code, \forall xSource code \near F, A%:E > f x.
Proof.
by rewrite cvgeNyPlt. Qed.

End ecvg_infty_realField.

Local Open Scope ereal_scope.
Lemma ge0_cvgeMlyUsed by
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
Source code (RSource code : realType) (aSource code : \bar R) : 0 <= a ->
  (n%:R%:E * a) @[nSource code --> \oo] --> +oo * a.
Proof.
rewrite le_eqVlt => /predU1P[<-|a_gt0].
  by rewrite mule0; under eq_fun do rewrite mule0; exact: cvg_cst.
rewrite gt0_mulye//; apply/cvgeyPge => A.
move: a a_gt0 => [r /[!(@lte_fin R)] r0|_ |//].
- near=> n; rewrite -EFinM lee_fin -ler_pdivrMr//.
  by near: n; exact: nbhs_infty_ger.
- near=> n; rewrite gt0_muley ?leey// lte_fin ltr0n//.
  by near: n; exact: nbhs_infty_gt.
Unshelve. all: by end_near. Qed.
Local Close Scope ereal_scope.

Section open_closed_sets_ereal.
Context {RSource code : realFieldType} .
Local Open Scope ereal_scope.
Implicit Types (x y : \bar R) (r : R).

Lemma open_ereal_ltSource code ySource code : open [set rSource code : 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_ereal_gtSource code ySource code : open [set rSource code : 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 open_ereal_lt'Source code xSource code ySource code : x < y -> ereal_nbhs x (fun uSource code => 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 open_ereal_gt'Source code xSource code ySource code : y < x -> ereal_nbhs x (fun uSource code => 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_ereal_lt_erealSource code xSource code : open [set ySource code | y < x].
Proof.
have openr r : open [set xSource code : \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 ySource code | y < +oo] = \bigcup_rSource code [set ySource code : \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_ereal_gt_erealSource code xSource code : open [set ySource code | x < y].
Proof.
have openr r : open [set xSource code | 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 ySource code | -oo < y] = \bigcup_rSource code [set ySource code : \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_ereal_le_erealUsed by
  • mathcomp.analysis.measure_theory.signed_measure
Source code ySource code : closed [set xSource code | y <= x].
Proof.
rewrite (_ : [set xSource code | y <= x] = ~` [set xSource code | y > x]).
  by rewrite predeqE=> x; split=> [rx|/negP]; [apply/negP|]; rewrite -leNgt.
exact/open_closedC/open_ereal_lt_ereal.
Qed.

Lemma closed_ereal_ge_erealSource code ySource code : closed [set xSource code | y >= x].
Proof.
rewrite (_ : [set xSource code | y >= x] = ~` [set xSource code | 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.
Context {RSource code : realFieldType}.
Implicit Types r : R.

Lemma nbhs_image_EFinSource code rSource code (XSource code : set R) :
  nbhs r X -> nbhs r%:E ((fun rSource code => r%:E) @` X).
Proof.
case => _/posnumP[e] xeX; exists e%:num => //= s res.
by exists s => //; exact: xeX.
Qed.

Lemma nbhs_open_ereal_ltSource code rSource code (fSource code : R -> R) : r < f r ->
  nbhs r%:E [set ySource code | 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 nbhs_open_ereal_gtSource code rSource code (fSource code : R -> R) : f r < r ->
  nbhs r%:E [set ySource code | (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_open_ereal_pinftySource code rSource code : (nbhs +oo [set ySource code | 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_open_ereal_ninftySource code rSource code : (nbhs -oo [set ySource code | y < r%:E])%E.
Proof.
rewrite nbhsE /=; eexists; last by move=> y; exact.
by split; [apply open_ereal_lt_ereal | rewrite /= ltNyr].
Qed.

Lemma ereal_hausdorffSource code : 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 xSource code => 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 xSource code => 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 xSource code => 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 xSource code => 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 {TSource code : Type} {FSource code : set_system T} {FFSource code : ProperFilter F} {RSource code : realFieldType}.
Local Open Scope ereal_scope.
Implicit Types f g h : T -> \bar R.

Lemma cvge_to_geSource code fSource code bSource code cSource code : f @ F --> c -> (\forall aSource code \near F, b <= f a) -> b <= c.
Proof.
by move=> /[swap]/(closed_cvg _ (@closed_ereal_le_ereal _ b)) /[apply].
Qed.

Lemma cvge_to_leSource code fSource code bSource code cSource code : f @ F --> c -> (\forall aSource code \near F, f a <= b) -> c <= b.
Proof.
by move=> /[swap]/(closed_cvg _ (@closed_ereal_ge_ereal _ b))/[apply].
Qed.

Lemma lime_geUsed by
  • mathcomp.analysis.ess_sup_inf
  • mathcomp.analysis.measure_theory.measure_extension
  • mathcomp.analysis.measure_theory.signed_measure
  • mathcomp.analysis.measure_theory.measure_function
  • mathcomp.analysis.realfun
  • mathcomp.analysis.sequences
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence
  • mathcomp.analysis.lebesgue_integral_theory.radon_nikodym
  • mathcomp.analysis.normedtype_theory.normed_module
Source code xSource code fSource code :
  cvg (f @ F) -> (\forall aSource code \near F, x <= f a) -> x <= lim (f @ F).
Proof.
exact: cvge_to_ge. Qed.

Lemma lime_leUsed by
  • mathcomp.analysis.esum
  • mathcomp.analysis.measure_theory.signed_measure
  • mathcomp.analysis.measure_theory.measure_function
  • mathcomp.analysis.realfun
  • mathcomp.analysis.sequences
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence
  • mathcomp.analysis.lebesgue_integral_theory.radon_nikodym
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
  • mathcomp.analysis.normedtype_theory.normed_module
Source code xSource code fSource code :
  cvg (f @ F) -> (\forall aSource code \near F, x >= f a) -> x >= lim (f @ F).
Proof.
exact: cvge_to_le. Qed.

End ProperFilterERealType.

Lemma cvgenyPUsed by
  • mathcomp.analysis.real_measure.lebesgue_measure
  • mathcomp.analysis.measure_theory.counting_measure
Source code {RSource code : realType} {TSource code} {FSource code : set_system T} {FFSource code : Filter F} (fSource code : T -> nat) :
  (((f n)%:R : R)%:E @[nSource code --> F] --> +oo%E) <-> (f @ F --> \oo).
Proof.
by rewrite cvgeryP cvgrnyP. Qed.

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

Lemma nbhs_ereal_pinftySource code :
  (\forall xSource code \near +oo%E, P x) <-> [/\ P +oo%E & \forall xSource code \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 nbhs_ereal_ninftySource code :
  (\forall xSource code \near -oo%E, P x) <-> [/\ P -oo%E & \forall xSource code \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.
Context {RSource code : realFieldType}.

Let ereal_order_nbhsESource code (xSource code : \bar R) :
  nbhs x = filter_from (fun iSource code => itv_open_ends i /\ x \in i)
                       (fun iSource code => [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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Order_isNbhsSource code.Build _ (\bar R) ereal_order_nbhsE.

End ereal_OrderNbhs.
Generated by rocqnavi
Source
Uses
Used By