Library Top.hilbert

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 linear_map.
Require Export R_compl.
Require Import mathcomp.ssreflect.ssreflect.
Require Import Decidable.
Require Export logic_tricks.

Complete subsets

Section CompleteSubset.

Context {E : NormedModule R_AbsRing}.

Definition complete_subset (phi:EProp) :=
   (lime : ((E Prop) Prop) E),
  ( F, ProperFilter F cauchy F
     ( P, F P ~~( x, P x phi x))
          phi (lime F)
           eps : posreal, F (ball (lime F) eps)).

End CompleteSubset.

PreHilbert spaces


Module PreHilbert.

Record mixin_of (E : ModuleSpace R_Ring) := Mixin {
  inner : E E R ;
  ax1 : (x y : E), inner x y = inner y x ;
  ax2 : (x : E), 0 inner x x ;
  ax3 : (x : E), inner x x = 0 x = zero ;
  ax4 : (x y : E) (l:R), inner (scal l x) y = l × inner x y ;
  ax5 : (x y z : E), inner (plus x y) z = inner x z + inner y z
}.

Section ClassDef.

Record class_of (T : Type) := Class {
  base : ModuleSpace.class_of R_Ring T ;
  mixin : mixin_of (ModuleSpace.Pack R_Ring T base T)
}.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition ModuleSpace := ModuleSpace.Pack _ cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> ModuleSpace.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion ModuleSpace : type >-> ModuleSpace.type.
Canonical ModuleSpace.

Notation PreHilbert := type.

End Exports.

End PreHilbert.

Export PreHilbert.Exports.

Section AboutPreHilbert.

Context {E : PreHilbert}.

Definition inner : E E R := PreHilbert.inner _ (PreHilbert.class E).

Definition Hnorm x := sqrt (inner x x).

Lemma inner_is_bilinear_form: is_bilinear_mapping inner.

Lemma inner_sym: x y, inner x y = inner y x.

Lemma inner_ge_0: x, 0 inner x x.

Lemma inner_eq_0 : x, inner x x = 0 x = zero.

Lemma norm_ge_0: x, 0 Hnorm x.

Lemma norm_eq_0: x, Hnorm x = 0 x = zero.

Lemma inner_scal_l: (x y :E) (l:R), inner (scal l x) y = l × inner x y.

Lemma inner_scal_r: (x y :E) (l:R), inner x (scal l y) = l × inner x y.

Lemma inner_zero_l: x, inner zero x = 0.

Lemma inner_zero_r: x, inner x zero = 0.

Lemma inner_plus_l : (x y z : E), inner (plus x y) z = inner x z + inner y z.

Lemma inner_plus_r : (x y z : E), inner x (plus y z) = inner x y + inner x z.

Lemma inner_opp_r: (x y : E), inner x (opp y) = - inner x y.

Lemma inner_opp_l: (x y : E), inner (opp x) y = - inner x y.

Lemma norm_zero: Hnorm zero = 0.

Lemma norm_opp: x, Hnorm (opp x) = Hnorm x.

Lemma norm_scal : l x, Hnorm (scal l x) = Rabs l × Hnorm x.

Lemma squared_norm: x, Hnorm x × Hnorm x = inner x x.

Lemma square_expansion_plus: x y,
  inner (plus x y) (plus x y) = inner x x + 2 × inner x y + inner y y.

Lemma square_expansion_minus: x y,
  inner (minus x y) (minus x y) = inner x x - 2 × inner x y + inner y y.

Equalities and inequalities

Lemma parallelogram_id: x y,
  (inner (plus x y) (plus x y)) + (inner (minus x y) (minus x y))
  = 2*((inner x x) + (inner y y)).

Lemma Cauchy_Schwartz: x y,
   Rsqr (inner x y) inner x x × inner y y.

Lemma Cauchy_Schwartz_with_norm: x y,
   Rabs (inner x y) Hnorm x × Hnorm y.

Lemma norm_triangle: x y, Hnorm (plus x y) Hnorm x + Hnorm y.

End AboutPreHilbert.

PreHilbert is NormedModule

Section PreHNormedModule.

Context {E : PreHilbert}.

Definition ball := fun (x:E) eps yHnorm (minus x y) < eps.

Lemma ball_center :
   (x : E) (e : posreal),
  ball x e x.

Lemma ball_sym :
   (x y : E) (e : R),
  ball x e y ball y e x.

Lemma ball_triangle :
   (x y z : E) (e1 e2 : R),
  ball x e1 y ball y e2 z ball x (e1 + e2) z.

Definition PreHilbert_UniformSpace_mixin :=
  UniformSpace.Mixin E ball ball_center ball_sym ball_triangle.

Canonical PreHilbert_UniformSpace :=
  UniformSpace.Pack E (PreHilbert_UniformSpace_mixin) E.

Canonical PreHilbert_NormedModuleAux :=
  NormedModuleAux.Pack R_AbsRing E
   (NormedModuleAux.Class R_AbsRing E
     (ModuleSpace.class _ (PreHilbert.ModuleSpace E))
        PreHilbert_UniformSpace_mixin) E.

Lemma norm_ball1 : (x y : E) (eps : R),
          Hnorm (minus y x) < eps Hierarchy.ball x eps y.

Lemma norm_ball2: (x y : E) (eps : posreal),
          Hierarchy.ball x eps y Hnorm (minus y x) < 1 × eps.

Lemma norm_scal_aux:
  ( (l : R) (x : E), Hnorm (scal l x) abs l × Hnorm x).

Definition PreHilbert_NormedModule_mixin :=
  NormedModule.Mixin R_AbsRing _
   Hnorm 1%R norm_triangle norm_scal_aux norm_ball1 norm_ball2 norm_eq_0.

Canonical PreHilbert_NormedModule :=
  NormedModule.Pack R_AbsRing E
     (NormedModule.Class _ _ _ PreHilbert_NormedModule_mixin) E.

End PreHNormedModule.

Hilbert spaces


Module Hilbert.

Record mixin_of (E : PreHilbert) := Mixin {
  lim : ((E Prop) Prop) E ;
  ax1 : F, ProperFilter F cauchy F
           eps : posreal, F (ball (lim F) eps)
}.

Section ClassDef.

Record class_of (T : Type) := Class {
  base : PreHilbert.class_of T ;
  mixin : mixin_of (PreHilbert.Pack T base T)
}.


Structure type := Pack { sort; _ : class_of sort ; _ : Type }.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition ModuleSpace := ModuleSpace.Pack _ cT xclass xT.
Definition PreHilbert := PreHilbert.Pack cT xclass xT.
End ClassDef.

Module Exports.

Coercion base : class_of >-> PreHilbert.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion ModuleSpace : type >-> ModuleSpace.type.
Canonical ModuleSpace.
Coercion PreHilbert : type >-> PreHilbert.type.
Canonical PreHilbert.

Notation Hilbert := type.

End Exports.

End Hilbert.

Export Hilbert.Exports.

Canonical Hilbert_UniformSpace (E : Hilbert) :=
  UniformSpace.Pack E (PreHilbert_UniformSpace_mixin) E.

Canonical Hilbert_NormedModule (E : Hilbert) :=
  NormedModule.Pack R_AbsRing E
     (NormedModule.Class _ _ _ PreHilbert_NormedModule_mixin) E.

Coercion Hilbert_NormedModule: Hilbert >-> NormedModule.

Hilbert is a CompleteScape

Section Hilbert_aux.

Context {E : Hilbert}.

Definition lim : ((E Prop) Prop) E :=
   Hilbert.lim _ (Hilbert.class E).

Lemma Hilbert_complete:
    (F:(EProp)->Prop), ProperFilter F
        cauchy F
           eps : posreal, F (ball (lim F) eps).

Definition Hilbert_CompleteSpace_mixin :=
  CompleteSpace.Mixin PreHilbert_UniformSpace lim Hilbert_complete.

Canonical Hilbert_CompleteSpace :=
  CompleteSpace.Pack E (CompleteSpace.Class _ _ Hilbert_CompleteSpace_mixin) E.

Canonical Hilbert_CompleteNormedModule :=
  CompleteNormedModule.Pack R_AbsRing E
    (CompleteNormedModule.Class R_AbsRing E
       (NormedModule.class _ PreHilbert_NormedModule)
        Hilbert_CompleteSpace_mixin) E.

End Hilbert_aux.

Convexity

Section Convex.

Context {E : ModuleSpace R_Ring}.

Definition convex (phi:E Prop) :=
    (u v:E) (theta:R), phi u phi v 0 theta 1
      phi (plus (scal theta u) (scal (1-theta) v)).

End Convex.

Orthogonal projection

Section OrthogonalP.

Context {E : PreHilbert}.

Variable phi:E Prop.

Hypothesis phi_nonempty: y:E, phi y.
Hypothesis phi_convex: convex phi.

Lemma ortho_projection_aux: u:E,
  is_finite (Glb_Rbar (fun r w:E, phi w r = norm (minus u w))).

Theorem ortho_projection_convex': complete_subset phi
    u:E,
   ( eps:posreal, decidable ( w:E, phi w norm (minus u w) < eps))
   v:E,
    phi v norm (minus u v)
        = Glb_Rbar (fun r w:E, phi w r = norm (minus u w)).

Theorem ortho_projection_convex_unique: complete_subset phi
    u:E, v v':E,
    phi v norm (minus u v)
        = Glb_Rbar (fun r w:E, phi w r = norm (minus u w))
    phi v' norm (minus u v')
        = Glb_Rbar (fun r w:E, phi w r = norm (minus u w))
    v = v'.

Theorem ortho_projection_convex: complete_subset phi
    u:E,
  ( eps:posreal, decidable ( w:E, phi w norm (minus u w) < eps))
   ! v:E,
    phi v norm (minus u v)
        = Glb_Rbar (fun r w:E, phi w r = norm (minus u w)).

Lemma charac_ortho_projection_convex_aux1sq : u v w : E, t : R,
     phi v phi w 0 < t 1
       (norm (minus u v)) = (Glb_Rbar (fun r w:E, phi w r = norm (minus u w)))
      (((norm (minus u v))
     (norm (minus u (plus (scal t w) (scal (1-t) v)))))).

Lemma charac_ortho_projection_convex_aux1 : u v w : E, t : R,
    phi v phi w 0 < t 1
      (norm (minus u v)) = (Glb_Rbar (fun r w:E, phi w r = norm (minus u w)))
      (((norm (minus u v))*(norm (minus u v)))
       ((norm (minus u (plus (scal t w) (scal (1-t) v)))
        *(norm (minus u (plus (scal t w) (scal (1-t) v))))))).

Lemma charac_ortho_projection_convex_aux2 : u v w : E, t : R,
    phi v phi w 0 < t 1
     minus u (plus (scal t w) (scal (1-t) v))
        = plus (minus u v) (scal t (minus v w)).

Lemma charac_ortho_projection_convex_aux3 : u v w : E, t : R,
   phi v phi w 0 < t 1
    (norm (minus u (plus (scal t w) (scal (1-t) v))))*
       (norm (minus u (plus (scal t w) (scal (1-t) v))))
     = (minus ((norm (minus u v))*(norm (minus u v)))
             ((2×t)*(inner (minus u v) (minus w v)))) +
            (t×t)*((norm (minus v w))*(norm (minus v w))).

Lemma charac_ortho_projection_convex_aux4 : u v w : E, t : R,
   phi v phi w 0 < t 1
     (norm (minus u v))
        = (Glb_Rbar (fun r w:E, phi w r = norm (minus u w)))
     0 (-(2×t×inner (minus u v) (minus w v))
            +(t×t)*((norm (minus v w))*(norm (minus v w)))).

Lemma charac_ortho_projection_convex_aux5 : u v w : E, t : R,
 phi v phi w 0 < t 1
   (norm (minus u v))
      = (Glb_Rbar (fun r w:E, phi w r = norm (minus u w)))
   (2*(inner (minus u v) (minus w v)))
           t*((norm (minus v w))*(norm (minus v w))) .

Lemma charac_ortho_projection_convex_aux1_r : u v w :E, phi v
         phi w inner (minus u v) (minus w v) 0
          ((norm (minus u v) × norm (minus u v))
             ((norm (minus u w) × norm (minus u w)))).

Definition th (u v w : E) := Rmin 1 ((inner (minus u v) (minus w v))
                        /((norm (minus v w))*(norm (minus v w)))).

Lemma charac_ortho_projection_convex: u:E, v:E, phi v
   (norm (minus u v) = Glb_Rbar (fun r w:E, phi w r = norm (minus u w))
      
   ( w:E, phi w inner (minus u v) (minus w v) 0)).

End OrthogonalP.

Section OrthogonalQ.

Context {E : PreHilbert}.

Variable phi:E Prop.

Hypothesis phi_mod: compatible_m phi.
Hypothesis phi_compl: complete_subset phi.

Theorem ortho_projection_subspace:
    u:E, ( eps:posreal, decidable ( w:E, phi w norm (minus u w) < eps))
   ! v:E,
    phi v norm (minus u v)
        = Glb_Rbar (fun r w:E, phi w r = norm (minus u w)).

Lemma charac_ortho_projection_subspace1: u:E, v:E, phi v
   (norm (minus u v) = Glb_Rbar (fun r w:E, phi w r = norm (minus u w))
      
   ( w:E, phi w inner (minus u v) (minus w v) 0)).

End OrthogonalQ.

Orthogonal complement

Section ortho_compl.

Context {E : PreHilbert}.

Variable phi:E Prop.
Hypothesis phi_compat: compatible_m phi.
Hypothesis phi_compl: complete_subset phi.

Definition orth_compl := fun x:E (y:E), phi y inner x y = 0.

Lemma orth_compl_compat: compatible_m orth_compl.

Lemma trivial_orth_compl : u : E, (( v : E, inner u v = 0) u = zero).

Lemma trivial_orth_compl' : (phi : E Prop) (u : E),
       closed phi phi u (( v : E, phi v inner u v = 0) u = zero).

Lemma direct_sumable_with_orth_compl: direct_sumable phi orth_compl.

Lemma charac_ortho_projection_subspace2:
   u:E, v:E, phi v
     (norm (minus u v) = Glb_Rbar (fun r w:E, phi w r = norm (minus u w))
         
     ( w:E, phi w inner v w = inner u w)).

Lemma direct_sum_with_orth_compl: x, m_plus phi orth_compl x.

Lemma direct_sum_with_orth_compl_decomp: u v,
    phi v norm (minus u v)
        = Glb_Rbar (fun r w:E, phi w r = norm (minus u w))
      orth_compl (minus u v).

Lemma direct_sum_with_orth_compl_charac1: u v,
    phi v norm (minus u v)
        = Glb_Rbar (fun r w:E, phi w r = norm (minus u w))
      (phi u v = u).

Lemma direct_sum_with_orth_compl_charac2: u v,
    phi v norm (minus u v)
        = Glb_Rbar (fun r w:E, phi w r = norm (minus u w))
      (orth_compl u v = zero).

End ortho_compl.