Library Top.compatible

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 Export Reals Coquelicot.Coquelicot.

AbelianGroup-compatibility

Section AboutCompatibleG.

Context {E : AbelianGroup}.

Definition compatible_g (P: E Prop) : Prop :=
   ( (x y:E), P x P y P (plus x (opp y)))
      ( (x:E), P x).

Lemma compatible_g_zero: P, compatible_g P P zero.

Lemma compatible_g_opp: P x, compatible_g P
     P x P (opp x).

Lemma compatible_g_plus: P x y, compatible_g P
     P x P y P (plus x y).

End AboutCompatibleG.

ModuleSpace-compatibility

Section AboutCompatibleM.

Context {E : ModuleSpace R_Ring}.

Definition compatible_m (phi:EProp):=
  compatible_g phi
  ( (x:E) (l:R), phi x phi (scal l x)).

Lemma compatible_m_zero: P, compatible_m P P zero.

Lemma compatible_m_plus: P x y, compatible_m P
     P x P y P (plus x y).

Lemma compatible_m_scal: P a y, compatible_m P
     P y P (scal a y).

Lemma compatible_m_opp: P x, compatible_m P
     P x P (opp x).

End AboutCompatibleM.

Sums and direct sums

Section Compat_m.

Context {E : ModuleSpace R_Ring}.

Variable phi:EProp.
Variable phi':EProp.

Definition m_plus (phi phi':E Prop)
   := (fun (x:E) ⇒ u u', phi u phi' u' x=plus u u').

Hypothesis Cphi: compatible_m phi.
Hypothesis Cphi': compatible_m phi'.

Lemma compatible_m_plus2: compatible_m (m_plus phi phi').

Definition direct_sumable := x, phi x phi' x x = zero.

Lemma direct_sum_eq1:
   direct_sumable
    ( u u' , phi u phi' u' plus u u' = zero u=zero u'=zero).

Lemma plus_u_opp_v : (u v : E), u = v (plus u (opp v) = zero).

Lemma plus_assoc_gen : (a b c d : E),
     plus (plus a b) (plus c d) = plus (plus a c) (plus b d).

Lemma direct_sum_eq2:
  ( u u' , phi u phi' u' plus u u' = zero u=zero u'=zero)
   ( u v u' v', phi u phi v phi' u' phi' v' plus u u' = plus v v' u=v u'=v').

Lemma direct_sum_eq3:
   ( u v u' v', phi u phi v phi' u' phi' v' plus u u' = plus v v' u=v u'=v')
      direct_sumable.

End Compat_m.