Library Algebra.ModuleSpace.ModuleSpace_compl

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
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.

Brief description

Complements on the module space algebraic structure.

Description

The ModuleSpace algebraic structure is defined in the Coquelicot library, including the canonical structure prod_ModuleSpace for the cartesian product of module spaces.
Module spaces are similar to vector spaces, except that the field of scalars is simply a ring of scalars.
For results that are only valid when the ring of scalars is commutative, or being ordered, see Algebra.ModuleSpace.ModuleSpace_R_compl where they are only stated in the case of the ring of real numbers R_Ring.

Usage

This module may be used through the import of Algebra.ModuleSpace.ModuleSpace, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

From Requisite Require Import ssr.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group Ring.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.

Section ModuleSpace_Facts.

Context {T : Type}.
Context {K : Ring}.
Context {E : ModuleSpace K}.

Lemma ms_w_zero_struct_r : zero_struct K zero_struct E.
Proof. intros HK u; rewrite -(scal_one u) (HK 1) scal_zero_l; easy. Qed.

Lemma inhabited_ms : inhabited E.
Proof. apply inhabited_g. Qed.

Lemma inhabited_fct_ms : inhabited (T E).
Proof. intros; apply inhabited_fct_g. Qed.

Lemma scal_compat :
   a b (u v : E), a = b u = v scal a u = scal b v.
Proof. intros; f_equal; easy. Qed.

Lemma scal_compat_l : a b (u : E), a = b scal a u = scal b u.
Proof. intros; f_equal; easy. Qed.

Lemma scal_compat_r : a (u v : E), u = v scal a u = scal a v.
Proof. intros; f_equal; easy. Qed.

Lemma scal_zero_rev :
   a (u : E), scal a u = 0 ¬ invertible a u = 0.
Proof.
intros a u H.
destruct (classic (invertible a)) as [[b [Hb _]] | Ha]; [right | now left].
rewrite -(scal_one u) -Hb -scal_assoc H scal_zero_r; easy.
Qed.

Lemma scal_not_zero :
   a (u : E), invertible a u 0 scal a u 0.
Proof. move=>> Ha Hu H; destruct (scal_zero_rev _ _ H); easy. Qed.

Lemma scal_reg_l :
   a1 a2 (u : E), u 0 scal a1 u = scal a2 u ¬ invertible (a1 - a2).
Proof.
intros a1 a2 u Hu H.
destruct (scal_zero_rev (a1 - a2) u) as [Ha | Ha]; try easy.
rewrite scal_minus_distr_r H minus_eq_zero; easy.
Qed.

Lemma scal_reg_r :
   a (u1 u2 : E), invertible a scal a u1 = scal a u2 u1 = u2.
Proof.
intros a u1 u2 Ha H.
destruct (scal_zero_rev a (u1 - u2)) as [Hu | Hu]; try easy.
rewrite scal_minus_distr_l H minus_eq_zero; easy.
apply minus_zero_reg; easy.
Qed.

Lemma scal_zero_compat_l : a (u : E), a = 0 scal a u = 0.
Proof. move=>> H; rewrite H; apply scal_zero_l. Qed.

Lemma scal_zero_compat_r : a (u : E), u = 0 scal a u = 0.
Proof. move=>> H; rewrite H; apply scal_zero_r. Qed.

Lemma scal_zero_reg_l :
   a1 (u : E), u 0 scal a1 u = 0 ¬ invertible a1.
Proof.
intros a1 u; rewrite -{2}(scal_zero_l u) -{2}(minus_zero_r a1).
apply scal_reg_l.
Qed.

Lemma scal_zero_reg_r :
   a (u : E), invertible a scal a u = 0 u = 0.
Proof. move=>>; erewrite <- scal_zero_r at 1; apply scal_reg_r. Qed.

Lemma scal_minus_l :
   a1 a2 (u : E), scal (a1 - a2) u = scal a1 u - scal a2 u.
Proof. intros; rewrite minus_eq scal_distr_r scal_opp_l; easy. Qed.

Lemma scal_minus_r :
   a (u1 u2 : E), scal a (u1 - u2) = scal a u1 - scal a u2.
Proof. intros; rewrite minus_eq scal_distr_l scal_opp_r; easy. Qed.

Lemma scal_opp : a (u : E), scal a u = scal (- a) (- u).
Proof. intros; rewrite scal_opp_l scal_opp_r opp_opp; easy. Qed.

Lemma convex_comb_2_eq :
   a1 a2 (u1 u2 : E),
    a1 + a2 = 1 scal a1 u1 + scal a2 u2 = scal a1 (u1 - u2) + u2.
Proof.
move=>> Ha; apply eq_sym in Ha; rewrite plus_minus_r_equiv in Ha; subst.
rewrite scal_minus_l scal_one minus_sym scal_minus_r plus_assoc; easy.
Qed.

Lemma axpy_equiv :
   {a} {u v w : E},
    invertible a w = scal a u + v u = scal (/ a) w - scal (/ a) v.
Proof.
intros a u v w Ha; split; intros H; rewrite H.
rewrite scal_distr_l scal_assoc (mult_inv_l Ha) scal_one minus_plus_r; easy.
rewrite scal_minus_distr_l 2!scal_assoc
    (mult_inv_r Ha) 2!scal_one plus_minus_l; easy.
Qed.

Lemma scal_inv :
   {a} {u v : E}, invertible a v = scal a u u = scal (/ a) v.
Proof.
move=>> Ha; rewrite -(plus_zero_r (scal _ _)).
move⇒ /(axpy_equiv Ha); rewrite scal_zero_r minus_zero_r //.
Qed.

Lemma scal_inv_equiv :
   {a} {u v : E}, invertible a v = scal a u u = scal (/ a) v.
Proof.
move=>> Ha; split. apply scal_inv; easy.
rewrite -{2}(inv_invol Ha); apply scal_inv, inv_invertible, Ha.
Qed.

Lemma scal_one_l : a (u : E), a = 1 scal a u = u.
Proof. intros; subst; apply scal_one. Qed.

Lemma scal_one_r : (a b : K), b = 1 scal a b = a.
Proof. intros; subst; apply mult_one_r. Qed.

Lemma scal_sum_distr_l :
   {n} a (u : 'E^n), scal a (sum u) = sum (scal a u).
Proof.
intros n; induction n as [| n Hn]; intros.
rewrite !sum_nil scal_zero_r; easy.
rewrite !sum_ind_l scal_distr_l Hn; easy.
Qed.

Lemma scal_sum_distr_r :
   {n} (a : 'K^n) (u : E), scal (sum a) u = sum (fun iscal (a i) u).
Proof.
intros n; induction n as [| n Hn]; intros.
rewrite !sum_nil scal_zero_l; easy.
rewrite !sum_ind_l scal_distr_r Hn; easy.
Qed.

Lemma sum_constF :
   {n} (u : E), sum (constF n u) = scal (sum (@ones _ n)) u.
Proof.
intros; rewrite scal_sum_distr_r; f_equal;
    apply extF; intro; rewrite scal_one; easy.
Qed.

End ModuleSpace_Facts.

Section Euclidean_space_Facts.

Context {K : Ring}.

Lemma sum_scal_invertible_compat :
   {n a} {u : 'K^n},
    invertible a invertible (sum u) invertible (sum (scal a u)).
Proof.
move=>>; rewrite -scal_sum_distr_l; apply mult_invertible_compat; easy.
Qed.

Lemma sum_scal_invertible_reg :
   {n a} {u : 'K^n},
    invertible a invertible (sum (scal a u)) invertible (sum u).
Proof. move=>>; rewrite -scal_sum_distr_l; apply mult_invertible_reg_r. Qed.

Lemma sum_scal_invertible_equiv :
   {n a} {u : 'K^n},
    invertible a invertible (sum (scal a u)) invertible (sum u).
Proof.
move=>> Ha; split; move: Ha.
apply sum_scal_invertible_reg.
apply sum_scal_invertible_compat.
Qed.

End Euclidean_space_Facts.