Library Lebesgue.topo_bases_R
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
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.
From Requisite Require Import stdlib_wR.
From Coq Require Import Qreals.
From Coquelicot Require Import Coquelicot.
Close Scope R_scope.
From Numbers Require Import countable_sets.
From Subsets Require Import Subsets.
From Lebesgue Require Import Rbar_compl UniformSpace_compl.
Local Open Scope R_scope.
Lemma Q_dense : ∀ a b, a < b → ∃ (l : Q), a < Q2R l < b.
Proof.
intros a b H.
assert (T1:0 < b-a).
apply Rplus_lt_reg_l with a; ring_simplify; exact H.
assert (T2:0 < /(b-a)).
now apply Rinv_0_lt_compat.
pose (q:=up(/(b-a))).
assert (0 < IZR q).
now apply Rlt_trans with (2:=proj1 (archimed _)).
∃ (Qmake (up (a×IZR q)) (Z.to_pos q)).
unfold Q2R; simpl.
rewrite Z2Pos.id.
2: apply lt_IZR; easy.
split.
apply Rmult_lt_reg_r with (IZR q); try assumption.
unfold Rdiv; rewrite Rmult_assoc, Rinv_l.
2: now apply Rgt_not_eq.
rewrite Rmult_1_r.
apply archimed.
apply Rmult_lt_reg_r with (IZR q); try assumption.
unfold Rdiv; rewrite Rmult_assoc, Rinv_l.
2: now apply Rgt_not_eq.
rewrite Rmult_1_r.
apply Rplus_lt_reg_r with (-(a×IZR q)).
apply Rle_lt_trans with (1:=(proj2 (archimed _))).
apply Rlt_le_trans with (IZR q × (b-a));[idtac|right; ring].
apply Rmult_lt_reg_r with (/(b-a)); try assumption.
rewrite Rmult_assoc, Rinv_r.
2: now apply Rgt_not_eq.
rewrite Rmult_1_l, Rmult_1_r.
apply archimed.
Qed.
Lemma Q_dense_Rbar :
∀ (a b : Rbar), Rbar_lt a b →
∃ (l : Q), Rbar_lt a (Q2R l) ∧ Rbar_lt (Q2R l) b.
Proof.
intros a b; case a; case b; clear a b; simpl; try easy.
intros a b; apply Q_dense.
intros r; destruct (Q_dense r (r+1)) as (l,Hl).
auto with real.
intros _; ∃ l; split; try easy.
intros r; destruct (Q_dense (r-1) r) as (l,Hl).
apply Rplus_lt_reg_l with (-r); ring_simplify.
auto with real.
intros _; ∃ l; split; try easy.
intros _; ∃ (Qmake 1 1); split; easy.
Qed.
Section R_second_countable.
Definition bottom_interv : (R → Prop) → R → Rbar :=
fun A x ⇒ Glb_Rbar (fun z ⇒ ∀ y, z < y < x → A y).
Definition top_interv : (R → Prop) → R → Rbar :=
fun A x ⇒ Lub_Rbar (fun z ⇒ ∀ y, x < y < z → A y).
Lemma bottom_interv_le :
∀ (A : R → Prop) (x : R), Rbar_le (bottom_interv A x) x.
Proof.
intros A x.
apply Glb_Rbar_correct.
intros y (H1,H2).
contradict H1; apply Rle_not_lt.
now apply Rlt_le.
Qed.
Lemma top_interv_ge :
∀ (A : R → Prop) (x : R), Rbar_le x (top_interv A x).
Proof.
intros A x.
apply Lub_Rbar_correct.
intros y (H1,H2).
contradict H1; apply Rle_not_lt.
now apply Rlt_le.
Qed.
Lemma charac_connex_inter :
∀ (A : R → Prop) x,
A x → (∀ y : R,
Rbar_lt (bottom_interv A x) y ∧ Rbar_lt y (top_interv A x) →
A y).
Proof.
intros A x H1.
pose (a:= bottom_interv A x).
pose (b:= top_interv A x).
intros y Hy.
case (total_order_T y x); intros Hy2.
destruct Hy2 as [Hy2|Hy2].
case (in_dec A y); try easy; intros Hy3.
absurd (Rbar_lt a y); try apply Hy.
apply Rbar_le_not_lt.
apply Glb_Rbar_correct.
unfold is_lb_Rbar; intros M HM.
case (Rbar_lt_le_dec M y); try easy.
intros K; unfold compl in Hy3; contradict Hy3.
apply HM; easy.
now rewrite Hy2.
case (in_dec A y); try easy; intros Hy3.
absurd (Rbar_lt y b); try apply Hy.
apply Rbar_le_not_lt.
apply Lub_Rbar_correct.
unfold is_ub_Rbar; intros M HM.
case (Rbar_lt_le_dec y M); try easy.
intros K; unfold compl in Hy3; contradict Hy3.
apply HM; easy.
Qed.
Lemma not_A_bottom_interv :
∀ (A : R → Prop) x,
open A → A x → is_finite (bottom_interv A x) →
¬ A (bottom_interv A x).
Proof.
intros A x H1 H2 Ha K.
pose (a:= bottom_interv A x).
destruct (H1 a); try assumption.
absurd (Rbar_lt (a-x0/2) a).
apply Rbar_le_not_lt.
apply Glb_Rbar_correct.
intros y (Hy1,Hy2).
case (Rbar_lt_le_dec a y); intros Hy3.
apply charac_connex_inter with x; try split; try easy.
trans x 2.
apply top_interv_ge.
apply H.
unfold ball; simpl.
unfold AbsRing_ball; simpl.
unfold abs, minus, plus, opp; simpl.
rewrite Rabs_left1.
apply Rplus_lt_reg_l with (y-x0/2).
apply Rle_lt_trans with (a-x0/2).
right; ring.
apply Rlt_le_trans with (1:=Hy1).
apply Rplus_le_reg_l with (-y); ring_simplify.
apply Rle_trans with (x0 × / 2);[idtac|right; field].
apply Rmult_le_pos.
left; apply x0.
left; apply pos_half_prf.
apply Rplus_le_reg_l with a; ring_simplify.
fold a in Ha; rewrite <- Ha in Hy3; apply Hy3.
fold a in Ha; rewrite <- Ha; simpl.
apply Rplus_lt_reg_l with (-a); ring_simplify.
rewrite <- Ropp_0; apply Ropp_lt_contravar.
apply Rmult_lt_0_compat.
apply x0.
apply pos_half_prf.
Qed.
Lemma not_A_top_interv :
∀ (A : R → Prop) x,
open A → A x → is_finite (top_interv A x) →
¬ A (top_interv A x).
Proof.
intros A x H1 H2 Hb K.
pose (b:= top_interv A x); fold b in Hb.
destruct (H1 b); try assumption.
absurd (Rbar_lt b (b+x0/2)).
apply Rbar_le_not_lt.
apply Lub_Rbar_correct.
intros y (Hy1,Hy2).
case (Rbar_lt_le_dec y b); intros Hy3.
apply charac_connex_inter with x; try split; try easy.
trans x 1.
apply bottom_interv_le.
apply H.
unfold ball; simpl.
unfold AbsRing_ball; simpl.
unfold abs, minus, plus, opp; simpl.
rewrite Rabs_right.
apply Rplus_lt_reg_l with (b).
apply Rle_lt_trans with (y).
right; ring.
apply Rlt_le_trans with (1:=Hy2).
apply Rplus_le_reg_l with (-b-x0/2); ring_simplify.
apply Rle_trans with (x0 × / 2);[idtac|right; field].
apply Rmult_le_pos.
left; apply x0.
left; apply pos_half_prf.
apply Rle_ge; apply Rplus_le_reg_l with b; ring_simplify.
rewrite <- Hb in Hy3; easy.
rewrite <- Hb; simpl.
apply Rplus_lt_reg_l with (-b); ring_simplify.
apply Rmult_lt_0_compat.
apply x0.
apply pos_half_prf.
Qed.
Lemma bottom_interv_lt :
∀ (A : R → Prop) x, open A → A x → Rbar_lt (bottom_interv A x) x.
Proof.
intros A x HA Hx.
case (Rbar_le_lt_or_eq_dec _ _ (bottom_interv_le A x));[easy|idtac].
intros H.
absurd (A x); try easy.
replace x with (real (bottom_interv A x)).
apply not_A_bottom_interv; try easy.
rewrite H; easy.
rewrite H; easy.
Qed.
Lemma top_interv_gt :
∀ (A : R → Prop) x, open A → A x → Rbar_lt x (top_interv A x).
Proof.
intros A x HA Hx.
case (Rbar_le_lt_or_eq_dec _ _ (top_interv_ge A x));[easy|idtac].
intros H.
absurd (A x); try easy.
replace x with (real (top_interv A x)).
apply not_A_top_interv; try easy.
rewrite <- H; easy.
rewrite <- H; easy.
Qed.
Lemma bottom_interv_eq :
∀ (A : R → Prop) (x y : R),
open A → A x →
Rbar_lt (bottom_interv A x) y → Rbar_lt y (top_interv A x) →
bottom_interv A y = bottom_interv A x.
Proof.
intros A x y HA Hx H1 H2.
assert (Hy: A y).
apply charac_connex_inter with x; try split; try easy.
case (Rbar_total_order (bottom_interv A y) (bottom_interv A x)); intros H.
destruct H as [H|H]; try easy.
assert (Hx2: is_finite (bottom_interv A x)).
destruct (bottom_interv A x); try easy.
contradict H; apply Rbar_le_not_lt; easy.
absurd (A (bottom_interv A x)).
apply not_A_bottom_interv; assumption.
apply charac_connex_inter with y; try split; try easy.
rewrite Hx2; easy.
rewrite Hx2; trans y 2.
apply top_interv_ge.
assert (Hy2: is_finite (bottom_interv A y)).
generalize (bottom_interv_le A y); intros K.
destruct (bottom_interv A y); try easy.
contradict H; apply Rbar_le_not_lt; easy.
absurd (A (bottom_interv A y)).
apply not_A_bottom_interv; try assumption.
apply charac_connex_inter with x; try split; try easy.
rewrite Hy2; easy.
rewrite Hy2; trans y 1.
apply bottom_interv_le.
Qed.
Lemma top_interv_eq :
∀ (A : R → Prop) (x y : R),
open A → A x →
Rbar_lt (bottom_interv A x) y → Rbar_lt y (top_interv A x) →
top_interv A y = top_interv A x.
Proof.
intros A x y HA Hx H1 H2.
assert (Hy: A y).
apply charac_connex_inter with x; try split; try easy.
case (Rbar_total_order (top_interv A y) (top_interv A x)); intros H.
destruct H as [H|H]; try easy.
assert (Hy2: is_finite (top_interv A y)).
generalize (top_interv_ge A y); intros K.
destruct (top_interv A y); try easy.
absurd (A (top_interv A y)).
apply not_A_top_interv; assumption.
apply charac_connex_inter with x; try split; try easy.
rewrite Hy2; trans y 2.
apply top_interv_ge.
rewrite Hy2; easy.
assert (Hx2: is_finite (top_interv A x)).
generalize (top_interv_ge A x); intros K.
destruct (top_interv A x); try easy.
absurd (A (top_interv A x)).
apply not_A_top_interv; try assumption.
apply charac_connex_inter with y; try split; try easy.
2:rewrite Hx2; easy.
rewrite Hx2; trans y 1.
apply bottom_interv_le.
Qed.
Lemma open_R_charac_Q :
∀ (A : R → Prop),
open A →
∀ x, A x ↔
(∃ q : Q, let y := Q2R q in
A y ∧
Rbar_lt (bottom_interv A y) x ∧
Rbar_lt x (top_interv A y)).
Proof.
intros A HA x; split.
intros Hx.
destruct (HA x Hx) as (eps,Heps).
destruct (Q_dense x (x+eps/2)) as (q,H1).
apply Rplus_lt_reg_l with (-x); ring_simplify.
apply Rmult_lt_0_compat.
apply eps.
apply pos_half_prf.
∃ q; intros y.
assert (A y).
apply Heps.
unfold ball; simpl.
unfold AbsRing_ball; simpl.
unfold abs, minus, plus, opp; simpl.
rewrite Rabs_right.
apply Rlt_le_trans with ((x+eps/2)+-x).
apply Rplus_lt_compat_r, H1.
apply Rplus_le_reg_l with (- (eps/2)); ring_simplify.
apply Rle_trans with (eps/2);[left|right; field].
apply Rmult_lt_0_compat.
apply eps.
apply pos_half_prf.
apply Rle_ge, Rplus_le_reg_l with x; ring_simplify; now left.
split; try assumption.
assert (Rbar_lt (bottom_interv A x) y).
trans x.
apply bottom_interv_lt; easy.
assert (Rbar_lt y (top_interv A x)).
assert (J:Rbar_le y (top_interv A x)).
apply Lub_Rbar_correct.
intros z Hz.
apply Heps.
unfold ball; simpl.
unfold AbsRing_ball; simpl.
unfold abs, minus, plus, opp; simpl.
rewrite Rabs_right.
apply Rle_lt_trans with (y+-x).
apply Rplus_le_compat_r; now left.
apply Rlt_le_trans with ((x+eps/2)+-x).
apply Rplus_lt_compat_r, H1.
apply Rplus_le_reg_l with (- (eps/2)); ring_simplify.
apply Rle_trans with (eps/2);[left|right; field].
apply Rmult_lt_0_compat.
apply eps.
apply pos_half_prf.
apply Rle_ge, Rplus_le_reg_l with x; ring_simplify; now left.
case (Rbar_le_lt_or_eq_dec _ _ J); try easy.
intros K.
absurd (A y); try easy.
replace y with (real (Finite y)) by easy; rewrite K.
apply not_A_top_interv; try easy.
rewrite <- K; easy.
split.
rewrite bottom_interv_eq with A x y; try assumption.
apply bottom_interv_lt; easy.
rewrite top_interv_eq with A x y; try assumption.
apply top_interv_gt; easy.
intros (p,(q, (H1,H2))).
apply charac_connex_inter with (Q2R p); try easy.
Qed.
Definition open_R_charac_list : (R → Prop) → nat → Rbar → Prop :=
fun A n x ⇒ let y := Q2R (bij_NQ n) in
A y ∧
Rbar_lt (bottom_interv A y) x ∧
Rbar_lt x (top_interv A y).
Lemma open_R_charac_list_correct :
∀ A, open A →
(∀ x, A x ↔ ∃ n, open_R_charac_list A n x).
Proof.
intros A HA x.
eapply iff_trans.
apply open_R_charac_Q; try easy.
unfold open_R_charac_list.
split.
intros (q,(H1,H2)).
∃ (bij_QN q).
rewrite bij_NQN; easy.
intros (n,Hn).
∃ (bij_NQ n); easy.
Qed.
Definition topo_basis_R : nat → R → Prop :=
fun n x ⇒ Q2R (fst (bij_NQ2 n)) < x < Q2R (snd (bij_NQ2 n)).
Lemma topo_basis_R_open : ∀ n, open (topo_basis_R n).
Proof.
intros; apply open_intoo.
Qed.
Lemma R_second_countable_aux1 :
∀ (A : R → Prop) a b (y : R),
(∀ (x : R), Rbar_lt a x ∧ Rbar_lt x b → A x) →
Rbar_lt a y ∧ Rbar_lt y b →
∃ (q1 q2 : Q),
(∀ x, Q2R q1 < x < Q2R q2 → A x) ∧
(Q2R q1 < y < Q2R q2).
Proof.
intros A a b y H1 (H2,H3).
destruct (Q_dense_Rbar _ _ H2) as (q1,Hq1).
destruct (Q_dense_Rbar _ _ H3) as (q2,Hq2).
∃ q1; ∃ q2; split.
intros x Hx; apply H1; split.
apply Rbar_lt_trans with (Q2R q1); easy. trans (Q2R q2).
simpl in Hq1; simpl in Hq2; easy.
Qed.
Lemma R_second_countable_aux2 :
∀ A, open A →
∃ P : nat → Prop,
(∀ x, A x ↔ ∃ n, P n ∧ topo_basis_R n x).
Proof.
intros A HA.
∃ (fun n ⇒ ∀ x, topo_basis_R n x → A x).
intros x; split.
intros Hx.
destruct (open_R_charac_Q A HA x) as (Y1,Y2).
destruct (Y1 Hx) as (q,H).
pose (y:=Q2R q).
destruct (R_second_countable_aux1 A (bottom_interv A y)
(top_interv A y) x) as (q1,(q2,H1)).
intros t Ht; apply charac_connex_inter with y; try apply H.
apply Ht.
apply H.
∃ (bij_Q2N (q1,q2)).
split; unfold topo_basis_R.
rewrite bij_NQ2N; easy.
rewrite bij_NQ2N.
apply H1.
intros (n,(H1,H2)).
apply H1; easy.
Qed.
Lemma R_second_countable : is_topo_basis topo_basis_R.
Proof.
split.
apply topo_basis_R_open.
intros A HA; destruct (R_second_countable_aux2 A HA) as [P HP]; now ∃ P.
Qed.
Lemma R_second_countable_ex : is_second_countable R_UniformSpace.
Proof.
∃ topo_basis_R; apply R_second_countable.
Qed.
Definition R2_UniformSpace := prod_UniformSpace R_UniformSpace R_UniformSpace.
Definition topo_basis_R2 : nat → R × R → Prop :=
topo_basis_Prod topo_basis_R topo_basis_R.
Lemma R2_second_countable : is_topo_basis topo_basis_R2.
Proof.
apply topo_basis_Prod_correct; apply R_second_countable.
Qed.
Lemma R2_second_countable_ex : is_second_countable R2_UniformSpace.
Proof.
∃ topo_basis_R2; apply R2_second_countable.
Qed.
End R_second_countable.