Library Top.check_sub_structure

This file is part of the Elfic 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.

Require Export Reals Coquelicot.Coquelicot.
Require Export compatible hilbert.
Require Export ProofIrrelevance.


Section Subgroups.

Context {G : AbelianGroup}.
Context {P: G Prop}.
Hypothesis CP: compatible_g P.

Record Sg:= mk_Sg {
    val :> G ;
    H: P val

Lemma Sg_eq: (x y:Sg), (val x = val y) x = y.

Definition Sg_zero : Sg := mk_Sg zero (compatible_g_zero P CP).

Definition Sg_plus (x y : Sg) : Sg :=
    mk_Sg (plus x y)
          (compatible_g_plus P (val x) (val y) CP (H x) (H y)).

Definition Sg_opp (x : Sg) : Sg :=
    mk_Sg (opp x)
          (compatible_g_opp P (val x) CP (H x)).

Lemma Sg_plus_comm: (x y:Sg), Sg_plus x y = Sg_plus y x.

Lemma Sg_plus_assoc:
   (x y z:Sg ), Sg_plus x (Sg_plus y z) = Sg_plus (Sg_plus x y) z.

Lemma Sg_plus_zero_r: x:Sg, Sg_plus x Sg_zero = x.

Lemma Sg_plus_opp_r: x:Sg, Sg_plus x (Sg_opp x) = Sg_zero.

Definition Sg_AbelianGroup_mixin :=
  AbelianGroup.Mixin Sg Sg_plus Sg_opp Sg_zero Sg_plus_comm
   Sg_plus_assoc Sg_plus_zero_r Sg_plus_opp_r.

Canonical Sg_AbelianGroup :=
  AbelianGroup.Pack Sg (Sg_AbelianGroup_mixin) Sg.

End Subgroups.


Section Submodules.

Context {G : ModuleSpace R_Ring}.
Context {P: G Prop}.

Hypothesis CPM: compatible_m P.

Let Sg_plus := (@Sg_plus _ P (proj1 CPM)).

Definition Sg_scal a (x: Sg) : (Sg):=
    mk_Sg (scal a (val x))
          (compatible_m_scal P a (val x) CPM (H x)).

Lemma Sg_mult_one_l : (x : Sg), Sg_scal (@one R_Ring) x = x.

Lemma Sg_mult_assoc : x y (f: Sg), Sg_scal x (Sg_scal y f) = Sg_scal (mult x y) f.

Lemma Sg_mult_distr_l : x (u v: Sg),
  Sg_scal x (Sg_plus u v) = Sg_plus (Sg_scal x u) (Sg_scal x v).

Lemma Sg_mult_distr_r : x y u,
  Sg_scal (plus x y) u = Sg_plus (Sg_scal x u) (Sg_scal y u).

Definition Sg_ModuleSpace_mixin :=
ModuleSpace.Mixin R_Ring (@Sg_AbelianGroup G P (proj1 CPM))
   _ Sg_mult_assoc Sg_mult_one_l Sg_mult_distr_l Sg_mult_distr_r.

Canonical Sg_ModuleSpace :=
  ModuleSpace.Pack R_Ring Sg (ModuleSpace.Class _ _ _ Sg_ModuleSpace_mixin) (@Sg G P).

End Submodules.


Section Subprehilbert.

Context {G : PreHilbert}.
Context {P: G Prop}.
Hypothesis CPM: compatible_m P.

Let Sg_plus := (@Sg_plus _ P (proj1 CPM)).
Let Sg_scal := (@Sg_scal _ P CPM).

Definition Sg_inner (x y : @Sg G P) : R :=
     (inner (val x) (val y)).

Lemma Sg_inner_comm : (x y : Sg),
        Sg_inner x y = Sg_inner y x.

Lemma Sg_inner_pos : (x : Sg),
        0 Sg_inner x x.

Lemma Sg_inner_def : (x : Sg),
                           Sg_inner x x= 0 x = @Sg_zero G P (proj1 CPM).

Lemma Sg_inner_scal : (x y: Sg) (l : R),
        Sg_inner (Sg_scal l x) y = l × (Sg_inner x y).

Lemma Sg_inner_plus : (x y z: Sg),
     Sg_inner (Sg_plus x y) z = plus (Sg_inner x z) (Sg_inner y z).

Definition Sg_PreHilbert_mixin :=
   PreHilbert.Mixin (@Sg_ModuleSpace G P CPM)
       _ Sg_inner_comm Sg_inner_pos Sg_inner_def Sg_inner_scal Sg_inner_plus.

Canonical Sg_PreHilbert :=
    PreHilbert.Pack Sg (PreHilbert.Class _ _ Sg_PreHilbert_mixin) (@Sg G P).

End Subprehilbert.


Section Subhilbert.

Context {G : Hilbert}.
Context {P: G Prop}.

Hypothesis CPM: compatible_m P.

Let Sg_plus := (@Sg_plus _ P (proj1 CPM)).
Let Sg_scal := (@Sg_scal _ P CPM).

Definition Sg_cleanFilter (Fi : (Sg Prop) Prop) : (G Prop) Prop
    := fun A : ((G Prop)) ⇒ V : (Sg Prop), Fi V
           ( f : (@Sg G P), V f A (val f)).

Lemma Sg_cleanFilterProper: (Fi: (Sg Prop) Prop),
  ProperFilter Fi ProperFilter (Sg_cleanFilter Fi).

Definition Sg_lim_v (Fi : (Sg Prop) Prop) :=
    lim (Sg_cleanFilter Fi).

End Subhilbert.