Library Top.lax_milgram_cea

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 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 lax_milgram.

Lax-Milgram-Cea's Theorem

Section LMC.

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.

Lemma Galerkin_orthogonality (u uh : E)
               (f:topo_dual E) (phi : E Prop) :
      ( (f : topo_dual E), decidable ( u : E, f u 0))
      phi uh
      is_sol_linear_pb_phi a (fun x:ETrue) f u
      is_sol_linear_pb_phi a phi f uh
      ( vh : E, phi vh a (minus u uh) vh = 0).

Lemma Lax_Milgram_Cea (u uh : E) (f:topo_dual E) (phi : E Prop) :
      ( (f : topo_dual E), decidable ( u : E, f u 0))
      phi uh compatible_m phi my_complete phi
      is_sol_linear_pb_phi a (fun x:ETrue) f u
      is_sol_linear_pb_phi a phi f uh ( vh : E, phi vh
      norm (minus u uh) (M/alpha) × norm (minus u vh)).

End LMC.