Library LM.lax_milgram

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 Numbers Require Import R_compl.
From Algebra Require Import Algebra.
From LM Require Import fixed_point hilbert continuous_linear_map.

Local Open Scope R_scope.

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 cms_ker : (f : E F), lin_map f
                  compatible_ms (ker f).
Proof.
intros f Hf.
repeat split; unfold ker.
intros x y Hx Hy; rewrite (lm_plus Hf) Hx Hy plus_zero_l; easy.
apply (lm_zero Hf).
intros x Hx; rewrite (lm_opp Hf) Hx opp_zero; easy.
intros l x Hx; rewrite (lm_scal Hf) Hx scal_zero_r; easy.
Qed.

Lemma clm_ker_convex : (f : EF), lin_map f
                 convex (ker f).
Proof.
intros f H x y t Hx Hy Ht.
unfold ker in ×.
destruct H as (G1,G2).
rewrite G1.
repeat (rewrite G2).
rewrite Hx; rewrite Hy.
repeat (rewrite scal_zero_r).
rewrite plus_zero_l.
reflexivity.
Qed.

End ker_generic.

Kernel of an application in the topo dual

Section ker_dual.

Context {E : Hilbert}.


Lemma clm_ker_closed : (f : topo_dual E),
                  closed (ker f).
Proof.
intros f x Hx.
unfold ker in ×.
cut (continuous f x).
unfold continuous, filterlim, filter_le, filtermap.
intros H. specialize H with (P:=fun yy 0).
case (Req_dec (f x) 0); try easy; intros H1.
assert (K: 0 < Rabs (f x)).
apply Rabs_pos_lt.
trivial.
exfalso.
apply Hx.
apply H.
(pos_div_2 (mkposreal _ K)).
simpl; unfold Hierarchy.ball; simpl.
unfold AbsRing_ball; simpl.
unfold abs; simpl.
intros y Hy.
destruct (Req_dec y 0).
rewrite H0 in Hy.
unfold minus in ×.
rewrite plus_zero_l in Hy.
rewrite Rabs_Ropp in Hy.
assert (Rabs (f x) / 2 < Rabs (f x)).
apply Rmult_lt_reg_l with 2.
auto with real.
assert (H1':2 × (Rabs (f x) / 2) = (Rabs (f x))).
field.
rewrite H1'.
replace (Rabs (f x)) with (1*(Rabs (f x))) at 1.
apply Rmult_lt_compat_r; auto with real.
ring_simplify; reflexivity.
exfalso.
apply Rlt_not_le in Hy.
apply Hy.
auto with real.
trivial.
apply clm_3_2.
apply clm_4_3.
apply clm_5_4.
apply f.
apply clm_6_5.
apply f.
apply Cf.
Qed.

Lemma clm_ker_my_complete : (f : topo_dual E),
                  my_complete (ker f).
Proof.
intros f.
apply closed_my_complete.
apply clm_ker_closed.
Qed.

Lemma cms_ker_alt : (f : topo_dual E),
                  compatible_ms (ker f).
Proof.
intros; apply cms_ker, Lf.
Qed.



End ker_dual.

RIESZ-FRECHET


Section Riesz_Frechet.

Context {E : Hilbert}.

Variable phi : E Prop.

Hypothesis phi_C : my_complete phi.

Hypothesis m_C : compatible_ms phi.

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.
Proof.
intros f H.
zero.
split.
apply (cms_zero m_C).
intros v Hv.
rewrite inner_zero_l.
destruct (Req_dec (f v) 0).
trivial.
exfalso.
apply H.
v.
split; trivial.
Qed.

Lemma cms_and : (phi phi' : E Prop), compatible_ms phi
          compatible_ms phi' compatible_ms (fun x : Ephi x phi' x).
Proof.
intros phi0 phi0' C C'.
split; [split; [split |] |].
intros x y Hx Hy; split; [apply C | apply C']; easy.
split; apply cms_zero; easy.
intros x Hx; split; [apply C | apply C']; easy.
intros l x Hx; split; [apply C | apply C']; easy.
Qed.

Lemma closed_and : (phi phi' : E Prop), my_complete phi
    my_complete phi' my_complete (fun x : Ephi x phi' x).
Proof.
intros phi0 phi0' C C' F HPf Hcf H.
split.
unfold my_complete in C, C'.
apply C; try assumption.
intros P HFP.
intro.
specialize (H P HFP).
apply H.
intro.
apply H0.
destruct H1 as (x,(H1,(H2,_))).
x; try intuition.
apply C'; try assumption.
intros P HFP.
intro.
specialize (H P HFP).
apply H.
intro.
apply H0.
destruct H1 as (x,(H1,(_,H2))).
x; try intuition.
Qed.

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.
Proof.
intros f HD2 H.
destruct H as (u0,H).
pose (PHI := fun w : Eker f w phi w).
assert ( 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)).
apply: direct_sum_with_orth_compl_charac1.
apply cms_and.
apply cms_ker.
apply f.
trivial.
unfold complete_subset.
(fixed_point.lim).
intros F K K0 K1.
split.
assert (PHI_C : my_complete PHI).
apply closed_and.
apply clm_ker_my_complete.
apply phi_C; try assumption.
apply PHI_C; try assumption.
apply: complete_cauchy; easy.
assert ( u, ! v:E,
       PHI v norm (minus u v)
       = Glb_Rbar (fun r w:E, PHI w
         r = norm (minus u w))).
intros u; apply: ortho_projection_convex.
zero.
split.
apply (cms_zero (cms_ker_alt f)).
apply (cms_zero m_C).
split.
assert (compatible_ms (fun x : Eker f x)).
apply cms_ker, f.
replace (scal (1 - theta) v)
        with (opp (opp (scal (1 - theta) v))).
apply (cms_minus H4).
apply H4.
apply H1.
rewrite <- scal_opp_one.
apply H4.
apply H4.
apply H2.
now rewrite opp_opp.
replace (scal (1 - theta) v)
        with (opp (opp (scal (1 - theta) v))).
apply (cms_minus m_C).
apply m_C.
apply H1.
rewrite <- scal_opp_one.
apply m_C.
apply m_C.
apply H2.
now rewrite opp_opp.
unfold complete_subset.
(fixed_point.lim).
intros F K K0 K1.
split.
assert (PHI_C : my_complete PHI).
apply closed_and.
apply clm_ker_my_complete.
apply phi_C; try assumption.
apply PHI_C; try assumption.
apply: complete_cauchy; easy.
apply HD2.
destruct (H1 u0).
assert (~(x = u0)).
rewrite <- H0.
intro hF.
unfold PHI in hF.
destruct hF as (hF1,hF2).
unfold ker in hF1.
intuition.
apply H2.
apply H2.
pose (v0 := minus u0 x).
assert (v0 zero).
unfold v0. intro.
absurd (x = u0).
trivial.
apply plus_reg_r with (opp x).
unfold minus in H4.
rewrite plus_opp_r.
symmetry; trivial.
pose (e0 := scal (/ (norm v0)) v0).
pose (u := scal (f e0) e0).
u.
split.
unfold u.
apply m_C.
unfold e0.
apply m_C.
unfold v0.
apply (cms_minus m_C).
intuition.
apply H2.
intros v Hv.
assert (e0 zero).
assert (f e0 zero).
unfold e0.
assert (Lin : (lin_map f)).
apply Lf.
destruct Lin as (Lin1,Lin2).
rewrite Lin2.
unfold scal.
simpl.
apply Rmult_integral_contrapositive.
split.
apply Rinv_neq_0_compat.
intro.
apply NormedModule.ax5 in H5.
intuition.
unfold v0. unfold minus.
rewrite Lin1.
assert (f (opp x) = 0).
assert (opp x = scal (opp one) x).
rewrite scal_opp_one.
reflexivity.
rewrite H5.
rewrite Lin2.
assert (ker f x).
apply H2.
unfold ker in H6.
rewrite H6.
rewrite scal_zero_r.
reflexivity.
rewrite H5.
rewrite plus_zero_r.
intuition.
trivial.
intro. rewrite H6 in H5.
rewrite lm_zero in H5.
intuition.
apply Lf.
assert (norm e0 = 1).
unfold e0.
rewrite norm_scal_R.
assert (abs (/norm v0) = /norm v0).
assert ( x : R, (0 x) abs(x) = x).
intros.
unfold abs.
simpl.
apply Rabs_pos_eq.
trivial.
apply H6.
assert (0 < / norm v0).
apply Rinv_0_lt_compat.
apply norm_gt_0.
intuition.
auto with real.
rewrite H6.
field. intro.
apply NormedModule.ax5 in H7.
intuition.
pose (lambda := (f v) / (f e0)).
pose (w := minus v (scal lambda e0)).
assert (f w = 0).
unfold w. unfold lambda. unfold minus.
assert (lin_map f).
apply Lf.
destruct H7.
rewrite H7.
assert (f (opp (scal (f v / f e0) e0))
        = opp ((scal (f v / f e0) (f e0)))).
rewrite <- scal_opp_one.
rewrite H8.
symmetry.
rewrite H8. rewrite scal_opp_one.
rewrite <- H8. rewrite <- H8. unfold e0.
reflexivity.
rewrite H9. unfold scal. simpl.
assert (mult (f v / f e0) (f e0) = f v).
assert ((f v / f e0) = mult (f v) (/f e0)).
intuition. rewrite H10.
rewrite <- mult_assoc.
change ((mult (/ f e0) (f e0)))
        with ((/ f e0)*(f e0)).
rewrite Rinv_l. rewrite mult_one_r. reflexivity.
unfold e0.
assert (Lin : (lin_map f)).
apply Lf. destruct Lin as (Lin1,Lin2).
rewrite Lin2. unfold scal; simpl.
apply Rmult_integral_contrapositive.
split. assert (0 < / norm v0).
apply Rinv_0_lt_compat.
apply norm_gt_0.
intuition.
intro. apply Rlt_not_le in H11.
apply H11.
auto with real.
unfold v0. unfold minus.
rewrite Lin1.
assert (f (opp x) = 0).
assert (opp x = scal (opp one) x).
rewrite scal_opp_one.
reflexivity.
rewrite H11.
rewrite Lin2.
assert (ker f x).
apply H2.
unfold ker in H12.
rewrite H12.
rewrite scal_zero_r.
reflexivity.
rewrite H11.
rewrite plus_zero_r.
intuition.
rewrite H10.
rewrite plus_opp_r.
reflexivity.
assert (orth_compl (fun xPHI x) v0).
unfold v0.
apply: direct_sum_with_orth_compl_decomp.
apply cms_and.
apply cms_ker, f.
trivial.
apply H2.
apply H2.
assert (orth_compl (fun xPHI x) e0).
unfold e0.
assert (compatible_ms
                (orth_compl (fun x0 : EPHI x0))).
apply orth_compl_compat.
apply H9; trivial.
assert (orth_compl (fun xPHI x) u).
unfold u.
assert (compatible_ms
                (orth_compl (fun x0 : EPHI x0))).
apply orth_compl_compat.
apply H10; trivial.
assert (inner u w = 0).
apply H10.
split.
trivial.
unfold w.
apply (cms_minus m_C).
trivial.
apply m_C.
unfold e0.
apply m_C.
unfold v0.
apply (cms_minus m_C).
intuition.
apply H2.
assert (inner u w = minus (inner u v) (f v)).
assert (minus (inner u v) (f v)
        = minus (inner u v) (scal lambda (inner u e0))).
unfold lambda. unfold u at 3.
rewrite (inner_scal_l e0 e0 (f e0)).
unfold scal. simpl.
rewrite mult_assoc.
assert (inner e0 e0 = 1).
rewrite <- squared_norm.
unfold norm in H6. simpl in H6.
rewrite H6.
ring_simplify; reflexivity.
rewrite H12.
rewrite mult_one_r.
assert ((f v / f e0) = mult (f v) (/ f e0)).
reflexivity.
rewrite H13.
rewrite <- mult_assoc.
rewrite <- Rinv_l_sym.
rewrite mult_one_r.
reflexivity.
assert (f e0 zero).
unfold e0.
assert (Lin : (lin_map f)).
apply Lf.
destruct Lin as (Lin1,Lin2).
rewrite Lin2.
unfold scal.
simpl.
apply Rmult_integral_contrapositive.
split.
apply Rinv_neq_0_compat.
intro.
apply NormedModule.ax5 in H14.
intuition.
unfold v0. unfold minus.
rewrite Lin1.
assert (f (opp x) = 0).
assert (opp x = scal (opp one) x).
rewrite scal_opp_one.
reflexivity.
rewrite H14.
rewrite Lin2.
assert (ker f x).
apply H2.
unfold ker in H15.
rewrite H15.
rewrite scal_zero_r.
reflexivity.
rewrite H14.
rewrite plus_zero_r.
intuition.
apply H14.
rewrite H12.
unfold w.
unfold minus.
rewrite inner_plus_r.
rewrite <- inner_scal_r.
rewrite <- inner_opp_r.
reflexivity.
rewrite H11 in H12.
apply plus_reg_r with (opp (f v)).
rewrite plus_opp_r.
unfold minus in H12.
trivial.
Qed.

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'.
Proof.
intros f u u' H H0.
assert ( v : E, phi v inner u v = inner u' v).
intros.
transitivity (f v).
symmetry.
apply H.
trivial.
apply H0.
trivial.
assert ( v : E, phi v inner (minus u u') v = 0).
intros. unfold minus.
rewrite inner_plus_l. rewrite inner_opp_l.
ring_simplify. rewrite H1. ring_simplify; reflexivity.
trivial.
apply trivial_orth_compl' in H2.
unfold minus in H2. apply plus_reg_r with (opp u').
rewrite plus_opp_r. trivial.
now apply: my_complete_closed.
apply (cms_minus m_C); easy.
Qed.

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).
Proof.
intros f H.
rewrite <- unique_existence; split.
apply Riesz_Frechet'_zero_phi.
trivial.
unfold uniqueness.
apply Riesz_Frechet_uniqueness_phi.
Qed.

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).
Proof.
intros f HD2 H.
rewrite <- unique_existence; split.
apply Riesz_Frechet'_nzero_phi.
trivial.
trivial.
trivial.
unfold uniqueness.
apply Riesz_Frechet_uniqueness_phi.
Qed.

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).
Proof.
intros f J Hor.
destruct Hor.
now apply Riesz_Frechet_nzero_phi.
now apply Riesz_Frechet_zero_phi.
Qed.

Riesz representation function

Context {F : Hilbert}.

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

Lemma iota_elim : (P : EProp) (v : E),
     (unique (fun x : EP x) v) Hierarchy.iota P = v.
Proof.
intros P v Hu.
assert (! v, P v).
v.
trivial.
apply iota_correct in H.
assert (P v).
apply Hu.
unfold unique in Hu.
destruct Hu as (_,Hu).
symmetry.
apply Hu.
trivial.
Qed.

Lemma iota_elimE (H : (CompleteNormedModule R_AbsRing)) : (P : HProp) (v : H),
     (unique (fun x : HP x) v) Hierarchy.iota P = v.
Proof.
intros P v Hu.
assert (H' : ! v, P v).
v.
trivial.
apply iota_correct in H'.
assert (P v).
apply Hu.
unfold unique in Hu.
destruct Hu as (_,Hu).
symmetry.
apply Hu.
trivial.
Qed.

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).
Proof.
intros f Hd Hd'.
unfold tau.
assert (H : ! (w:E), phi w (v:E),
      phi v f v = inner w v).
apply Riesz_Frechet_strong_phi; trivial.
destruct H as (w,H).
generalize H.
intros H'.
apply (iota_elim _ _) in H.
rewrite H.
apply H'.
Qed.

Theorem Riesz_Frechet_moreover1_zero_phi :
    (f:topo_dual E),
       (¬ f_phi_neq_zero f) operator_norm_phi phi f
                                   = norm (tau f).
Proof.
intros f H.
simpl.
assert (! (u:E), phi u (v:E), phi v
      f v = inner u v).
apply Riesz_Frechet_zero_phi.
intro Hf.
destruct Hf as (vf,Hf).
apply H.
vf; trivial.
destruct H0 as (u,H0).
apply (iota_elim _ _ ) in H0.
unfold tau.
rewrite H0.
assert ( v, phi v f v = 0).
intros v HV.
destruct (Req_dec (f v) 0).
trivial.
exfalso.
apply H.
v.
split; trivial.
assert (u = zero).
rewrite <- H0.
assert (! (u:E), phi u (v:E),
      phi v f v = inner u v).
apply Riesz_Frechet_zero_phi.
intro Hf.
destruct Hf as (vf,Hf).
apply H.
vf; trivial.
destruct H2 as (u2,H2).
assert ( v, phi v inner u2 v = zero).
intros v0 Hv0.
assert (f v0 = inner u2 v0).
apply H2.
trivial.
rewrite <- H3.
unfold f_phi_neq_zero in H.
destruct (is_zero_dec (f v0)).
trivial.
exfalso.
apply H.
v0; split; trivial.
generalize H2; intro H2'.
apply (iota_elim _ _ ) in H2.
rewrite H2.
specialize (H3 u2).
apply PreHilbert.ax3 in H3.
trivial.
apply H2'.
rewrite H2.
rewrite norm_zero.
assert ( u, u zero phi u norm (f u) 0 × norm u).
intros u0 H3 H3'.
unfold f_phi_neq_zero.
rewrite H1.
rewrite norm_zero.
ring_simplify; auto with real.
trivial.
apply (operator_norm_helper3'_phi phi) in H3.
assert (Rbar_le 0 (operator_norm_phi phi f)).
apply operator_norm_ge_0_phi.
try assumption.
apply Rbar_le_antisym.
assert (is_finite (operator_norm_phi phi f)).
apply operator_norm_helper3_phi with 0.
try assumption.
apply Rle_refl.
intros u0 Hu0 Hu0'.
rewrite H1.
rewrite norm_zero.
ring_simplify; auto with real.
trivial.
unfold Rbar_le.
rewrite <- H5.
trivial.
trivial.
try assumption.
now apply Rle_refl.
Qed.

Theorem Riesz_Frechet_moreover1_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) operator_norm_phi phi f = norm (tau f).
Proof.
intros f K H.
simpl.
assert (! (u:E), phi u (v:E), phi v
      f v = inner u v).
apply Riesz_Frechet_nzero_phi; trivial.
destruct H as (v,H).
destruct H0 as (u,H0).
assert (! (u:E), phi u (v:E), phi v
      f v = inner u v).
apply Riesz_Frechet_nzero_phi; trivial.
v.
trivial.
destruct H1 as (u1,H1).
assert (Heq : u = u1).
unfold unique in H1.
destruct H1 as (H11,H12).
symmetry.
apply H12.
apply H0.
apply (iota_elim _ _ ) in H0.
unfold tau.
rewrite H0.
assert (u zero).
rewrite Heq.
destruct H1 as (H11,H12).
assert (f v = inner u1 v).
apply H11.
exact (proj1 H).
intro.
absurd (f v = zero).
trivial.
rewrite H2 in H1.
rewrite inner_zero_l in H1.
trivial.
assert (norm u 0).
intro.
apply norm_eq_zero in H3.
intuition.
exfalso; intuition.
rewrite H2 in H1.
rewrite inner_zero_l in H1.
trivial.
assert (Haf : (norm(f u))/(norm u)=norm u).
assert (f u = inner u u).
rewrite <- Heq in H1.
apply H1.
apply H1.
rewrite H3.
rewrite <- squared_norm.
assert (norm (Hnorm u × Hnorm u) = norm u × norm u).
assert (HnN : Hnorm u = norm u).
reflexivity.
rewrite HnN.
assert (Hnorm : x, 0 x norm(x) = x).
intros x Posx.
unfold norm.
simpl.
unfold abs.
simpl.
unfold Rabs.
destruct (Rcase_abs x).
absurd (0 x); trivial.
apply Rlt_not_le in r.
trivial.
trivial.
apply Hnorm.
apply Rle_0_sqr.
rewrite H4.
field.
destruct (Req_dec (norm u) 0).
apply norm_eq_zero in H5.
exfalso; intuition.
trivial.
assert (HG : Rbar_le (norm u) (operator_norm_phi phi f)).
rewrite <- Haf.
unfold operator_norm_phi.
destruct (Is_only_zero_set_dec_phi E).
unfold Lub_Rbar.
destruct (ex_lub_Rbar
 (fun x : R u0 : Hilbert_NormedModule E,
 u0 zero phi u0 x = norm (f u0) / norm u0)).
simpl. destruct x.
unfold is_lub_Rbar in i.
unfold is_ub_Rbar in i.
destruct i.
apply H3.
u; intuition.
rewrite <- Heq in H1.
apply H1.
trivial.
trivial.
destruct i.
unfold is_ub_Rbar in H3.
simpl in H3.
apply H3 with (norm (f u) / norm u).
u.
rewrite <- Heq in H1.
split; try assumption.
split; try reflexivity.
apply H1.
apply (Is_only_zero_set_correct1_phi E phi) with u in i.
absurd (norm u = 0).
exfalso; intuition.
rewrite i.
rewrite norm_zero.
reflexivity.
rewrite <- Heq in H1.
apply H1.
assert (HD : Rbar_le (operator_norm_phi phi f) (norm u)).
destruct (operator_norm_helper2'_phi phi f).
destruct f.
apply op_norm_finite_phi; try assumption.
destruct H3 as (HZ,Hof).
rewrite Hof.
apply norm_ge_0.
destruct H3 as (HZ,Hof).
assert (Hfin : is_finite (operator_norm_phi phi f)).
destruct f; trivial.
apply op_norm_finite_phi; try assumption.
destruct (operator_norm_phi phi f).
apply Hof.
apply norm_ge_0.
intros u0 Hu0 Hp0.
assert (HU0 : (Rabs (f u0) / (norm u0)) norm u).
assert (HU02 : f u0 = inner u u0).
rewrite <- Heq in H1.
apply H1.
trivial.
rewrite HU02.
assert (HU03 : Rabs (inner u u0) norm u × norm u0).
apply Cauchy_Schwartz_with_norm.
apply Rmult_le_reg_r with (norm u0).
assert (Hvnz : u0 zero).
intro.
absurd (u0 zero).
intuition.
trivial.
apply norm_gt_0.
trivial.
field_simplify.
assert ( x, x / 1 = x).
intro x.
field.
repeat (rewrite H4).
rewrite Rmult_comm.
field_simplify in HU03.
trivial.
assert (Hvnz : u0 zero).
trivial.
apply Rgt_not_eq.
apply Rlt_gt.
apply norm_gt_0.
trivial.
assert (RaN : Rabs (f u0) = norm (f u0)).
unfold norm; simpl.
reflexivity.
rewrite RaN in HU0.
apply (Rmult_le_compat_r (norm u0)
                         (norm (f u0) / norm u0)
                         (norm u)) in HU0.
field_simplify in HU0.
assert (Hx1 : x, x / 1 = x).
intro x; field.
repeat (rewrite Hx1 in HU0).
rewrite Rmult_comm.
trivial.
apply Rgt_not_eq.
apply Rlt_gt.
apply norm_gt_0.
trivial.
apply norm_ge_0.
simpl.
apply is_finite_correct in Hfin.
destruct Hfin as (y,Hy).
absurd (Rbar_lt (Finite y) p_infty).
apply Rbar_le_not_lt.
rewrite Hy.
apply Rbar_le_refl.
intuition.
apply is_finite_correct in Hfin.
destruct Hfin as (y,Hy).
absurd (Rbar_lt m_infty (Finite y)).
apply Rbar_le_not_lt.
rewrite Hy.
apply Rbar_le_refl.
simpl.
trivial.
apply Rbar_le_antisym; trivial.
Qed.

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 phi f = norm (tau f).
Proof.
intros f Hd Hd0.
destruct Hd.
apply Riesz_Frechet_moreover1_nzero_phi; trivial.
apply Riesz_Frechet_moreover1_zero_phi; trivial.
Qed.

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)))
     lin_map tau.
Proof.
intros H HhH; split.
intros x y.
apply Riesz_Frechet_uniqueness_phi with (plus x y).
apply (iota_correct (fun u : Ephi u v0 : E, phi v0
                                  (plus x y) v0 = inner u v0)).
apply Riesz_Frechet_strong_phi.
apply HhH.
trivial.
split.
replace (tau y) with (opp (opp (tau y))).
apply (cms_minus m_C).
apply phi_tau.
trivial.
trivial.
apply (cms_opp m_C).
apply phi_tau.
trivial.
trivial.
rewrite opp_opp.
reflexivity.
intros v Hv.
rewrite inner_plus_l.
apply trans_eq with (x v + y v).
reflexivity.
f_equal.
apply (iota_correct (fun u : Ephi u v0 : E,
                              phi v0 x v0 = inner u v0)).
apply Riesz_Frechet_strong_phi; trivial.
trivial.
apply (iota_correct (fun u : Ephi u v0 : E,
                              phi v0 y v0 = inner u v0)).
apply Riesz_Frechet_strong_phi.
trivial.
trivial.
trivial.
intros l x.
apply Riesz_Frechet_uniqueness_phi with (scal l x).
apply (iota_correct (fun u : Ephi u v0 : E,
                     phi v0 (scal l x) v0 = inner u v0)).
apply Riesz_Frechet_strong_phi.
trivial.
trivial.
split.
apply m_C.
apply phi_tau.
trivial. trivial.
intros v Hv.
rewrite inner_scal_l.
apply trans_eq with (l×x v).
reflexivity.
f_equal.
apply (iota_correct (fun u : Ephi u v0 : E,
                         phi v0 x v0 = inner u v0)).
apply Riesz_Frechet_strong_phi.
trivial.
trivial.
trivial.
Qed.

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 phi.
Hypothesis phi_m : compatible_ms phi.
Hypothesis Hba : bound_bilin_map a M.
Hypothesis Hca : is_coercive a alpha.

Definition sol_lin_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) ⇒
  (Hierarchy.iota (fun u : Ephi 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).
Proof.
intros f HdH Hd.
unfold Tau.
assert (H : ! (w:E), phi w (v:E),
      phi v f v = inner w v).
apply Riesz_Frechet_strong_phi; trivial.
destruct H as (w,H).
generalize H.
intros H'.
apply (iota_elim _ _) in H.
rewrite H.
apply H'.
Qed.

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)).
Proof.
intros C Halpha rho Hrho.
assert (HR : (-(alpha×alpha)/(C×C)) + ((Rsqr ((rho×C) - (alpha/C))) + 1)
       =
        1 - 2 × rho × alpha + rho × rho × C × C).
rewrite Rsqr_minus.
assert (Hra : 2 × (rho × C) × (alpha / C) = 2×rho×alpha).
rewrite Rmult_assoc.
assert (Hra2 : (Rmult (Rmult rho C) (Rdiv alpha C))
               =
               (Rmult rho (Rmult C (Rdiv alpha C)))).
ring.
rewrite Hra2.
assert (Hra3 : Rdiv alpha C = Rmult alpha (Rinv C)).
field.
apply Rgt_not_eq.
apply Rlt_gt.
apply Rlt_le_trans with alpha.
apply Halpha.
apply Halpha.
rewrite Hra3.
assert (Hra4 : (C × (alpha × / C)) = alpha).
field.
apply Rgt_not_eq.
apply Rlt_gt.
apply Rlt_le_trans with alpha.
apply Halpha.
apply Halpha.
trivial.
rewrite Hra4.
rewrite Rmult_assoc.
reflexivity.
rewrite Hra.
ring_simplify.
assert (Hp : r r1 r2, r1 = r2 r1 + r = r2 + r).
intros r r1 r2 Heq.
rewrite Heq; reflexivity.
apply Hp.
rewrite Rsqr_mult.
assert (Hqd : (alpha × alpha) / (C × C)
       = (alpha / C).
rewrite Rsqr_div'.
reflexivity.
rewrite <- Hqd.
rewrite Rplus_comm.
rewrite <- Rplus_assoc.
assert (Aa : alpha × alpha / (C × C)
      + - (alpha × alpha) / (C × C) = 0).
field.
apply Rgt_not_eq.
apply Rlt_gt.
apply Rlt_le_trans with alpha.
apply Halpha.
apply Halpha.
rewrite Aa.
ring_simplify.
assert (Hpowr : Rsqr rho = pow rho (S (S O))).
unfold Rsqr.
ring_simplify.
reflexivity.
assert (Hpowc : Rsqr C = pow C (S (S O))).
unfold Rsqr.
ring_simplify.
reflexivity.
rewrite Hpowr.
rewrite Hpowc.
reflexivity.
rewrite <- HR.
rewrite <- Rplus_assoc.
rewrite Rplus_comm.
rewrite <- Rplus_assoc.
apply Rplus_le_le_0_compat.
assert (H2 : (alpha × alpha) / (C × C) 1).
apply Rmult_le_reg_r with (C×C).
apply Rlt_0_sqr.
trivial.
apply Rgt_not_eq.
apply Rlt_gt.
apply Rlt_le_trans with alpha.
apply Halpha.
apply Halpha.
field_simplify; trivial.
assert (Hd1 : x, x / 1 = x).
intros x.
field.
repeat (rewrite Hd1).
assert (Hpowc : Rsqr C = pow C (S (S O))).
unfold Rsqr.
ring_simplify.
reflexivity.
assert (Hpowa : Rsqr alpha = pow alpha (S (S O))).
unfold Rsqr.
ring_simplify.
reflexivity.
rewrite <- Hpowc. rewrite <- Hpowa.
apply Rsqr_le_abs_1.
unfold Rabs.
destruct (Rcase_abs alpha).
absurd (0 < alpha); trivial.
apply Rle_not_gt.
auto with real.
trivial.
apply Halpha.
destruct (Rcase_abs C).
absurd (0 < C); trivial.
apply Rle_not_gt.
auto with real.
trivial.
apply Rlt_le_trans with alpha.
apply Halpha.
apply Halpha.
apply Halpha.
apply Rgt_not_eq.
apply Rlt_gt.
apply Rlt_le_trans with alpha.
apply Halpha.
apply Halpha.
apply Rplus_le_reg_r with (alpha × alpha / (C × C)).
ring_simplify.
rewrite Rdiv_opp_l.
ring_simplify.
trivial.
apply Rle_0_sqr.
Qed.

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).
Proof.
intros C Halpha rho Hrho.
assert (Hc : C 0).
replace C with (0 + C).
apply tech_Rplus.
auto with real.
apply Rlt_le_trans with alpha.
apply Halpha.
apply Halpha.
ring.
split.
apply sqrt_pos.
assert ((rho×rho×C×C < (2×rho×alpha))).
rewrite (Rmult_comm 2 rho).
rewrite (Rmult_assoc (Rmult rho rho) C).
assert (H : (Rmult (Rmult rho rho) (Rmult C C))
       = Rmult rho (Rmult rho (Rmult C C))).
ring.
rewrite H.
assert (H0 : rho × 2 × alpha = Rmult rho (Rmult 2 alpha)).
ring.
rewrite H0.
clear H.
clear H0.
apply Rmult_lt_compat_l.
intuition.
apply Rmult_lt_reg_r with (/(C×C)).
apply Rinv_0_lt_compat.
apply Rlt_0_sqr.
trivial.
field_simplify.
assert (Hcarre : C ^ 2 = C × C).
field.
rewrite Hcarre.
clear Hcarre.
apply Hrho.
trivial. trivial.
assert (H' : 1 - 2 × rho × alpha + rho × rho × C × C < 1).
assert (H0 : (1 - (2×rho×alpha)) + rho × rho × C × C
           =
            Rplus 1 (Rplus (-2×rho×alpha) (rho×rho×C×C))).
ring_simplify.
assert (Hp : r r1 r2, r1 = r2 r1 + r = r2 + r).
intros r r1 r2 Heq.
rewrite Heq; reflexivity.
apply Hp.
ring_simplify.
reflexivity.
rewrite H0.
replace 1 with (Rplus 1 0) at 2.
apply Rplus_lt_compat_l.
apply Rplus_lt_reg_r with (2 × rho × alpha).
rewrite Rplus_comm.
rewrite <- Rplus_assoc.
ring_simplify.
ring_simplify in H.
trivial.
ring.
rewrite <- sqrt_1 at 2.
apply sqrt_lt_1_alt.
split.
assert (HR : (-(alpha×alpha)/(C×C)) + ((Rsqr ((rho×C) - (alpha/C))) + 1)
       =
        1 - 2 × rho × alpha + rho × rho × C × C).
rewrite Rsqr_minus.
assert (Hra : 2 × (rho × C) × (alpha / C) = 2×rho×alpha).
rewrite Rmult_assoc.
assert (Hra2 : (Rmult (Rmult rho C) (Rdiv alpha C))
               =
               (Rmult rho (Rmult C (Rdiv alpha C)))).
ring.
rewrite Hra2.
assert (Hra3 : Rdiv alpha C = Rmult alpha (Rinv C)).
field.
trivial.
rewrite Hra3.
assert (Hra4 : (C × (alpha × / C)) = alpha).
field.
trivial.
rewrite Hra4.
rewrite Rmult_assoc.
reflexivity.
rewrite Hra.
ring_simplify.
assert (Hp : r r1 r2, r1 = r2 r1 + r = r2 + r).
intros r r1 r2 Heq.
rewrite Heq; reflexivity.
apply Hp.
rewrite Rsqr_mult.
assert (Hqd : (alpha × alpha) / (C × C)
       = (alpha / C).
rewrite Rsqr_div'.
reflexivity.
trivial.
rewrite <- Hqd.
rewrite Rplus_comm.
rewrite <- Rplus_assoc.
assert (Aa : alpha × alpha / (C × C)
      + - (alpha × alpha) / (C × C) = 0).
field.
trivial.
rewrite Aa.
ring_simplify.
assert (Hpowr : Rsqr rho = pow rho (S (S O))).
unfold Rsqr.
ring_simplify.
reflexivity.
assert (Hpowc : Rsqr C = pow C (S (S O))).
unfold Rsqr.
ring_simplify.
reflexivity.
rewrite Hpowr.
rewrite Hpowc.
reflexivity.
apply comp_lm_aux_phi.
trivial.
trivial.
trivial.
Qed.

Theorem Lax_Milgram_115
   (f:topo_dual E):
   u : E, alpha*(Rsqr (norm u)) ((a u) u).
Proof.
intros u.
unfold is_coercive in Hca.
unfold Rsqr.
rewrite <- Rmult_assoc.
apply (proj2 Hca).
Qed.

Theorem Lax_Milgram_116_phi :
                u : E, operator_norm_phi phi (A u) M*(norm u).
Proof.
intros u.
unfold operator_norm_phi.
destruct (Is_only_zero_set_dec_phi E).
unfold Lub_Rbar.
destruct (ex_lub_Rbar
 (fun x : R u0 : Hilbert_NormedModule E,
     u0 zero phi u0 x = (norm (A u u0) / norm u0))).
simpl.
unfold is_lub_Rbar in i.
unfold is_ub_Rbar in i.
destruct i.
assert (HM : M', M' = M×norm u).
(M×norm u).
reflexivity.
destruct HM as (N,HN).
rewrite <- HN.
assert (H' : Rbar_le x N).
apply H0.
intros x0 HH.
simpl.
destruct HH as (u0,(Hu01,(Hu00,Hu02))).
rewrite Hu02.
rewrite HN.
apply Rmult_le_reg_r with (norm u0).
apply norm_gt_0; trivial.
replace (norm ((A u) u0)
        / norm u0 × norm u0) with
        (norm ((A u) u0)).
destruct Hba as (Hba1,(Hba2,Hba3)).
replace ((A u) u0) with (a u u0).
apply Hba3.
apply A_bil.
field.
assert (Hg : 0 < norm u0).
apply norm_gt_0; trivial.
apply Rgt_not_eq.
apply Rlt_gt; trivial.
unfold Rbar_le in H'.
destruct x.
trivial.
simpl.
rewrite HN.
replace 0 with (0×0) by ring.
apply Rmult_le_compat; trivial.
apply Rle_refl.
apply Rle_refl.
apply (proj1 (proj2 Hba)).
apply norm_ge_0.
simpl.
replace 0 with (0×0) by ring.
rewrite HN.
apply Rmult_le_compat; trivial.
apply Rle_refl.
apply Rle_refl.
apply (proj1 (proj2 Hba)).
apply norm_ge_0.
simpl.
replace 0 with (0×0) by ring.
apply Rmult_le_compat; trivial.
apply Rle_refl.
apply Rle_refl.
apply (proj1 (proj2 Hba)).
apply norm_ge_0.
Qed.

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))).
Proof.
intros HdD HD u Hu.
apply Ropp_le_contravar.
apply Rle_trans with (a u u).
apply Lax_Milgram_115.
apply f.
assert (H : (A u) u = inner (Tau (A u)) u).
unfold Tau.
assert (H0 : ! (u0:E), phi u0 (v:E),
             phi v ((A u) v = inner u0 v)).
apply Riesz_Frechet_strong_phi; trivial.
destruct H0 as (w,H0).
assert (H0' : Hierarchy.iota (fun u0 : Ephi u0 v : E, phi v
       ((A u) v = inner u0 v)) = w).
apply iota_elim.
trivial.
rewrite H0'.
apply H0.
trivial.
rewrite <- H.
assert (Hr : a u u = (A u) u).
apply A_bil.
rewrite Hr.
apply Rle_refl.
Qed.

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).
Proof.
intros HH HD u.
apply Rle_trans with (operator_norm_phi phi (A u)).
unfold Tau.
rewrite (Riesz_Frechet_moreover1_phi phi).
apply Rle_refl.
trivial.
trivial.
try assumption.
trivial.
trivial.
apply Lax_Milgram_116_phi; trivial.
Qed.

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, (sol_lin_pb_phi f u))).
Proof.
intros Hd Hdec H.
destruct H as (u,H).
u.
assert (HA : v, (A u) v = a u v).
intros v.
symmetry.
apply A_bil.
unfold unique.
split.
unfold sol_lin_pb_phi.
split.
apply H.
intros v phi_V.
assert (H1 : ! (w:E), phi w (v:E),
      phi v f v = inner w v).
apply Riesz_Frechet_strong_phi; try assumption.
intro xx.
trivial.
trivial.
destruct H1 as (uf,Huf).
assert (Huf' : Hierarchy.iota (fun w : Ephi w v0 : E, phi v0
                                  f v0 = inner w v0) = uf).
apply iota_elim.
trivial.
unfold Tau in H.
rewrite Huf' in H.
assert (H2 : ! (w:E), phi w (v:E),
      phi v (A u) v = inner w v).
apply Riesz_Frechet_strong_phi; trivial.
trivial.
destruct H2 as (uA,HuA).
assert (HuA' : Hierarchy.iota (fun w : Ephi w v0 : E, phi v0
                                           (A u) v0 = inner w v0) = uA).
apply iota_elim.
trivial.
assert (Haf : uA = uf).
rewrite <- HuA'.
destruct H as (H,Hun).
rewrite <- (proj2 H).
trivial.
assert (HH1 : a u v = inner uA v).
rewrite <- HA.
apply HuA.
trivial.
assert (HH2 : f v = inner uA v).
rewrite Haf.
apply Huf.
trivial.
rewrite HH1 HH2.
reflexivity.
intros x' Hx'.
destruct H as (H,Hun).
apply Hun.
unfold sol_lin_pb_phi in Hx'.
unfold Tau.
assert (H1 : ! (w:E), phi w (v:E),
      phi v ((A u) v = inner w v)).
apply Riesz_Frechet_strong_phi; trivial.
split.
exact (proj1 Hx').
assert (H2 : ! (w:E), phi w (v:E),
      phi v f v = inner w v).
apply Riesz_Frechet_strong_phi; trivial.
destruct H1 as (wa,H1).
destruct H2 as (wf,H2).
assert (H1' : Hierarchy.iota (fun u0 : Ephi u0
        v : E, phi v ((A u) v = inner u0 v)) = wa).
apply iota_elim.
trivial.
assert (H2' : Hierarchy.iota (fun u0 : Ephi u0
        v : E, phi v f v = inner u0 v) = wf).
apply iota_elim.
trivial.
rewrite H2'.
assert ( v: E, phi v f v = inner wf v).
intros v'.
apply H2.
assert ( v: E, phi v a x' v = inner wf v).
intros v' Hv'.
rewrite (proj2 Hx').
apply H0.
trivial.
trivial.
assert ((Hierarchy.iota (fun u0 : Ephi u0 v : E, phi v
   ((A x') v = inner u0 v))) = wf).
apply iota_elim.
assert (H5 : ! (w:E), phi w (v:E),
             phi v ((A x') v = inner w v)).
apply Riesz_Frechet_strong_phi; trivial.
unfold unique; split.
split.
rewrite <- H2'.
assert (Hphi: ! (w:E), phi w (v:E),
      phi v f v = inner w v).
apply Riesz_Frechet_strong_phi; trivial.
destruct Hphi as (w,Hphi).
generalize Hphi.
intros Hphi'.
apply (iota_elim _ _) in Hphi.
rewrite Hphi.
apply Hphi'.
intros v Hv.
transitivity (a x' v).
symmetry.
apply A_bil.
apply H3.
trivial.
intros x'0 Hh.
destruct H5 as (y,H5).
destruct H5 as (H51,H52).
assert (y = x'0).
apply H52.
trivial.
assert (y = wf).
apply H52.
split.
rewrite <- H2'.
assert (Hphi: ! (w:E), phi w (v:E),
      phi v f v = inner w v).
apply Riesz_Frechet_strong_phi; trivial.
destruct Hphi as (w,Hphi).
generalize Hphi.
intros Hphi'.
apply (iota_elim _ _) in Hphi.
rewrite Hphi.
apply Hphi'.
intros v Hv.
transitivity (a x' v).
symmetry.
apply A_bil.
apply H3.
trivial.
rewrite <- H5, H4.
reflexivity.
trivial.
Qed.

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, (sol_lin_pb_phi f u)).
Proof.
intros Hr Hd Hd0 H.
destruct H as (u,H).
apply Lax_Milgram'_aux1_phi; trivial.
u.
unfold g_map_app in H.
unfold minus in H.
destruct H as (H,H2).
rewrite <- plus_assoc in H.
destruct H as (Pu,H).
symmetry in H.
assert (Hu0 : plus u zero = u).
rewrite plus_zero_r. reflexivity.
rewrite <- Hu0 in H at 1.
generalize H; clear H; move⇒ /plus_reg_l H.
clear Hu0.
symmetry in H.
assert (H0 : minus (scal r (Tau f))
              (scal r (Tau (A u))) = zero).
unfold minus.
rewrite plus_comm.
trivial.
assert (Hm : minus (scal r (Tau f))
        (scal r (Tau (A u))) =
       scal r (minus (Tau f) (Tau (A u)))).
rewrite scal_minus_distr_l.
reflexivity.
rewrite Hm in H0.
assert (minus (Tau f) (Tau (A u)) = zero).
destruct (is_zero_dec
          (minus (Tau f) (Tau (A u)))).
trivial.
absurd (norm
       (scal r (minus (Tau f)
        (Tau (A u))))= 0).
apply Rgt_not_eq.
apply Rlt_gt.
rewrite norm_scal_R.
apply Rmult_lt_0_compat.
unfold abs.
simpl.
unfold Rabs.
destruct (Rcase_abs r).
absurd (0 < r).
apply Rle_not_gt.
auto with real.
apply Hr.
apply Hr.
apply norm_gt_0.
trivial.
rewrite H0.
rewrite norm_zero.
reflexivity.
split.
unfold minus in H1.
split; try assumption.
apply plus_reg_r with (opp (Tau (A u))).
rewrite plus_opp_r.
symmetry.
trivial.
intros x' Hbil.
apply H2.
split.
exact (proj1 Hbil).
rewrite (proj2 Hbil).
rewrite <- plus_assoc.
rewrite plus_opp_l.
rewrite plus_zero_r.
reflexivity.
Qed.

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')).
Proof.
intros Hd Hd0 Hr v v'.
assert (H :(norm (minus (g_map_app r f v)
                     (g_map_app r f v'))
         = (plus (norm (minus v v') (-
   2 × r × inner (Tau (A (minus v v'))) (minus v v') +
   r × r × (norm (Tau (A (minus v v')))))).
assert (Haux : minus (g_map_app r f v)
                     (g_map_app r f v')
              = (minus (minus v v')
               (scal r (Tau (A (minus v v')))))).
unfold g_map_app.
unfold minus.
rewrite opp_plus.
rewrite opp_plus.
rewrite <- plus_assoc.
rewrite <- plus_assoc.
rewrite <- plus_assoc.
rewrite <- plus_assoc.
rewrite plus_comm.
rewrite (plus_comm (opp v') _).
assert (Hp1 : a b, plus (plus a b) v
              = plus a (plus b v)).
intros.
rewrite plus_assoc.
reflexivity.
rewrite Hp1.
rewrite Hp1.
rewrite Hp1.
rewrite (plus_assoc v (opp v') _).
assert (Hp2 : a b, plus a (plus b
          (plus (opp v') v)) =
          plus (plus a b) (plus (opp v') v)).
intros.
rewrite plus_assoc. reflexivity.
rewrite Hp2.
rewrite Hp2.
rewrite plus_comm.
rewrite (plus_comm (opp v') v).
assert (Hpaux : ((plus (opp (scal r (Tau (A v))))
     (plus (scal r (Tau f))
        (plus (opp (opp (scal r (Tau (A v')))))
           (opp (scal r (Tau f)))))))
   = (opp (scal r (Tau (A (plus v (opp v'))))))).
rewrite plus_assoc.
rewrite opp_opp.
rewrite (plus_comm _ (opp (scal r (Tau f)))).
assert (Hg : a b c d : E, plus (plus a b) (plus c d)
                           = plus (plus a d) (plus b c)).
intros.
rewrite plus_assoc.
rewrite plus_assoc.
rewrite plus_comm.
rewrite (plus_comm a0 d).
rewrite <- (plus_assoc d a0 b).
rewrite <- (plus_assoc d _ _).
reflexivity.
rewrite Hg.
rewrite plus_opp_r.
rewrite plus_zero_r.
replace (opp (scal r (Tau (A (plus v (opp v'))))))
        with
        (scal r (Tau (A (opp (plus v (opp v')))))).
replace ((opp (scal r (Tau (A v)))))
        with
        (scal r (Tau (A (opp v)))).
rewrite opp_plus.
rewrite opp_opp.
assert (ALf : lin_map A).
apply A.
destruct ALf as (Alf1,Alf2).
assert (H : lin_map Tau).
apply Riesz_Frechet_moreover2_phi; trivial.
destruct H as (Hl1,Hl2).
rewrite Alf1.
rewrite Hl1.
rewrite scal_distr_l.
reflexivity.
rewrite <- scal_opp_one.
rewrite scal_assoc.
assert (H : lin_map Tau).
apply Riesz_Frechet_moreover2_phi; trivial.
destruct H as (Hl1,Hl2).
rewrite <- Hl2.
rewrite <- Hl2.
assert (ALf : lin_map A).
apply A.
destruct ALf as (Alf1,Alf2).
rewrite <- Alf2.
rewrite <- Alf2.
assert (Hsr : (scal r (opp v))
        = (scal (mult (opp one) r) v)).
rewrite <- scal_assoc.
rewrite scal_opp_one.
rewrite scal_opp_r.
reflexivity.
rewrite Hsr.
reflexivity.
rewrite <- scal_opp_r.
rewrite <- scal_opp_one.
replace ((scal (opp one) (Tau (A (plus v (opp v'))))))
        with
        ((Tau (scal (opp one) (A (plus v (opp v')))))).
assert (H : lin_map Tau).
apply Riesz_Frechet_moreover2_phi; trivial.
destruct H as (Hl1,Hl2).
replace (Tau (A (opp (plus v (opp v')))))
     with (Tau (scal (opp one) (A (plus v (opp v'))))).
reflexivity.
clear Hp1 Hp2 Hg.
assert (Hlb : l y, scal l (A y)
                      = A (scal l y)).
intros l y.
apply clm_eq_ext.
intro x.
replace ((A (scal l y)) x) with (a (scal l y) x).
replace ((scal l (A y) x)) with (scal l (a y x)).
destruct Hba as (Hba1,Hba2).
symmetry; apply Hba1.
replace (a y x) with ((A y) x).
reflexivity.
symmetry.
apply A_bil.
assert (HAa : (A (scal l y)) x = a (scal l y) x).
symmetry; apply A_bil.
rewrite HAa.
reflexivity.
symmetry.
rewrite Hlb.
rewrite scal_opp_one.
reflexivity.
assert (HL : lin_map Tau).
apply Riesz_Frechet_moreover2_phi; trivial.
destruct HL as (Hl1,Hl2).
rewrite Hl2.
reflexivity.
rewrite Hpaux.
reflexivity.
rewrite Haux.
transitivity ((Hnorm (minus (minus v v')
              (scal r (Tau (A (minus v v'))))))*
              (Hnorm (minus (minus v v')
              (scal r (Tau (A (minus v v'))))))).
unfold norm; simpl.
reflexivity.
rewrite squared_norm.
rewrite square_expansion_minus.
rewrite <- squared_norm.
replace (Hnorm (minus v v')
       × Hnorm (minus v v')) with
         ((norm (minus v v')).
replace ((norm (minus v v') -
   2 × inner (minus v v') (scal r (Tau (A (minus v v')))) +
       inner (scal r (Tau (A (minus v v'))))
     (scal r (Tau (A (minus v v')))))
  with
   (plus ((norm (minus v v'))
     (- 2 × inner (minus v v') (scal r (Tau (A (minus v v')))) +
       inner (scal r (Tau (A (minus v v'))))
     (scal r (Tau (A (minus v v')))))).
apply Rplus_eq_compat_l.
rewrite <- squared_norm.
replace (Hnorm (scal r (Tau (A (minus v v')))))
      with (r× (Hnorm (Tau (A (minus v v'))))).
replace (r × Hnorm (Tau (A (minus v v'))) ×
        (r × Hnorm (Tau (A (minus v v')))))
       with (r × r × (norm (Tau (A (minus v v')))).
rewrite Rplus_comm.
rewrite (Rplus_comm (-2 × r × inner (Tau (A
                 (minus v v'))) (minus v v')) _ ).
apply Rplus_eq_compat_l.
rewrite inner_scal_r.
rewrite inner_sym.
ring.
ring_simplify.
replace (Hnorm (Tau (A (minus v v'))) ^ 2)
   with ((norm (Tau (A (minus v v')))).
reflexivity.
unfold Rsqr.
unfold pow.
ring_simplify.
reflexivity.
replace r with (Rabs r) at 1.
rewrite Hnorm_scal.
reflexivity.
unfold Rabs.
destruct (Rcase_abs r).
absurd (r < 0).
apply Rle_not_lt, Rlt_le, Hr.
trivial.
reflexivity.
rewrite Rplus_assoc.
apply Rplus_eq_compat_l.
ring.
reflexivity.
intros Hv Hv'.
rewrite H.
assert (H2 : (1 - 2 × r × alpha + r × r × M × M)
            × (norm (minus v v')
           = plus (Rsqr (norm (minus v v')))
             (- 2×r×alpha*(Rsqr (norm (minus v v')))
              + r×r×M×M*(Rsqr (norm (minus v v'))))).
rewrite Rmult_plus_distr_r.
rewrite Rplus_comm.
rewrite <- Rplus_assoc.
rewrite (Rplus_comm
        ((norm (minus v v')
         + -2 × r × alpha × (norm (minus v v')) _).
apply Rplus_eq_compat_l.
rewrite Rmult_plus_distr_r.
ring_simplify.
reflexivity.
rewrite H2.
apply Rplus_le_compat_l.
apply Rplus_le_compat.
replace (-2 × r × alpha × (norm (minus v v'))
    with ((-2×r)*(alpha ×(norm (minus v v'))).
replace (-2 × r × inner
     (Tau (A (minus v v'))) (minus v v'))
    with
     ((2×r)*(- inner
     (Tau (A (minus v v'))) (minus v v')))
    by ring.
replace (-2 × r × (alpha × (norm (minus v v')))
    with
     ((2×r)*(-alpha × (norm (minus v v')))
    by ring.
apply Rmult_le_compat_l.
apply Rmult_le_pos.
auto with real.
apply Rlt_le, Hr.
replace (- alpha × (norm (minus v v'))
        with (- (alpha*(Rsqr (norm (minus v v'))))).
apply Lax_Milgram_117_phi; trivial.
apply (cms_minus phi_m); trivial.
ring.
replace (norm (inner (Tau (A (minus v v'))) (minus v v')))
    with (abs ((inner (Tau (A (minus v v'))) (minus v v')))).
ring.
reflexivity.
replace (r×r × (norm (Tau (A (minus v v'))))
        with
        ((r×r) × (norm (Tau (A (minus v v')))).
replace (r×r × M×M × (norm (minus v v'))
        with
        ((r×r) *(M×M × (norm (minus v v'))).
apply Rmult_le_compat_l.
apply Rle_0_sqr.
replace (M × M × (norm (minus v v'))
        with (Rsqr (M × (norm (minus v v')))).
apply sqrt_le_0.
apply Rle_0_sqr.
apply Rle_0_sqr.
repeat (rewrite sqrt_Rsqr).
apply Lax_Milgram_118_phi; trivial.
apply Rmult_le_pos.
apply Hba.
apply norm_ge_0.
apply norm_ge_0.
ring_simplify.
rewrite Rsqr_mult.
apply Rmult_eq_compat_r.
unfold pow.
replace (M×1) with M by ring.
reflexivity.
ring.
reflexivity.
Qed.

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:Ephi x))
   0 < r < ((2×alpha)/(M×M))
   (! u:E, phi u (g_map_app r f u = u)).
Proof.
intros Hd Hd0 HE Hr.
assert (HC : is_contraction_phi (g_map_app r f) phi).
unfold is_contraction_phi.
destruct (Req_dec ((1 - (2×r×alpha)) + r×r×M×M) 0).
assert ( v v', phi v phi v' Rsqr (norm (minus (g_map_app r f v) (g_map_app r f v')))
         = 0).
assert ( v v', phi v phi v' Rsqr (norm (minus (g_map_app r f v) (g_map_app r f v')))
          0).
intros v v' Hv Hv'.
replace 0 with ((1 - 2 × r × alpha + r × r × M × M)
          × Rsqr (norm (minus v v'))).
apply g_map_diff_phi; trivial.
rewrite H.
ring.
intros v v' Hv Hv'.
destruct (Req_dec (norm (minus (g_map_app r f v)
         (g_map_app r f v')) 0).
trivial.
destruct (Rlt_le_dec
     (norm (minus (g_map_app r f v)
     (g_map_app r f v')) 0).
absurd ((norm (minus (g_map_app r f v)
           (g_map_app r f v')) < 0).
apply Rle_not_gt.
apply Rle_0_sqr.
trivial.
apply Rle_le_eq.
split; trivial.
apply H0; trivial.
(1 / 2).
split.
apply Rmult_lt_reg_r with 2.
auto with real.
field_simplify.
replace (1 / 1) with 1 by field.
replace (2/1) with 2 by field.
auto with real.
unfold is_Lipschitz_phi.
split.
assert (Hstrong : 0 < 1/2).
apply Rdiv_lt_0_compat.
auto with real.
auto with real.
auto with real.
intros x1 x2 r0 Hr0 Hp1 Hp2 Hx2.
unfold ball_x in Hx2.
simpl in Hx2.
unfold hilbert.ball in Hx2.
unfold ball_y.
simpl.
unfold hilbert.ball.
specialize (H0 x1 x2).
unfold norm in H0; simpl in H0.
apply Rsqr_0_uniq in H0.
rewrite H0.
apply Rmult_lt_0_compat.
apply Rdiv_lt_0_compat.
auto with real.
auto with real.
trivial.
trivial.
trivial.
((sqrt ((1 - (2×r×alpha)) + r×r×M×M))).
split.
apply comp_lax_milgram_phi; trivial.
split.
apply (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
unfold is_Lipschitz_phi.
split.
apply comp_lax_milgram_phi; trivial.
split.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
intros x1 x2 r1 Hr0 Hp1 Hp2 Hx2.
unfold ball_x in Hx2.
simpl in Hx2.
unfold hilbert.ball in Hx2.
unfold ball_y.
simpl.
unfold hilbert.ball.
apply Rle_lt_trans with
    (sqrt (1 - 2 × r × alpha + r × r × M × M)
   × (Hnorm (minus x1 x2))).
assert (Hsq : Hnorm (minus (g_map_app r f x1)
       (g_map_app r f x2))
     = (sqrt (Rsqr (norm (minus (g_map_app r f x1)
          (g_map_app r f x2)))))).
rewrite sqrt_Rsqr.
unfold norm; simpl.
reflexivity.
apply norm_ge_0.
rewrite Hsq.
assert (Hsq2 : sqrt (1 - 2 × r × alpha + r × r × M × M)
               × Hnorm (minus x1 x2)
              =
               sqrt ((1 - 2 × r × alpha + r × r × M × M)
                     × Rsqr (Hnorm (minus x1 x2)))).
rewrite sqrt_mult_alt.
rewrite sqrt_Rsqr.
reflexivity.
assert (Hh : Hnorm (minus x1 x2) = norm (minus x1 x2)).
unfold norm; simpl; reflexivity.
rewrite Hh.
apply norm_ge_0.
apply comp_lm_aux_phi.
split.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
trivial.
rewrite Hsq2.
apply sqrt_le_1.
apply Rle_0_sqr.
apply Rmult_le_pos.
apply comp_lm_aux_phi.
split.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
trivial.
apply Rle_0_sqr.
apply g_map_diff_phi; trivial.
apply Rmult_lt_compat_l.
apply sqrt_lt_R0.
assert (0 1 - 2 × r × alpha + r × r × M × M).
apply comp_lm_aux_phi.
split.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
trivial.
apply Rdichotomy in H.
destruct H.
absurd (0 1 - 2 × r × alpha + r × r × M × M).
apply Rlt_not_le.
trivial.
trivial.
trivial.
trivial.
destruct (FixedPoint_C_phi (g_map_app r f) phi); trivial.
intros x Hx.
unfold g_map_app.
replace (scal r (Tau f)) with (opp (scal (opp r) (Tau f))).
apply (cms_minus phi_m).
apply (cms_minus phi_m).
trivial.
apply phi_m.
apply phi_Tau.
trivial.
trivial.
apply phi_m.
apply phi_Tau.
trivial. trivial.
rewrite scal_opp_l.
rewrite opp_opp; reflexivity.
intros x y _ _.
(2*(norm (minus x y)) + 1).
split.
apply Rplus_le_le_0_compat.
apply Rmult_le_pos.
auto with real.
apply norm_ge_0.
auto with real.
unfold Hierarchy.ball. simpl. unfold hilbert.ball.
unfold norm. simpl.
rewrite <- Rplus_0_r at 1.
apply Rplus_le_lt_compat.
assert (Hh : Hnorm (minus x y) = 1×Hnorm (minus x y)).
ring.
rewrite Hh.
apply Rmult_le_compat.
auto with real.
destruct (norm_ge_0 (minus x y)).
unfold norm in H. simpl in H.
auto with real.
rewrite H.
unfold norm; simpl.
auto with real.
auto with real.
ring_simplify.
auto with real.
auto with real.
apply (cms_nonempty phi_m).
x.
unfold unique.
split.
split.
exact (proj1 H).
apply eq_close.
apply (proj1 (proj2 H)).
intros y Hy.
apply eq_close.
apply close_sym.
apply (proj1 (proj2 (proj2 H))).
exact (proj1 Hy).
rewrite (proj2 Hy); apply close_refl.
Qed.

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, sol_lin_pb_phi f u
          ( u', sol_lin_pb_phi f u' u'=u).
Proof.
intros Hd Hd0.
destruct (Is_only_zero_set_dec_phi E phi).
assert (Haux : r, 0 < r < ((2×alpha)/(M×M))
              ! u:E, (sol_lin_pb_phi f u)).
intros r Hr.
apply Lax_Milgram'_aux2_phi with r; trivial.
trivial.
apply Lax_Milgram'_aux3_phi; trivial.
specialize (Haux (alpha / (M × M))).
assert (Haux' : ! u : E, sol_lin_pb_phi f u).
apply Haux.
split.
apply Rdiv_lt_0_compat.
exact (proj1 Hca).
apply Rmult_lt_0_compat.
apply Rlt_le_trans with alpha.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
apply Rlt_le_trans with alpha.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
replace (alpha / (M × M)) with (1 × (alpha / (M × M))).
replace (2 × alpha / (M × M)) with (2× (alpha / (M × M))).
apply Rmult_lt_compat_r.
apply Rdiv_lt_0_compat.
exact (proj1 Hca).
apply Rmult_lt_0_compat.
apply Rlt_le_trans with alpha.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
apply Rlt_le_trans with alpha.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
auto with real.
replace (alpha / (M × M)) with (alpha × (/ (M×M))).
replace (2× alpha / (M × M)) with (2× alpha × (/ (M×M))).
rewrite Rmult_assoc.
reflexivity.
field.
assert (HM : 0 < M).
apply Rlt_le_trans with alpha.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
apply Rgt_not_eq.
apply Rlt_gt.
trivial.
field.
assert (HM : 0 < M).
apply Rlt_le_trans with alpha.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
apply Rgt_not_eq.
apply Rlt_gt.
trivial.
field.
assert (HM : 0 < M).
apply Rlt_le_trans with alpha.
exact (proj1 Hca).
apply coercivity_le_continuity_phi with phi a; trivial.
apply Rgt_not_eq.
apply Rlt_gt.
trivial.
destruct Haux' as (u,Hu).
unfold unique in Hu.
u.
split.
exact (proj1 Hu).
intros u' Hu'.
symmetry.
apply (proj2 Hu).
trivial.
zero.
split.
unfold sol_lin_pb_phi.
split.
apply (cms_zero phi_m).
trivial.
intros v Hv.
apply Is_only_zero_set_correct1_phi with E phi v in i.
rewrite i.
assert (a zero zero = a (scal zero zero) zero).
rewrite scal_zero_l.
reflexivity.
rewrite H.
replace (a (scal zero zero) zero)
        with (scal zero (a zero zero)).
rewrite scal_zero_l.
assert (lin_map f).
apply f.
destruct H0 as (H01,H02).
replace (f zero) with (f (scal zero zero)).
transitivity (scal zero (f zero)).
rewrite scal_zero_l.
reflexivity.
symmetry.
apply H02.
rewrite scal_zero_l.
reflexivity.
symmetry.
apply Hba.
trivial.
intros u' Hu'.
apply Is_only_zero_set_correct1_phi with E phi u' in i.
rewrite i.
reflexivity.
exact (proj1 Hu').
Qed.

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, sol_lin_pb_phi f u
          ( u', sol_lin_pb_phi f u' u'=u)
           norm u /alpha × norm f.
Proof.
intros Hd Hd0.
assert (H' : u : E,
             sol_lin_pb_phi f u
             ( u' : E, sol_lin_pb_phi f u' u' = u)).
apply Lax_Milgram''_phi; trivial.
destruct H' as (u,(He,Hu)).
u.
split; trivial.
split; trivial.
destruct (is_zero_dec u).
+ rewrite H.
  rewrite norm_zero.
  destruct Hca as (Hca',_).
  apply Rmult_le_pos.
  assert (Hsp : 0 < / alpha).
  apply Rinv_0_lt_compat.
  trivial.
  auto with real.
  apply norm_ge_0.
+ assert (alpha*(Rsqr (norm u)) norm f × norm u).
  apply Rle_trans with (norm (f u)).
  apply Rle_trans with (norm (a u u)).
  destruct Hca as (Hca1,Hca2).
  specialize (Hca2 u).
  unfold norm; simpl.
  unfold abs; simpl.
  unfold Rsqr.
  unfold norm in Hca2; simpl in Hca2.
  rewrite <- Rmult_assoc.
  apply Rle_trans with (a u u).
  exact Hca2.
  unfold Rabs.
  destruct (Rcase_abs (a u u)).
  apply Rle_trans with 0.
  auto with real.
  apply Ropp_0_ge_le_contravar.
  apply Rle_ge.
  auto with real.
  right; reflexivity.
  specialize ((proj2 He) u).
  intros Heu.
  specialize (Heu (proj1 He)).
  rewrite Heu.
  apply Rle_refl.
  apply operator_norm_estimation.
  apply Rmult_le_reg_l with (norm u).
  apply norm_gt_0; trivial.
  rewrite (Rmult_comm (norm u) (/ alpha × norm f)).
  apply Rmult_le_reg_l with alpha.
  apply Hca.
  assert (Ha : alpha × (/ alpha × norm f × norm u)
               = norm f × norm u).
  field.
  apply Rgt_not_eq.
  apply Rlt_gt.
  apply Hca.
  rewrite Ha.
  intuition.
Qed.

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 phi.
Hypothesis phi_m : compatible_ms phi.
Hypothesis Hba : bound_bilin_map 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, sol_lin_pb_phi a phi f u
          ( u', sol_lin_pb_phi a phi f u' u'=u)
           norm u /alpha × norm f.
Proof.
intros Hd Hd0.
assert (Hbil : ! (A:(clm E (topo_dual E))),
              (u v:E), a u v = (A u) v).
apply bound_blm_representation with M.
trivial.
destruct Hbil as (A0,Hbil).
apply Lax_Milgram_Aux_phi with M A0; try assumption.

Qed.

End Lax_Milgram.

Section LM_True.

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.

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, sol_lin_pb_phi a (fun _True) f u
          ( u', sol_lin_pb_phi a (fun _True) f u' u'=u)
           norm u /alpha × norm f.
Proof.
intros Hd HD.
assert (Hdd : decidable (f_phi_neq_zero (fun _True) f)).
unfold f_phi_neq_zero.
destruct (Hd f).
left.
destruct H as (u,H).
u; now split.
right.
intros (u,J).
apply H.
u; intuition.
assert (Hmc : my_complete (fun x : ETrue)).
easy.
assert (Hmm : compatible_ms (fun x : ETrue)).
split; try split; try easy.
generalize (Lax_Milgram_phi a M alpha (fun x : ETrue)
 Hmc Hmm Hba Hca) ⇒ LMP.
specialize (LMP f).
assert (Haa : ( f0 : topo_dual E,
       decidable (f_phi_neq_zero (fun _ : ETrue) f0))).
intros g.
destruct (Hd g).
destruct H as (v,H).
left.
v.
split; try easy.
right.
intro Hh.
apply H.
destruct Hh as (h,(_,Hhh)).
now h.
specialize (LMP Haa).
assert (HD' : ( (f0 : topo_dual E) (u : E) (eps : posreal),
       decidable
         ( w : E,
            (ker f0 w True) norm (minus u w) < eps))).
intros g u e.
destruct (HD g u e).
left.
destruct H as (w,H).
w.
split; try intuition.
right.
intro Hh.
apply H.
destruct Hh as (w,Hh).
w.
intuition.
specialize (LMP HD').
trivial.
Qed.

End LM_True.