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:ETrue) 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:ETrue) 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.