Library LM.lax_milgram_cea
This file is part of the Coq Numerical Analysis 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.
From Coq Require Import Decidable FunctionalExtensionality ProofIrrelevanceFacts Reals ssreflect.
From Coquelicot Require Import Coquelicot.
Close Scope R_scope.
From Algebra Require Import Algebra.
From LM Require Import fixed_point hilbert continuous_linear_map lax_milgram.
Local Open Scope R_scope.
Lax-Milgram-Cea's Theorem
Section LMC.
Context { E : Hilbert }.
Variable a : E → E → R.
Variable M : R.
Variable alpha : R.
Hypothesis Hba : bound_bilin_map 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 →
sol_lin_pb_phi a (fun x:E ⇒ True) f u →
sol_lin_pb_phi a phi f uh →
(∀ vh : E, phi vh → a (minus u uh) vh = 0).
Proof.
intros Hd phi_uh Hle Hleh vh SubEh.
unfold minus.
destruct Hba as ((Hba1,Hba2),_).
rewrite (lm_plus (Hba1 vh)).
replace (opp uh) with (scal (opp one) uh).
rewrite (lm_scal (Hba1 vh)).
rewrite scal_opp_one.
unfold sol_lin_pb_phi in Hle.
destruct Hle as (_,Hle).
rewrite Hle.
rewrite (proj2 Hleh).
rewrite plus_opp_r.
reflexivity.
trivial.
trivial.
rewrite scal_opp_one.
reflexivity.
Qed.
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_ms phi → my_complete phi →
sol_lin_pb_phi a (fun x:E ⇒ True) f u →
sol_lin_pb_phi a phi f uh → (∀ vh : E, phi vh →
norm (minus u uh) ≤ (M/alpha) × norm (minus u vh)).
Proof.
intros Hdf Huh HM HC H1 H2 vh Hvh.
destruct (is_zero_dec (minus u uh)).
rewrite H.
rewrite norm_zero.
apply Rmult_le_pos.
destruct Hba as (_,(Hb,_)).
replace (M / alpha) with (M × / alpha); try trivial.
replace 0 with (0×0).
apply Rmult_le_compat; auto with real.
intuition.
destruct Hca as (Hc,_).
apply Rinv_0_lt_compat in Hc.
auto with real. ring.
apply norm_ge_0.
assert (Ha : a (minus u uh) (minus u vh) = a (minus u uh) u).
transitivity (minus (a (minus u uh) u) (a (minus u uh) vh)).
destruct Hba as ((Hba1,Hba2),_).
rewrite (lm_plus (Hba2 _)).
unfold minus at 3.
replace (a (minus u uh) (opp vh)) with (opp (a (minus u uh) vh)).
reflexivity.
replace (opp vh) with (scal (opp one) vh).
rewrite (lm_scal (Hba2 _)).
rewrite scal_opp_one.
reflexivity.
rewrite scal_opp_one.
reflexivity.
replace (a (minus u uh) vh) with 0.
unfold minus at 1.
rewrite opp_zero.
rewrite plus_zero_r.
reflexivity.
symmetry.
apply Galerkin_orthogonality with f phi; try assumption.
apply Rmult_le_reg_l with alpha.
apply Hca.
field_simplify.
replace (alpha × norm (minus u uh) / 1) with (alpha × norm (minus u uh))
by field.
replace (M × norm (minus u vh) / 1) with (M × norm (minus u vh)) by field.
apply Rmult_le_reg_r with (norm (minus u uh)).
now apply norm_gt_0.
destruct Hba as (H0,H3).
destruct H3 as (H3,H4).
specialize (H4 (minus u uh) (minus u vh)).
apply Rle_trans with (norm (a (minus u uh) (minus u vh)));
try assumption.
rewrite Ha.
destruct Hca as (H5,H6).
unfold sol_lin_pb_phi in ×.
destruct H1 as (X1,H1).
destruct H2 as (X2,H2).
replace (a (minus u uh) u)
with (a (minus u uh) (minus u uh)).
specialize (H6 (minus u uh)).
unfold norm at 3.
simpl.
apply Rle_trans with (a (minus u uh) (minus u uh)).
trivial.
unfold abs.
simpl.
apply Rle_abs.
destruct H0 as (H0,H7).
unfold minus.
rewrite (lm_plus (H7 _)).
rewrite -(plus_zero_r (a (plus u (opp uh)) u)).
f_equal.
now rewrite plus_zero_r.
specialize (H1 uh).
apply H1 in X1.
specialize (H2 uh).
apply H2 in X2.
clear H1 H2.
rewrite (lm_plus (H0 _)).
replace (a u (opp uh)) with (opp (a u uh)).
rewrite X1.
replace (a (opp uh) (opp uh)) with (a uh uh).
rewrite X2.
rewrite plus_opp_l; reflexivity.
replace (opp uh) with (scal (opp one) uh).
replace (opp uh) with (scal (opp one) uh).
rewrite (lm_scal (H0 _)) (lm_scal (H7 _)).
rewrite 2!scal_opp_l scal_one opp_opp scal_one.
reflexivity.
rewrite scal_opp_one.
reflexivity.
rewrite scal_opp_one; reflexivity.
replace (opp uh) with (scal (opp one) uh).
rewrite (lm_scal (H7 _)) scal_opp_one.
reflexivity.
rewrite scal_opp_one.
reflexivity.
rewrite Rmult_assoc (Rmult_comm (norm _)) -Rmult_assoc.
assumption.
destruct Hca.
intro Hk.
rewrite Hk in H0.
absurd (0 < 0); try assumption.
exact (Rlt_irrefl 0).
Qed.
End LMC.