Library Lebesgue.Bochner.topology_compl

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Leclerc
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 ssreflect Utf8.

From Coquelicot Require Import Coquelicot.

From Numbers Require Import countable_sets.
From Lebesgue Require Import Rbar_compl.

Require Import hierarchy_notations.

Open Scope R_scope.
Open Scope hy_scope.

Section open_subspaces.

    Context {S : UniformSpace}.

    Lemma open_union {I : Type} :
         U : I (S Prop), ( i : I, open (U i))
             open (fun x i : I, U i x).
    Proof.
        moveU HU x.
        casei Uix.
        case: (HU i x).
            exact Uix.
        move ⇒ ɛ Hɛ.
         ɛ ⇒ y Bxɛy.
         i; apply Hɛ ⇒ //.
    Qed.

    Context {A : AbsRing}.
    Context {E : NormedModule A}.
    Open Scope hy_scope.

    Lemma NM_open_ball_norm : (a : E) (ɛ : R), 0 < ɛ open (ball_norm a ɛ).
    Proof.
        movea ɛ Hɛ; unfold openx Hx.
        suff: locally_norm x (ball_norm a ɛ)
            by apply locally_le_locally_norm.
        unfold locally_norm, ball_norm in Hx |- ×.
        pose η := ɛ - (norm (minus x a)).
        assert (0 < η); unfold η.
        apply Rgt_lt, (Rgt_minus ɛ (norm (minus x a))) ⇒ //.
        pose sigη := mkposreal η H.
         sigηy /= .
        apply Rle_lt_trans with (norm (minus y x) + (norm (minus x a))).
        replace (minus y a) with (minus y x + minus x a)
            by rewrite <-(minus_trans x) ⇒ //.
        apply norm_triangle.
        clear sigη; clear H.
        replace ɛ with ((ɛ - minus x a ) + minus x a ) at 1.
        unfold plus ⇒ /=.
        apply (Rplus_lt_compat_r ( minus x a ) ( minus y x ) (ɛ - ( minus x a ))).
        unfold η in .
        unfold plus ⇒ //.
        setoid_rewrite Rplus_assoc.
        rewrite Rplus_opp_l; apply Rplus_ne.
    Qed.

    Lemma NM_open_neq : x : E,
        open (fun yy x).
    Proof.
        movex y Neqxy.
        assert (0 < minus x y ) as Hdxy.
            apply norm_gt_0.
            unfold minus.
            moveAbs.
            apply Neqxy.
            apply plus_reg_r with (opp y).
            rewrite plus_opp_r Abs ⇒ //.
        suff: (locally_norm y (λ y0 : E, y0 x)).
            apply locally_le_locally_norm.
         (RIneq.mkposreal _ Hdxy) ⇒ z /= By.
        moveAbs.
        rewrite Abs in By.
        unfold ball_norm in By.
        apply: Rlt_irrefl.
        exact By.
    Qed.

End open_subspaces.

Section closed_subspaces.

    Context {S : UniformSpace}.

    Lemma closed_inter {I : Type} :
         F : I (S Prop), ( i : I, closed (F i))
             closed (fun x i : I, F i x).
    Proof.
        moveF HF.
        movex NHx i.
        unfold closed in HF.
        pose HFix := HF i x; clearbody HFix.
        apply HFix.
        moveH.
        apply NHx.
        unfold locally.
        unfold locally in H; case: H ⇒ ɛ Hɛ.
         ɛ ⇒ y /Hɛ ⇒ Abs.
        moveH'.
        apply Abs ⇒ //.
    Qed.

End closed_subspaces.

Section density.

    Context {S : UniformSpace}.

    Definition fun_dense (P : S Prop) (Q : S Prop) (f : x : S, Q x posreal S) : Prop :=
        ( x : S, P x Q x)
        ( x : S, π : Q x,
             ɛ : posreal, ball x ɛ (f x π ɛ) P (f x π ɛ)).

    Definition dense (P : S Prop) (Q : S Prop) : Prop :=
         f, fun_dense P Q f.

    Lemma fun_dense_dense {P Q : S Prop} {f : x : S, Q x posreal S} :
        fun_dense P Q f dense P Q.
    Proof.
         f ⇒ //.
    Qed.

    Definition fun_separable (u : nat S) (P : S Prop) (f : x : S, P x posreal nat) : Prop :=
        ( n : nat, P (u n))
        ( x : S, π : P x,
             ɛ : posreal, ball x ɛ (u (f x π ɛ))).

    Definition separable (P : S Prop) : Prop :=
         u : nat S, ( n : nat, P (u n)) x : S, P x
             ɛ : posreal, n : nat, ball x ɛ (u n).

    Lemma fun_separable_separable {u : nat S} {P : S Prop} {f : ( x : S, P x posreal nat)} :
        fun_separable u P f separable P.
    Proof.
        move ⇒ [H1 H2].
         u; split ⇒ //.
        movex Px ɛ.
         (f x Px ɛ); apply H2.
    Qed.

    Definition seq_separable (u : nat S) (P : S Prop) : Prop :=
        ( n : nat, P (u n))
        ( x : S, P x
             ɛ : posreal, n : nat, ball x ɛ (u n)).

    Lemma fun_separble_seq_separable {u : nat S} {P : S Prop} {f} :
        fun_separable u P f seq_separable u P.
    Proof.
        move ⇒ [H1 H2].
        split ⇒ //.
        movex Px ɛ.
         (f x Px ɛ) ⇒ //.
    Qed.

End density.

Section denseQR.

    Definition QinR (x : R) :=
         r : Q, x = Q2R r.

    Definition denseQR_fn : x : R_UniformSpace, True posreal R_UniformSpace :=
        fun x _ sigɛQ2R
            match sigɛ with mkposreal ɛ _
                let q := up (/ɛ) in
                (Qmake (up (x×IZR q)) (Z.to_pos q))
            end.

    Theorem fun_denseQR : fun_dense QinR (fun _ : R_UniformSpaceTrue) denseQR_fn.
    Proof.
        split; [easy | unfold denseQR_fn; movex _Hɛ]; split; swap 1 2].
        unfold QinR; ((up (x × IZR (up (/ ɛ))) # Z.to_pos (up (/ ɛ)))) ⇒ //.
        unfold ball ⇒ /=; unfold AbsRing_ball.
        pose a := x;
        pose b := (x + ɛ)%R;
        assert= b - a)%R as Eqɛ.
            unfold a, b;
            unfold Rminus;
            rewrite Rplus_assoc;
            replace+ - x)%R with- x)%R by unfold Rminus ⇒ //;
            rewrite Rplus_minus ⇒ //.
        fold a.
        pose q := up (/ɛ).
        rewrite Eqɛ in q.
        rewrite Eqɛ; fold q.
        assert (a < b)%R.
            unfold a, b.
            replace x with (x + 0)%R at 1
                by apply Rplus_ne.
            apply Rplus_lt_compat_l ⇒ //.
        unfold abs ⇒ /=.
        apply Raux.Rabs_lt.
        suff: (a < (Q2R (up (a × IZR q) # Z.to_pos q)) < b).
            caseH1 H2; split.
            rewrite Ropp_minus_distr.
            unfold minus ⇒ /=; unfold plus ⇒ /=; unfold opp ⇒ /=.
            lra.
            unfold minus, plus, opp ⇒ /=.
            lra.
        assert (0 < b-a)%R as T1.
        rewrite <-Eqɛ ⇒ //.
        assert (0 < /(b-a))%R as T2.
        now apply Rinv_0_lt_compat.
        assert (0 < IZR q)%R.
        now apply Rlt_trans with (2:=proj1 (archimed _)).
        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))%R.
        apply Rle_lt_trans with (1:=(proj2 (archimed _))).
        apply Rlt_le_trans with (IZR q × (b-a))%R;[idtac|right; ring].
        apply Rmult_lt_reg_r with (/(b-a))%R; try assumption.
        rewrite Rmult_assoc Rinv_r.
        2: now apply Rgt_not_eq.
        rewrite Rmult_1_l Rmult_1_r.
        apply archimed.
    Qed.

    Definition separableR_fn : x : R_UniformSpace, True posreal nat :=
        fun x π sigɛbij_QN
            match sigɛ with mkposreal ɛ _
                let q := up (/ɛ) in
                (Qmake (up (x×IZR q)) (Z.to_pos q))
            end.

    Theorem fun_separableR : fun_separable (fun nQ2R (bij_NQ n)) (fun _True) separableR_fn.
    Proof.
        split ⇒ //.
        unfold separableR_fnx _ ɛ.
        case: fun_denseQR ⇒ [_ H].
        case: (H x I ɛ) ⇒ [{}H _].
        unfold denseQR_fn in H.
        rewrite bij_NQN ⇒ //.
    Qed.

    Theorem separableR : separable (fun _ : R_UniformSpaceTrue).
    Proof.
        exact (fun_separable_separable fun_separableR).
    Qed.

    Theorem seq_separableR : seq_separable (fun nQ2R (bij_NQ n)) (fun _ : R_UniformSpaceTrue).
    Proof.
        exact (fun_separble_seq_separable fun_separableR).
    Qed.

End denseQR.

Section NM_density.

    Context {A : AbsRing}.
    Context {E : NormedModule A}.

    Definition NM_separable (P : E Prop) : Prop :=
         u : nat E, x : E, P x
             ɛ : posreal, n : nat, ball_norm x ɛ (u n).

    Lemma separable_NM_separable :
         P : E Prop, separable P NM_separable P.
    Proof.
        moveP; unfold separable.
        caseu [Hu1 Hu2].
         ux /Hu2.
        pose Hloc := locally_ball_norm; clearbody Hloc.
        unfold locally_norm, ball_norm in Hloc.
        moveHux ɛ.
        case: (Hloc A E x ɛ) ⇒ ɛ' Hɛ'; clear Hloc.
        case: (Hux ɛ') ⇒ k /Hɛ' Hprox.
         k ⇒ //.
    Qed.

    Definition NM_seq_separable (u : nat E) (P : E Prop) : Prop :=
        ( n : nat, P (u n))
        ( x : E, P x
             ɛ : posreal, n : nat, ball_norm x ɛ (u n)).

    Lemma seq_separable_NM_seq_separable {u : nat E} {P : E Prop} :
        seq_separable u P NM_seq_separable u P.
    Proof.
        unfold separable.
        case ⇒ [Hu1 Hu2].
        split ⇒ //.
        movex /Hu2.
        pose Hloc := locally_ball_norm; clearbody Hloc.
        unfold locally_norm, ball_norm in Hloc.
        moveHux ɛ.
        case: (Hloc A E x ɛ) ⇒ ɛ' Hɛ'; clear Hloc.
        case: (Hux ɛ') ⇒ k /Hɛ' Hprox.
         k ⇒ //.
    Qed.

    Definition dist (x : E) (P : E Prop) :=
        (Glb_Rbar (fun d : R y : E, P y minus x y = d)).

    Definition NM_seq_separable_weak (u : nat E) (P : E Prop) : Prop :=
        ( x : E, P x
             ɛ : posreal, n : nat, ball_norm x ɛ (u n)).

    Lemma NM_seq_separable_seq_separable_weak {u : nat E} {P : E Prop} :
        NM_seq_separable u P NM_seq_separable_weak u P.
    Proof.
        move ⇒ [_ H2] //.
    Qed.

    Lemma NM_seq_separable_weak_le {u : nat E} {P : E Prop} :
         Q : E Prop,
            ( x : E, Q x P x)
            NM_seq_separable_weak u P
            NM_seq_separable_weak u Q.
    Proof.
        moveQ LeQP H x /LeQP/H//.
    Qed.

End NM_density.

Section NM_seq_separable_subspace.


End NM_seq_separable_subspace.

Lemma NM_separableR : NM_separable (fun _ : R_NormedModuleTrue).
Proof.
    apply separable_NM_separable.
    apply separableR.
Qed.

Lemma NM_seq_separableR : NM_seq_separable (fun nQ2R (bij_NQ n)) (fun _ : R_NormedModuleTrue).
Proof.
    apply seq_separable_NM_seq_separable.
    apply seq_separableR.
Qed.

Lemma NM_seq_separable_weakR : NM_seq_separable_weak (fun nQ2R (bij_NQ n)) (fun _ : R_NormedModuleTrue).
Proof.
    apply NM_seq_separable_seq_separable_weak.
    apply NM_seq_separableR.
Qed.