Library Top.lax_milgram

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 Import hilbert.
Require Export continuous_linear_map.
Require Export Decidable.
Require Export FunctionalExtensionality.
Require Export mathcomp.ssreflect.ssreflect.
Require Export Coquelicot.Hierarchy.
Require Export Reals.
Require Export logic_tricks.
Require Export ProofIrrelevanceFacts.
Require Export Reals Coquelicot.Coquelicot.
Require Export R_compl.
Require Export logic_tricks.
Require Export compatible.

Section ker_generic.

Context {E : Hilbert}.
Context {F : NormedModule R_AbsRing}.

Kernel of an application

Definition ker (f : E F) := fun x:Ef x = zero.

Lemma compatible_m_ker : (f : E F), is_linear_mapping f
                  compatible_m (ker f).

Lemma clm_ker_convex : (f : EF), is_linear_mapping f
                 convex (ker f).

End ker_generic.

Kernel of an application in the topo dual

Section ker_dual.

Context {E : Hilbert}.

Lemma ker_nnker_equiv : (f : topo_dual E) x,
                        (ker (m f) x) ~~(ker (m f) x).

Lemma clm_ker_closed : (f : topo_dual E),
                  closed (ker f).

Lemma clm_ker_my_complete : (f : topo_dual E),
                  my_complete (ker f).

Lemma compatible_m_nnker : (f : topo_dual E),
                  compatible_m (fun x¬ ¬ ker f x).

Lemma clm_ker_complete : (f : topo_dual E),
                  complete_subset (fun x~~ ker f x).

Lemma clm_ker_convex2 : (f : topo_dual E),
                 convex (fun x~~ ker f x).

End ker_dual.

RIESZ-FRECHET


Section Riesz_Frechet.

Context {E : Hilbert}.

Variable phi : E Prop.

Hypothesis phi_C : my_complete (fun x : E~~phi x).

Hypothesis m_C : compatible_m (fun x:E~~ phi x).

Definition f_phi_neq_zero (f : topo_dual E) :=
                     ( u0, ~~ phi u0 f u0 0).

Riesz-Frechet theorem

Theorem Riesz_Frechet'_zero_phi : (f:topo_dual E),
   ¬f_phi_neq_zero f (u:E), ~~phi u (v:E),
     ~~phi v f v = inner u v.

Lemma compatible_m_and : (phi phi' : E Prop), compatible_m phi
          compatible_m phi' compatible_m (fun x : Ephi x phi' x).

Lemma closed_and : (phi phi' : E Prop), my_complete phi
    my_complete phi' my_complete (fun x : Ephi x phi' x).

Lemma Riesz_Frechet'_nzero_phi : (f:topo_dual E),
   ( u, eps:posreal, decidable ( w:E, ((ker f w ~~phi w)
                                                           norm (minus u w) < eps)))
   f_phi_neq_zero f (u:E), ~~phi u (v:E),
     ~~phi v f v = inner u v.

Theorem Riesz_Frechet_uniqueness_phi: (f:topo_dual E),
     u u',
     ((~~phi u) (v:E), ~~phi v f v = inner u v)
     ((~~phi u') (v:E), ~~phi v f v = inner u' v) u = u'.

Theorem Riesz_Frechet_zero_phi : (f:topo_dual E),
      (¬ f_phi_neq_zero f) ! (u:E), ~~phi u ( (v:E),
      ~~phi v f v = inner u v).

Theorem Riesz_Frechet_nzero_phi : (f:topo_dual E),
       ( u, eps:posreal, decidable ( w:E, ((ker f w ~~phi w)
                                                           norm (minus u w) < eps)))
      f_phi_neq_zero f ! (u:E), ~~phi u ( (v:E),
      ~~phi v f v = inner u v).

Theorem Riesz_Frechet_strong_phi : (f:topo_dual E),
    ( u, eps:posreal, decidable ( w:E, ((ker f w ~~phi w)
                                                           norm (minus u w) < eps)))
    (decidable (f_phi_neq_zero f)) ! (u:E), ~~phi u ( (v:E),
    ~~phi v f v = inner u v).

Riesz representation function

Context {F : Hilbert}.

Definition tau := fun (f:topo_dual E) ⇒
  (iota (fun u : E~~phi u v : E, ~~phi v f v = inner u v)).

Lemma iota_elim : (P : EProp) (v : E),
     (unique (fun x : EP x) v) iota P = v.

Lemma iota_elimE (H : (CompleteNormedModule R_AbsRing)) : (P : HProp) (v : H),
     (unique (fun x : HP x) v) iota P = v.

Lemma phi_tau :
     (f : topo_dual E),
     ( u, eps:posreal,
        decidable ( w:E, ((ker f w ~~phi w) norm (minus u w) < eps)))
    (decidable (f_phi_neq_zero f)) ~~phi (tau f).

Theorem Riesz_Frechet_moreover1_zero_phi :
    (f:topo_dual E),
       (¬ f_phi_neq_zero f) operator_norm_phi (fun x:E~~phi x) f
                                   = norm (tau f).

Theorem Riesz_Frechet_moreover1_nzero_phi :
    (f:topo_dual E),
    ( u, eps:posreal, decidable ( w:E, ((ker f w
                                                           (fun x:E~~phi x) w)
                                                           norm (minus u w) < eps)))
        (f_phi_neq_zero f) operator_norm_phi (fun x:E~~ phi x) f = norm (tau f).

Theorem Riesz_Frechet_moreover1_phi:
    (f:topo_dual E),
     (decidable (f_phi_neq_zero f))
      ( u, eps:posreal, decidable ( w:E, ((ker f w ~~phi w)
                                                           norm (minus u w) < eps)))
         operator_norm_phi (fun x:E~~phi x) f = norm (tau f).

Theorem Riesz_Frechet_moreover2_phi :
    ( f:topo_dual E,
     decidable (f_phi_neq_zero f))
  ( (f:topo_dual E), u, eps:posreal, decidable ( w:E, ((ker f w ~~phi w)
                                                           norm (minus u w) < eps)))
     is_linear_mapping tau.

End Riesz_Frechet.

LAX-MILGRAM


Section LM_aux.

Context {E : Hilbert}.

Variable a : E E R.
Variable M : R.
Variable alpha : R.
Variable phi : E Prop.

Hypothesis phi_C : my_complete (fun x:E~~phi x).
Hypothesis phi_m : compatible_m (fun x:E~~phi x).
Hypothesis Hba : is_bounded_bilinear_mapping a M.
Hypothesis Hca : is_coercive a alpha.

Definition is_sol_linear_pb_phi (f:E R) (u:E):=
    ~~ phi u v:E, ~~phi v a u v = f v.

Definition Tau := fun (f:topo_dual E) ⇒
  (iota (fun u : E~~ phi u v : E, ~~ phi v f v = inner u v)).

Lemma phi_Tau : (f : topo_dual E),
    ( u, eps:posreal, decidable ( w:E, ((ker f w ~~ phi w)
                                                           norm (minus u w) < eps)))
    (decidable (f_phi_neq_zero phi f)) ~~ phi (Tau f).

Calculations

Variable A : (clm E (topo_dual E)).
Hypothesis A_bil : unique (fun A : (clm E (topo_dual E)) ⇒
                                     (u v:E), a u v = (A u) v) A.
Hypothesis A_dec : (u0 : E), decidable ( u : E, ~~phi u A u0 u 0).
Hypothesis A_dec2 : (u0 : E), decidable ( u : E, A u0 u 0).

Lemma comp_lm_aux_phi : (C : R),
     (0 < alpha C) ( (rho : R), 0 < rho < (2×alpha)/(C×C)
      0 ((1 - (2×rho×alpha)) + rho×rho×C×C)).

Lemma comp_lax_milgram_phi : (C : R),
     (0 < alpha C) ( (rho : R), 0 < rho < (2×alpha)/(C×C)
      0 (sqrt ((1 - (2×rho×alpha)) + rho×rho×C×C)) < 1).

Theorem Lax_Milgram_115
   (f:topo_dual E):
   u : E, alpha*(Rsqr (norm u)) ((a u) u).

Theorem Lax_Milgram_116_phi :
                u : E, operator_norm_phi (fun x:E~~phi x) (A u) M*(norm u).

Theorem Lax_Milgram_117_phi (f:topo_dual E) : ( g : topo_dual E, decidable (f_phi_neq_zero phi g))
  ( (f:topo_dual E), u, eps:posreal, decidable ( w:E, ((ker f w ~~phi w)
                                                           norm (minus u w) < eps)))
   u : E, ~~phi u - (inner (Tau (A u)) u) - (alpha*(Rsqr (norm u))).

Theorem Lax_Milgram_118_phi (f:topo_dual E) :
             ( (f:topo_dual E), u, eps:posreal,
                     decidable ( w:E, ((ker f w ~~phi w)
                                                           norm (minus u w) < eps)))
             ( f: topo_dual E, decidable (f_phi_neq_zero phi f))
              u : E, norm (Tau (A u)) M*(norm u).

Implication (2) -> (1)

Theorem Lax_Milgram'_aux1_phi (f:topo_dual E) :
     ( f : topo_dual E, decidable (f_phi_neq_zero phi f))
   ( g : topo_dual E, u, eps:posreal, decidable ( w:E, ((ker g w ~~phi w)
                                                           norm (minus u w) < eps)))
   ((! u:E, ~~phi u Tau ((A u)) = Tau f)
   (! u:E, (is_sol_linear_pb_phi f u))).

Implication (3) -> (2)

Definition g_map_app (r : R) (f : topo_dual E) :=
      (fun u:Eplus (minus u (scal r (Tau (A u)))) (scal r (Tau f))).

Theorem Lax_Milgram'_aux2_phi (r : R) (f:topo_dual E) :
     0 < r < ((2×alpha)/(M×M))
   ( (f : topo_dual E), decidable (f_phi_neq_zero phi f))
   ( (g : topo_dual E), u, eps:posreal, decidable ( w:E, ((ker g w ~~phi w)
                                                           norm (minus u w) < eps)))
   (! u:E, ~~phi u (g_map_app r f u = u))
   (! u:E, (is_sol_linear_pb_phi f u)).

Contraction and Fixpoint

Lemma g_map_diff_phi (r : R) (f:topo_dual E) :
       ( (f0 : topo_dual E), decidable (f_phi_neq_zero phi f0))
      ( (f : topo_dual E), u, eps:posreal, decidable ( w:E, ((ker f w ~~phi w)
                                                           norm (minus u w) < eps)))
     0 < r < ((2×alpha)/(M×M))
     (v v' : E), ~~phi v ~~phi v'
       Rsqr (norm (minus (g_map_app r f v) (g_map_app r f v')))
        (1 - 2 × r × alpha + r × r × M × M)
          × Rsqr (norm (minus v v')).

Theorem Lax_Milgram'_aux3_phi (r : R)(f:topo_dual E) :
     ( f0 : topo_dual E, decidable (f_phi_neq_zero phi f0))
   ( f0 : topo_dual E, u, eps:posreal, decidable ( w:E, ((ker f0 w ~~phi w)
                                                           norm (minus u w) < eps)))
   (¬ Is_only_zero_set_phi E (fun x:E~~phi x))
   0 < r < ((2×alpha)/(M×M))
   (! u:E, ~~phi u (g_map_app r f u = u)).

Weak versions of Lax-Milgram theorem

Theorem Lax_Milgram''_phi (f:topo_dual E):
  ( f0 : topo_dual E, decidable (f_phi_neq_zero phi f0))
   ( f0 : topo_dual E, u, eps:posreal,
                               decidable ( w:E, ((ker f0 w ~~phi w)
                                norm (minus u w) < eps)))
   u:E, is_sol_linear_pb_phi f u
          ( u', is_sol_linear_pb_phi f u' u'=u).

Theorem Lax_Milgram_Aux_phi (f:topo_dual E):
  ( f0 : topo_dual E, decidable (f_phi_neq_zero phi f0))
   ( f0 : topo_dual E, u, eps:posreal,
      decidable ( w:E, ((ker f0 w ~~phi w)
       norm (minus u w) < eps)))
   u:E, is_sol_linear_pb_phi f u
          ( u', is_sol_linear_pb_phi f u' u'=u)
           norm u /alpha × norm f.

End LM_aux.

Lax-Milgram theorem

Section Lax_Milgram.

Context {E : Hilbert}.

Variable a : E E R.
Variable M : R.
Variable alpha : R.
Variable phi : E Prop.
Hypothesis phi_C : my_complete (fun x:E~~ phi x).
Hypothesis phi_m : compatible_m (fun x:E~~ phi x).
Hypothesis Hba : is_bounded_bilinear_mapping a M.
Hypothesis Hca : is_coercive a alpha.

Theorem Lax_Milgram_phi (f:topo_dual E):
  ( f0 : topo_dual E, decidable (f_phi_neq_zero phi f0))
   ( f0 : topo_dual E, u, eps:posreal,
      decidable ( w:E, ((ker f0 w ~~phi w)
       norm (minus u w) < eps)))
   u:E, is_sol_linear_pb_phi a phi f u
          ( u', is_sol_linear_pb_phi a phi f u' u'=u)
           norm u /alpha × norm f.

End Lax_Milgram.

Section LM_True.

Context{E : Hilbert}.
Variable a : E E R.
Variable M : R.
Variable alpha : R.
Hypothesis Hba : is_bounded_bilinear_mapping a M.
Hypothesis Hca : is_coercive a alpha.

Theorem Lax_Milgram_true (f:topo_dual E):
  ( g: topo_dual E, decidable ( u0, g u0 0))
  ( f0 : topo_dual E, u, eps:posreal,
      decidable ( w:E, ((ker f0 w)
       norm (minus u w) < eps)))
   u:E, is_sol_linear_pb_phi a (fun _True) f u
          ( u', is_sol_linear_pb_phi a (fun _True) f u' u'=u)
           norm u /alpha × norm f.

End LM_True.