Library Lebesgue.UniformSpace_compl

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Complements on uniform spaces.

Description

It is based on the uniform spaces provided by the Coquelicot library.

Used logic axioms


From Requisite Require Import stdlib_wR.

From Coquelicot Require Import Coquelicot. Close Scope R_scope.

From Numbers Require Import countable_sets.
From Subsets Require Import Subsets_wDep.
From Lebesgue Require Import R_compl Rbar_compl.

Local Open Scope R_scope.

Section UniformSpace_compl.

Complements on UniformSpace.



Definition at_left_alt (x : R) : (R Prop) Prop :=
  within (fun x'x' x) (locally x).
Definition at_right_alt (x : R) : (R Prop) Prop :=
  within (fun x'x x') (locally x).

Lemma filterlim_within :
   {T : Type} {U : UniformSpace} {F} {FF : Filter F} {G} {FG : Filter G}
      (D : U Prop) (f : T U),
    F (fun xD (f x))
    filterlim f F G
    filterlim f F (within D G).
Proof.
intros T U F FF G FG D f HfD Hflim P HP.
unfold filtermap.
apply filter_imp with (fun xD (f x) (D (f x) P (f x))); try tauto.
apply filter_and; try assumption.
apply (Hflim (fun x'D x' P x') HP).
Qed.

Lemma open_not_equiv :
   {T : UniformSpace} (A : T Prop),
    open (fun x¬ A x) closed A.
Proof.
intros T A; split; try apply open_not.
intros HA x; apply or_to_imply.
destruct (imply_to_or _ _ (HA x)) as [Hx | Hx].
right; apply NNPP; easy.
left; easy.
Qed.

Lemma closed_not_equiv :
   {T : UniformSpace} (A : T Prop),
    closed (fun x¬ A x) open A.
Proof.
assert (H : T (A : T Prop), A = fun x¬ ¬ A x).
  intros; apply subset_ext; intros; split; try easy; apply NNPP.
intros T A; rewrite (H T A) at 1.
rewrite open_not_equiv; easy.
Qed.

Lemma open_and_finite :
   {T : UniformSpace} (A : nat T Prop) N,
    ( n, (n < S N)%nat open (A n))
    open (fun x n, (n < S N)%nat A n x).
Proof.
intros T A N HA; induction N as [ | N HN].
apply open_ext with (A 0%nat); auto.
intros x; split; intros Hx; auto.
intros n Hn; rewrite lt_1 in Hn; rewrite Hn; easy.
apply open_ext with (fun x( n, (n < S N)%nat A n x) A (S N) x).
intros x; split.
intros [Hx1 Hx2] n Hn; rewrite lt_S in Hn;
    destruct Hn as [Hn | Hn]; try rewrite Hn; auto.
intros Hx; split; intros; apply Hx; lia.
apply open_and.
apply HN; intros; auto.
auto.
Qed.

Lemma open_or_any :
   {T : UniformSpace} {Idx : Type} (A : Idx T Prop),
    ( i, open (A i)) open (fun x i, A i x).
Proof.
intros T Idx A HA x [i Hx].
destruct (HA i x Hx) as [e He].
e; intros; i; auto.
Qed.

Lemma open_or_count :
   {T : UniformSpace} (A : nat T Prop),
    ( n, open (A n)) open (fun x n, A n x).
Proof.
intro; apply open_or_any.
Qed.

Lemma open_or_finite :
   {T : UniformSpace} (A : nat T Prop) N,
    ( n, (n < S N)%nat open (A n))
    open (fun x n, (n < S N)%nat A n x).
Proof.
intros T A N HA.
pose (B n := match (lt_dec n (S N)) with | left _A n | right _fun _False end).
assert (HB1 : n, (n < S N)%nat B n = A n).
  intros n Hn; unfold B; case (lt_dec n (S N)); intros Hn'; easy.
assert (HB2 : n, (¬ n < S N)%nat B n = fun _False).
  intros n Hn; unfold B; case (lt_dec n (S N)); easy.
apply open_ext with (fun x n, B n x).
intros x; split.
intros [n Hx]; case (lt_dec n (S N)); intros Hn.
n; split; try easy; rewrite HB1 in Hx; easy.
rewrite HB2 in Hx; easy.
intros [n [Hn Hx]]; n; rewrite HB1; easy.
apply open_or_count; intros n.
case (lt_dec n (S N)); intros Hn.
rewrite HB1; auto.
rewrite HB2; try apply open_false; easy.
Qed.

Lemma closed_or_finite :
   {T : UniformSpace} (A : nat T Prop) N,
    ( n, (n < S N)%nat closed (A n))
    closed (fun x n, (n < S N)%nat A n x).
Proof.
intros T A N HA.
apply closed_ext with (fun x¬ n, (n < S N)%nat ¬ A n x).
intros x; split; intros Hx1.
apply not_all_not_ex; intros Hx2; apply Hx1; intros n Hn Hx3; apply (Hx2 n); easy.
intros Hx2; contradict Hx1; apply all_not_not_ex; intros n Hx3; apply (Hx2 n); easy.
apply closed_not, open_and_finite; intros; apply open_not; auto.
Qed.

Lemma closed_and_any :
   {T : UniformSpace} {Idx : Type} (A : Idx T Prop),
    ( i, closed (A i)) closed (fun x i, A i x).
Proof.
intros T Idx A HA.
apply closed_ext with (fun x¬ i, ¬ A i x).
intros x; split; [apply not_ex_not_all | intros Hx1 [n Hx2]; auto].
apply closed_not, open_or_any; intros; apply open_not; auto.
Qed.

Lemma closed_and_count :
   {T : UniformSpace} (A : nat T Prop),
    ( n, closed (A n)) closed (fun x n, A n x).
Proof.
intro; apply closed_and_any.
Qed.

Lemma closed_and_finite :
   {T : UniformSpace} (A : nat T Prop) N,
    ( n, (n < S N)%nat closed (A n))
    closed (fun x n, (n < S N)%nat A n x).
Proof.
intros T A N HA.
apply closed_ext with (fun x¬ n, (n < S N)%nat ¬ A n x).
intros x; split; intros Hx1.
apply NNPP; intros Hx2; apply not_all_ex_not in Hx2; destruct Hx2 as [n Hn];
    apply Hx1; n; auto with zarith.
intros [n [Hn Hx2]]; auto.
apply closed_not, open_or_finite; intros; apply open_not; auto.
Qed.

Lemma open_ball :
   {K} (x : AbsRing_UniformSpace K) r, open (ball x r).
Proof.
unfold ball; simpl; unfold AbsRing_ball. intros K x r.
case (Rle_lt_dec r 0); intro Hr.
apply open_ext with (fun _False); try easy.
intros y; split; intros Hy; try easy. contradict Hr.
apply Rlt_not_le, Rle_lt_trans with (abs (minus y x));
    try apply abs_ge_0; easy.
intros y Hy.
pose (e := (r - abs (minus y x)) / 2).
assert (He0 : 0 < e) by (apply Rdiv_lt_0_compat; lra).
(mkposreal e He0); simpl. unfold ball; simpl; unfold AbsRing_ball.
intros t Ht; replace r with (abs (minus y x) + e + e).
apply AbsRing_ball_triangle with y; try easy. unfold AbsRing_ball; lra.
unfold e; lra.
Qed.

Lemma open_fst :
   {T1 T2 : UniformSpace} (A : T1 Prop),
    open A open (fun (x : T1 × T2) ⇒ A (fst x)).
Proof.
intros T1 T2 A HA x Hx.
destruct (HA _ Hx) as [e He].
e; intros y [Hy _]; auto.
Qed.

Lemma open_snd :
   {T1 T2 : UniformSpace} (A : T2 Prop),
    open A open (fun (x : T1 × T2) ⇒ A (snd x)).
Proof.
intros T1 T2 A HA x Hx.
destruct (HA _ Hx) as [e He].
e; intros y [_ Hy]; auto.
Qed.

Lemma open_prod :
   {T1 T2 : UniformSpace} (A1 : T1 Prop) (A2 : T2 Prop),
    open A1 open A2 open (fun xA1 (fst x) A2 (snd x)).
Proof.
intros T1 T2 A1 A2 HA1 HA2 x [Hx1 Hx2].
destruct (HA1 (fst x) Hx1) as [[e1 He1a] He1b].
destruct (HA2 (snd x) Hx2) as [[e2 He2a] He2b].
pose (e := Rmin e1 e2).
assert (He0 : 0 < e) by now apply Rmin_pos.
(mkposreal e He0).
intros y [Hy1 Hy2]; split; [apply He1b | apply He2b];
    apply ball_le with e; try easy; [apply Rmin_l | apply Rmin_r].
Qed.


End UniformSpace_compl.

Section topo_basis_Def.

Definition is_topo_basis :
     {T : UniformSpace} {Idx : Type}, (Idx T Prop) Prop :=
  fun T Idx B
    ( i, open (B i))
    ( A, open A P, x, A x i, P i B i x).

Definition is_topo_basis_Prop :
     {T : UniformSpace}, ((T Prop) Prop) Prop :=
  fun T PB
    ( B, PB B open B)
    ( A, open A
       x, A x B, (PB B y, B y A y) B x).

Definition is_second_countable : UniformSpace Prop :=
  fun T (B : nat T Prop), is_topo_basis B.

Context {T1 T2 : UniformSpace}.

Variable B1 : nat T1 Prop.
Variable B2 : nat T2 Prop.

Definition topo_basis_Prod : (nat T1 × T2 Prop) :=
  fun nlet n1n2 := bij_NN2 n in fun x
    B1 (fst n1n2) (fst x) B2 (snd n1n2) (snd x).

End topo_basis_Def.

Section topo_basis_Facts1.

Context {T : UniformSpace}.

Lemma is_topo_basis_Prop_open : is_topo_basis_Prop (@open T).
Proof.
split; try easy.
intros A HA x; split.
intros Hx; A; easy.
intros [B [[HB1 HB2] HB3]]; auto.
Qed.


Context {K1 K2 : AbsRing}.

Let T1 := AbsRing_UniformSpace K1.
Let T2 := AbsRing_UniformSpace K2.

Lemma topo_basis_Prod_correct :
   (B1 : nat T1 Prop) (B2 : nat T2 Prop),
    is_topo_basis B1 is_topo_basis B2 is_topo_basis (topo_basis_Prod B1 B2).
Proof.
intros B1 B2 [HB1a HB1b] [HB2a HB2b]; split.
intros; apply open_prod; auto.
intros A HA; (fun n x, topo_basis_Prod B1 B2 n x A x).
intros x; split.
intros Hx; destruct (HA x Hx) as [e He].
pose (A1 := ball (fst x) e).
assert (HA1 : open A1) by apply open_ball.
assert (Hx1 : A1 (fst x)) by apply ball_center.
destruct (HB1b A1 HA1) as [P1 HP1].
destruct (proj1 (HP1 (fst x)) Hx1) as [n1 [Hn1a Hn1b]].
pose (A2 := ball(snd x) e).
assert (HA2 : open A2) by apply open_ball.
assert (Hx2 : A2 (snd x)) by apply ball_center.
destruct (HB2b A2 HA2) as [P2 HP2].
destruct (proj1 (HP2 (snd x)) Hx2) as [n2 [Hn2a Hn2b]].
(bij_N2N (n1, n2)); split.
intros y [Hy1 Hy2]; rewrite bij_NN2N in ×.
apply He; split; [apply <- HP1; n1 | apply HP2; n2]; easy.
split; rewrite bij_NN2N; easy.
intros [n [Hn1 Hn2]]; auto.
Qed.

Lemma is_second_countable_Prod :
  is_second_countable T1 is_second_countable T2
  is_second_countable (prod_UniformSpace T1 T2).
Proof.
intros [B1 HB1] [B2 HB2]; (topo_basis_Prod B1 B2).
apply topo_basis_Prod_correct; easy.
Qed.

End topo_basis_Facts1.

Section R_UniformSpace_compl.

Complements on R_UniformSpace.

Lemma open_intoo : a b, open (fun xa < x < b).
Proof.
intros a b; apply open_and; [apply open_gt | apply open_lt].
Qed.

Definition Rloc_seq_l : R nat R := fun x nx - / (INR n + 1).
Definition Rloc_seq_r : R nat R := fun x nx + / (INR n + 1).

Lemma Rloc_seq_l_incr :
   x n m, (n m)%nat Rloc_seq_l x n Rloc_seq_l x m.
Proof.
intros x n m Hnm.
apply Rplus_le_compat_l, Ropp_le_contravar, Rinv_le_contravar.
apply INRp1_pos.
auto with real.
Qed.

Lemma Rloc_seq_r_decr :
   x n m, (n m)%nat Rloc_seq_r x m Rloc_seq_r x n.
Proof.
intros x n m Hnm.
apply Rplus_le_compat_l, Rinv_le_contravar.
apply INRp1_pos.
auto with real.
Qed.

Lemma filterlim_Rloc_seq_r :
   x, filterlim (Rloc_seq_r x) eventually (at_right x).
Proof.
intros x.
intros P [alpha H].
unfold Rloc_seq_r.
destruct (nfloor_ex (/ alpha)) as [N [_ HN]].
  apply Rlt_le, Rinv_0_lt_compat, cond_pos.
N; intros n Hn; apply H.
2: replace x with (x + 0) at 1; try now ring_simplify.
2: apply Rplus_lt_compat_l, InvINRp1_pos.
unfold ball; simpl; unfold AbsRing_ball.
replace (x + / (INR n + 1)) with (plus x (/ (INR n + 1))); try easy.
unfold minus; rewrite plus_comm, plus_assoc.
rewrite plus_opp_l, plus_zero_l.
replace (abs (/ (INR n + 1))) with (Rabs (/ (INR n + 1))); try easy.
rewrite Rabs_pos_eq.
2: apply Rlt_le, InvINRp1_pos.
rewrite <- Rinv_inv.
apply Rinv_lt_contravar.
2: apply Rlt_le_trans with (INR N + 1);
    [assumption | now apply Rplus_le_compat_r, le_INR].
apply Rmult_lt_0_compat;
    [apply Rinv_0_lt_compat, cond_pos | apply INRp1_pos].
Qed.

Lemma filterlim_Rloc_seq_l :
   x, filterlim (Rloc_seq_l x) eventually (at_left x).
Proof.
intros x.
pose (x' := - x).
replace x with (- x').
2: unfold x'; apply Ropp_involutive.
unfold Rloc_seq_l.
replace (fun n- x' - / (INR n + 1)) with (fun n- (x' + / (INR n + 1))).
2: apply fun_ext; intros n; now ring_simplify.
apply filterlim_comp with (g := Ropp) (G := at_right x').
apply filterlim_Rloc_seq_r.
apply filterlim_Ropp_right.
Qed.

End R_UniformSpace_compl.

Section Rbar_UniformSpace_compl.

Rbar UniformSpace.

Definition Rbar_ball : Rbar R Rbar Prop :=
  fun x eps yRabs (Rbar_atan y - Rbar_atan x) < eps.

Lemma Rbar_ball_center : x (e : posreal), Rbar_ball x e x.
Proof.
intros x e; unfold Rbar_ball; rewrite Rminus_eq_0, Rabs_R0; apply e.
Qed.

Lemma Rbar_ball_sym : x y (e : R), Rbar_ball x e y Rbar_ball y e x.
Proof.
intros x y e; unfold Rbar_ball; intros H.
replace (Rbar_atan x - Rbar_atan y) with
    (-(Rbar_atan y - Rbar_atan x)) by ring.
now rewrite Rabs_Ropp.
Qed.

Lemma Rbar_ball_triangle :
   x y z (e1 e2 : R),
    Rbar_ball x e1 y Rbar_ball y e2 z Rbar_ball x (e1 + e2) z.
Proof.
unfold Rbar_ball; intros x y z e1 e2 H1 H2.
replace (Rbar_atan z - Rbar_atan x) with
    ((Rbar_atan z - Rbar_atan y) + (Rbar_atan y - Rbar_atan x)) by ring.
apply Rle_lt_trans with (1 := Rabs_triang _ _); lra.
Qed.

Definition Rbar_UniformSpace_mixin :=
  UniformSpace.Mixin Rbar (Finite 0) Rbar_ball Rbar_ball_center Rbar_ball_sym Rbar_ball_triangle.

Canonical Rbar_UniformSpace := UniformSpace.Pack Rbar Rbar_UniformSpace_mixin Rbar.

Lemma open_Rbar_lt : x, open (fun yRbar_lt x y).
Proof.
intros x y Hxy.
assert (H : 0 < Rbar_atan y - Rbar_atan x)
    by now apply Rlt_0_minus, Rbar_atan_monot.
(mkposreal _ H).
intros z; unfold ball; simpl; unfold Rbar_ball, Rabs.
case (Rcase_abs (Rbar_atan z - Rbar_atan y)); intros H1 H2;
    apply Rbar_atan_monot_rev; lra.
Qed.

Lemma open_Rbar_gt : x, open (fun yRbar_gt x y).
Proof.
intros x y Hxy.
assert (H: 0 < (Rbar_atan x - Rbar_atan y))
    by now apply Rlt_0_minus, Rbar_atan_monot.
(mkposreal _ H).
intros z; unfold ball; simpl; unfold Rbar_ball, Rabs.
case (Rcase_abs (Rbar_atan z - Rbar_atan y)); intros H1 H2;
    apply Rbar_atan_monot_rev; lra.
Qed.

Lemma open_Rbar_intoo : a b, open (fun yRbar_lt a y Rbar_lt y b).
Proof.
intros; apply open_and; [apply open_Rbar_lt | apply open_Rbar_gt].
Qed.

Lemma open_Rbar_neq : (x : Rbar), open (fun yy x).
Proof.
intros x; apply open_ext with (fun yRbar_lt y x Rbar_gt y x).
intros y; apply Rbar_dichotomy.
apply open_or; [apply open_Rbar_gt | apply open_Rbar_lt].
Qed.

Lemma closed_Rbar_ge : x, closed (fun yRbar_ge x y).
Proof.
intros x; apply closed_ext with (fun y¬ Rbar_lt x y).
intros y; split; [apply Rbar_not_lt_le | apply Rbar_le_not_lt].
apply closed_not, open_Rbar_lt.
Qed.

Lemma closed_Rbar_le : x, closed (fun yRbar_le x y).
Proof.
intros x; apply closed_ext with (fun y¬ Rbar_gt x y).
intros y; split; [apply Rbar_not_lt_le | apply Rbar_le_not_lt].
apply closed_not, open_Rbar_gt.
Qed.

Lemma closed_Rbar_intcc : a b, closed (fun yRbar_le a y Rbar_le y b).
Proof.
intros; apply closed_and; [apply closed_Rbar_le | apply closed_Rbar_ge].
Qed.

Lemma closed_Rbar_eq : (x : Rbar), closed (fun yy = x).
Proof.
intros x; apply closed_ext with (fun y¬ y x).
intros y; apply Rbar_not_neq_eq.
apply closed_not, open_Rbar_neq.
Qed.

Ltac explicit_finite y Hy0 Hr r Hy :=
  rewrite is_finite_correct in Hy0; destruct Hy0 as [r Hy];
  rewrite Hy; rewrite Hy in Hr; simpl in Hr; clear y Hy.

Lemma open_R_Rbar :
   A, open A open (fun yis_finite y A (real y)).
Proof.
intros A HA y [Hy0 Hr]. explicit_finite y Hy0 Hr r Hy.
destruct (HA r Hr) as [[e He0] He].
unfold ball in He; simpl in He;
    unfold AbsRing_ball, abs, minus, plus, opp in He; simpl in He.
pose (k := Rmax (1 + Rsqr (r + e)) (1 + Rsqr (r - e))).
assert (Hk1 : 1 < k).
  case (Req_dec r e); intros H1; unfold k; [rewrite H1 | ].
  apply Rlt_le_trans with (1 + Rsqr (e + e)); try apply Rmax_l.
  2: apply Rlt_le_trans with (1 + Rsqr (r - e)); try apply Rmax_r.
  1,2: rewrite <- (Rplus_0_r 1) at 1; apply Rplus_lt_compat_l, Rlt_0_sqr; lra.
assert (Hk0 : 0 < k) by (apply Rlt_trans with 1; lra).
pose (f := Rmin (e / k) (Rmin (atan (r + e) - atan r) (atan r - atan (r - e)))).
assert (Hf0 : 0 < f).
  repeat apply Rmin_glb_lt; try (apply Rdiv_lt_0_compat; lra).
  1,2 : apply Rlt_0_minus, atan_increasing; lra.
assert (Hf1 : k × f e).
  rewrite Rmult_comm, Rle_div_r; try apply Rmin_l; easy.
assert (Hf2 : f Rmin (atan (r + e) - atan r) (atan r - atan (r - e))).
  apply Rmin_r.
assert (Hf3 : f atan (r + e) - atan r).
  apply Rle_trans with (1 := Hf2), Rmin_l.
assert (Hf4 : f atan r - atan (r - e)).
  apply Rle_trans with (1 := Hf2), Rmin_r.
(mkposreal f Hf0). unfold ball; simpl; unfold Rbar_ball; simpl.
intros y Ht; apply Rabs_lt_between' in Ht.
assert (Hy0 : is_finite y).
  destruct (atan_bound (r - e)) as [Hr1 _].
  destruct (atan_bound (r + e)) as [_ Hr2].
  case_eq y; try easy; intros Hy; exfalso;
    rewrite Hy in Ht; simpl in Ht; destruct Ht as [Ht1 Ht2]; lra.
split; try easy. explicit_finite y Hy0 Ht t Hy; simpl.
apply He, Rle_lt_trans with (k × Rabs (atan t - atan r)).
apply atan_locally_Lipschitz_rev.
1,2: rewrite Rmin_right, Rmax_left; try (left; apply atan_increasing; lra).
1,2: split.
left; apply Rle_lt_trans with (atan r - f); lra.
left; apply Rlt_le_trans with (atan r + f); lra.
1,2: left; apply atan_increasing; lra.
apply Rlt_le_trans with (k × f); try apply Rmult_lt_compat_l; try easy.
apply Rabs_lt_between'; easy.
Qed.

Lemma open_Rbar_is_finite : open is_finite.
Proof.
pose (full := fun _ : RTrue).
apply open_ext with (fun yis_finite y full y); try (unfold full; tauto).
apply open_R_Rbar, open_true.
Qed.

Lemma open_Rbar_R : B, open B open (fun xB (Finite x)).
Proof.
intros B HB x Hx.
destruct (HB x Hx) as [f Hf]. f. intros t Ht; apply Hf, Rle_lt_trans with (Rabs (t - x)); try easy.
apply atan_Lipschitz.
Qed.

End Rbar_UniformSpace_compl.