Library Algebra.ModuleSpace.ModuleSpace_lin_comb
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.
Support for linear combinations on module spaces.
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.
Let K : Ring and E : ModuleSpace K.
Let a : 'K^n and u : 'E^n.
Lemmas about lin_comb have "lc" in their names, usually as prefix "lc_",
sometimes as suffix "_lc".
Let T : Type and f : '(T → K)^n.
Let E1 E2 : ModuleSpace K.
Let f : E1 → E2.
Let u v : 'K^n.
This module may be used through the import of Algebra.ModuleSpace.ModuleSpace,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- f_lc_compat f states that f transports linear combination lin_comb.
Usage
From Requisite Require Import ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group Ring.
From Algebra Require Import ModuleSpace_compl ModuleSpace_FF_FT.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section Lin_comb_Def1.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Definition lin_comb {n} L (B : 'E^n) : E := sum (scalF L B).
Correctness lemmas.
Lemma lc_eq_l :
∀ {n} L M (B : 'E^n), L = M → lin_comb L B = lin_comb M B.
Proof. intros; f_equal; easy. Qed.
Lemma lc_eq_r :
∀ {n} L (B C : 'E^n), B = C → lin_comb L B = lin_comb L C.
Proof. intros; f_equal; easy. Qed.
Lemma lc_eq :
∀ {n} L M (B C : 'E^n), L = M → B = C → lin_comb L B = lin_comb M C.
Proof. intros; f_equal; easy. Qed.
Lemma lc_ext_l :
∀ {n} {L} M {B : 'E^n},
(∀ i, L i = M i) → lin_comb L B = lin_comb M B.
Proof. intros; apply lc_eq_l, extF; easy. Qed.
Lemma lc_ext_r :
∀ {n} {L B} (C : 'E^n),
(∀ i, B i = C i) → lin_comb L B = lin_comb L C.
Proof. intros; apply lc_eq_r, extF; easy. Qed.
Lemma lc_ext :
∀ {n} {L} M {B} (C : 'E^n),
(∀ i, L i = M i) → (∀ i, B i = C i) →
lin_comb L B = lin_comb M C.
Proof. intros; apply lc_eq; apply extF; easy. Qed.
End Lin_comb_Def1.
Section Lin_comb_Def2.
Context {T : Type}.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Definition fct_lc_l {n} (f : '(T → K)^n) (B : 'E^n) : T → E :=
sum (fct_scalF_l f B).
Correctness lemmas.
Lemma fct_lc_l_eq :
∀ {n} (f : '(T → K)^n) (B : 'E^n) t,
fct_lc_l f B t = lin_comb (f^~ t) B.
Proof. intros; apply fct_sum_eq. Qed.
Lemma fct_lc_r_eq :
∀ {n} L (f : '(T → E)^n) t,
lin_comb L f t = lin_comb L (f^~ t).
Proof. intros; apply fct_sum_eq. Qed.
End Lin_comb_Def2.
Section Lin_comb_Facts0.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Lemma lc_scalF_compat :
∀ {n} {L} M {B} (C : 'E^n),
scalF L B = scalF M C → lin_comb L B = lin_comb M C.
Proof. move=>>; apply sum_eq. Qed.
Lemma lc_scalF_zero_compat :
∀ {n} L (B : 'E^n), scalF L B = 0 → lin_comb L B = 0.
Proof. move=>>; apply sum_zero_compat. Qed.
Lemma lc_zero_compat_l :
∀ {n} L (B : 'E^n), L = 0 → lin_comb L B = 0.
Proof. intros; apply lc_scalF_zero_compat, scalF_zero_compat_l; easy. Qed.
Lemma lc_zero_compat_r :
∀ {n} L (B : 'E^n), B = 0 → lin_comb L B = 0.
Proof. intros; apply lc_scalF_zero_compat, scalF_zero_compat_r; easy. Qed.
Lemma lc_nil : ∀ L (B : 'E^0), lin_comb L B = 0.
Proof. intros; apply sum_nil. Qed.
Lemma lc_ind_l :
∀ {n} L (B : 'E^n.+1),
lin_comb L B = scal (L ord0) (B ord0) + lin_comb (liftF_S L) (liftF_S B).
Proof.
intros; unfold lin_comb; rewrite sum_ind_l scalF_correct scalF_liftF_S; easy.
Qed.
Lemma lc_ind_r :
∀ {n} L (B : 'E^n.+1),
lin_comb L B =
lin_comb (widenF_S L) (widenF_S B) + scal (L ord_max) (B ord_max).
Proof.
intros; unfold lin_comb; rewrite sum_ind_r scalF_correct scalF_widenF_S; easy.
Qed.
Lemma lc_plus_l :
∀ {n} L1 L2 (B : 'E^n),
lin_comb (L1 + L2) B = lin_comb L1 B + lin_comb L2 B.
Proof. intros; unfold lin_comb; rewrite scalF_distr_r sum_plus; easy. Qed.
Lemma lc_plus_r :
∀ {n} L (B1 B2 : 'E^n),
lin_comb L (B1 + B2) = lin_comb L B1 + lin_comb L B2.
Proof. intros; unfold lin_comb; rewrite scalF_distr_l sum_plus; easy. Qed.
Lemma lc_castF_compat :
∀ {n1 n2} (H : n1 = n2) {L1} L2 {B1 : 'E^n1} (B2 : 'E^n2),
castF H L1 = L2 → castF H B1 = B2 →
lin_comb L1 B1 = lin_comb L2 B2.
Proof.
intros n1 n2 H; intros; apply (sum_castF_compat H), scalF_castF_compat; easy.
Qed.
Lemma lc_castF :
∀ {n1 n2} (H : n1 = n2) L (B : 'E^n1),
lin_comb (castF H L) (castF H B) = lin_comb L B.
Proof. intros n1 n2 H L B; apply eq_sym, (lc_castF_compat H); easy. Qed.
Lemma lc_castF_l :
∀ {n1 n2} (H : n1 = n2) L1 (B2 : 'E^n2),
lin_comb (castF H L1) B2 = lin_comb L1 (castF (eq_sym H) B2).
Proof.
intros n1 n2 H L1 B2.
apply eq_sym, (lc_castF_compat H); try rewrite castF_can; easy.
Qed.
Lemma lc_castF_r :
∀ {n1 n2} (H : n1 = n2) L2 (B1 : 'E^n1),
lin_comb L2 (castF H B1) = lin_comb (castF (eq_sym H) L2) B1.
Proof.
intros n1 n2 H L2 B1.
apply eq_sym, (lc_castF_compat H); try rewrite castF_can; easy.
Qed.
Lemma lc_zero_l : ∀ {n} (B : 'E^n), lin_comb 0 B = 0.
Proof. intros; unfold lin_comb; rewrite scalF_zero_l sum_zero; easy. Qed.
Lemma lc_zero_r : ∀ {n} L, lin_comb L (0 : 'E^n) = 0.
Proof. intros; unfold lin_comb; rewrite scalF_zero_r sum_zero; easy. Qed.
End Lin_comb_Facts0.
Section Lin_comb_Facts1.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Lemma lc_constF_l :
∀ {n} a (B : 'E^n), lin_comb (constF n a) B = scal a (sum B).
Proof. intros; rewrite scal_sum_distr_l; easy. Qed.
Lemma lc_constF_r :
∀ {n} (L : 'K^n) (u : E), lin_comb L (constF n u) = scal (sum L) u.
Proof. intros; rewrite scal_sum_distr_r; easy. Qed.
Lemma lc_1 :
∀ L (B : 'E^1), lin_comb L B = scal (L ord0) (B ord0).
Proof. intros; apply sum_1. Qed.
Lemma lc_2 :
∀ L (B : 'E^2),
lin_comb L B = scal (L ord0) (B ord0) + scal (L ord_max) (B ord_max).
Proof. intros; apply sum_2. Qed.
Lemma lc_3 :
∀ L (B : 'E^3),
lin_comb L B =
scal (L ord0) (B ord0) +
scal (L ord1) (B ord1) +
scal (L ord_max) (B ord_max).
Proof. intros; apply sum_3. Qed.
Lemma lc_singleF :
∀ L0 (u0 : E), lin_comb (singleF L0) (singleF u0) = scal L0 u0.
Proof. intros; unfold lin_comb; rewrite scalF_singleF; apply sum_singleF. Qed.
Lemma lc_coupleF :
∀ L0 L1 (u0 u1 : E),
lin_comb (coupleF L0 L1) (coupleF u0 u1) = scal L0 u0 + scal L1 u1.
Proof. intros; unfold lin_comb; rewrite scalF_coupleF; apply sum_coupleF. Qed.
Lemma lc_tripleF :
∀ L0 L1 L2 (u0 u1 u2 : E),
lin_comb (tripleF L0 L1 L2) (tripleF u0 u1 u2) =
scal L0 u0 + scal L1 u1 + scal L2 u2.
Proof. intros; unfold lin_comb; rewrite scalF_tripleF; apply sum_tripleF. Qed.
Lemma lc_concatF :
∀ {n1 n2} L1 L2 (B1 : 'E^n1) (B2 : 'E^n2),
lin_comb (concatF L1 L2) (concatF B1 B2) = lin_comb L1 B1 + lin_comb L2 B2.
Proof. intros; unfold lin_comb; rewrite scalF_concatF sum_concatF; easy. Qed.
Lemma lc_concatF_zero_ll :
∀ {n1 n2} L2 (B1 : 'E^n1) (B2 : 'E^n2),
lin_comb (concatF 0 L2) (concatF B1 B2) = lin_comb L2 B2.
Proof.
intros; unfold lin_comb; rewrite scalF_concatF scalF_zero_l;
apply sum_concatF_zero_l.
Qed.
Lemma lc_concatF_zero_lr :
∀ {n1 n2} L1 (B1 : 'E^n1) (B2 : 'E^n2),
lin_comb (concatF L1 0) (concatF B1 B2) = lin_comb L1 B1.
Proof.
intros; unfold lin_comb; rewrite scalF_concatF scalF_zero_l;
apply sum_concatF_zero_r.
Qed.
Lemma lc_concatF_zero_rl :
∀ {n1 n2} (L1 : 'K^n1) L2 (B2 : 'E^n2),
lin_comb (concatF L1 L2) (concatF 0 B2) = lin_comb L2 B2.
Proof.
intros; unfold lin_comb; rewrite scalF_concatF scalF_zero_r;
apply sum_concatF_zero_l.
Qed.
Lemma lc_concatF_zero_rr :
∀ {n1 n2} L1 (L2 : 'K^n2) (B1 : 'E^n1),
lin_comb (concatF L1 L2) (concatF B1 0) = lin_comb L1 B1.
Proof.
intros; unfold lin_comb; rewrite scalF_concatF scalF_zero_r;
apply sum_concatF_zero_r.
Qed.
Lemma lc_splitF :
∀ {n1 n2} L (B : 'E^(n1 + n2)),
lin_comb L B =
lin_comb (firstF L) (firstF B) + lin_comb (lastF L) (lastF B).
Proof.
intros; unfold lin_comb; rewrite sum_splitF scalF_firstF scalF_lastF; easy.
Qed.
Lemma lc_splitF_l :
∀ {n1 n2} L (B1 : 'E^n1) (B2 : 'E^n2),
lin_comb L (concatF B1 B2) = lin_comb (firstF L) B1 + lin_comb (lastF L) B2.
Proof. intros; rewrite lc_splitF firstF_concatF lastF_concatF; easy. Qed.
Lemma lc_splitF_r :
∀ {n1 n2} L1 L2 (B : 'E^(n1 + n2)),
lin_comb (concatF L1 L2) B = lin_comb L1 (firstF B) + lin_comb L2 (lastF B).
Proof. intros; rewrite lc_splitF firstF_concatF lastF_concatF; easy. Qed.
Lemma lc_skipF :
∀ {n} {L} {B : 'E^n.+1} i0,
lin_comb L B = scal (L i0) (B i0) + lin_comb (skipF L i0) (skipF B i0).
Proof. intros n L B i0; unfold lin_comb; rewrite (sum_skipF _ i0); easy. Qed.
Lemma lc_skipF_ex_l :
∀ {n} L0 L1 (B : 'E^n.+1) i0,
∃ L, lin_comb L B = scal L0 (B i0) + lin_comb L1 (skipF B i0) ∧
L i0 = L0 ∧ skipF L i0 = L1.
Proof.
intros n L0 L1 B i0; destruct (skipF_ex L0 L1 i0) as [L [HL0 HL1]].
∃ L; repeat split; try easy; rewrite -HL0 -HL1; apply lc_skipF.
Qed.
Lemma lc_skipF_ex_r :
∀ {n} L u0 (B1 : 'E^n) i0,
∃ B, lin_comb L B = scal (L i0) u0 + lin_comb (skipF L i0) B1 ∧
B i0 = u0 ∧ skipF B i0 = B1.
Proof.
intros n L u0 B1 i0; destruct (skipF_ex u0 B1 i0) as [B [Hu0 HB1]].
∃ B; repeat split; try easy; rewrite -Hu0 -HB1; apply lc_skipF.
Qed.
Lemma lc_one :
∀ {n L} {B : 'E^n.+1} i0,
skipF (scalF L B) i0 = 0 → lin_comb L B = scal (L i0) (B i0).
Proof. move=>>; rewrite -scalF_correct; apply sum_one. Qed.
Lemma lc_one_l :
∀ {n L} {B : 'E^n.+1} i0,
skipF L i0 = 0 → lin_comb L B = scal (L i0) (B i0).
Proof.
intros; apply lc_one; rewrite -scalF_skipF.
apply scalF_zero_compat_l; easy.
Qed.
Lemma lc_one_r :
∀ {n L} {B : 'E^n.+1} i0,
skipF B i0 = 0 → lin_comb L B = scal (L i0) (B i0).
Proof.
intros; apply lc_one; rewrite -scalF_skipF.
apply scalF_zero_compat_r; easy.
Qed.
Lemma lc_skip_zero_l :
∀ {n L} {B : 'E^n.+1} i0,
L i0 = 0 → lin_comb L B = lin_comb (skipF L i0) (skipF B i0).
Proof.
intros n L B i0 HL; unfold lin_comb; rewrite (sum_skip_zero _ i0); try easy.
rewrite scalF_correct HL scal_zero_l; easy.
Qed.
Lemma lc_skip_zero_r :
∀ {n L} {B : 'E^n.+1} i0,
B i0 = 0 → lin_comb L B = lin_comb (skipF L i0) (skipF B i0).
Proof.
intros n L B i0 HB; unfold lin_comb; rewrite (sum_skip_zero _ i0); try easy.
rewrite scalF_correct HB scal_zero_r; easy.
Qed.
Lemma lc_liftF_S_l :
∀ {n} L1 (B : 'E^n),
lin_comb (liftF_S L1) B = lin_comb L1 (castF_1pS (concatF 0 B)).
Proof.
intros n L1 B; pose (B1 := insertF B 0 ord0).
assert (HB1a : B1 ord0 = 0) by now unfold B1; rewrite insertF_correct_l.
assert (HB1b : skipF B1 ord0 = B) by apply skipF_insertF.
rewrite -skipF_first -{1}HB1b -lc_skip_zero_r// -insertF_concatF_0; easy.
Qed.
Lemma lc_liftF_S_r :
∀ {n} L (B1 : 'E^n.+1),
lin_comb L (liftF_S B1) = lin_comb (castF_1pS (concatF 0 L)) B1.
Proof.
intros n L B1; pose (L1 := insertF L 0 ord0).
assert (HL1a : L1 ord0 = 0) by now unfold L1; rewrite insertF_correct_l.
assert (HL1b : skipF L1 ord0 = L) by apply skipF_insertF.
rewrite -skipF_first -{1}HL1b -lc_skip_zero_l// -insertF_concatF_0; easy.
Qed.
Lemma lc_widenF_S_l :
∀ {n} L1 (B : 'E^n),
lin_comb (widenF_S L1) B = lin_comb L1 (castF_p1S (concatF B 0)).
Proof.
intros n L1 B; pose (B1 := insertF B 0 ord_max).
assert (HB1a : B1 ord_max = 0) by now unfold B1; rewrite insertF_correct_l.
assert (HB1b : skipF B1 ord_max = B) by apply skipF_insertF.
rewrite -skipF_last -{1}HB1b -lc_skip_zero_r// -insertF_concatF_max; easy.
Qed.
Lemma lc_widenF_S_r :
∀ {n} L (B1 : 'E^n.+1),
lin_comb L (widenF_S B1) = lin_comb (castF_p1S (concatF L 0)) B1.
Proof.
intros n L B1; pose (L1 := insertF L 0 ord_max).
assert (HL1a : L1 ord_max = 0) by now unfold L1; rewrite insertF_correct_l.
assert (HL1b : skipF L1 ord_max = L) by apply skipF_insertF.
rewrite -skipF_last -{1}HL1b -lc_skip_zero_l// -insertF_concatF_max; easy.
Qed.
Lemma lc_skip2F :
∀ {n} L (B : 'E^n.+2) {i0 i1} (H : i1 ≠ i0),
lin_comb L B =
scal (L i0) (B i0) + scal (L i1) (B i1) +
lin_comb (skip2F L H) (skip2F B H).
Proof.
intros n L B i0 i1 H; unfold lin_comb; rewrite (sum_skip2F _ H); easy.
Qed.
Lemma lc_two :
∀ {n L} {B : 'E^n.+2} {i0 i1 : 'I_n.+2} (H : (i1 ≠ i0)%nat),
skip2F (scalF L B) H = 0 →
lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
Proof. move=>>; rewrite -!scalF_correct; apply sum_two. Qed.
Lemma lc_two_l :
∀ {n L} {B : 'E^n.+2} {i0 i1} (H : i1 ≠ i0),
skip2F L H = 0 →
lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
Proof.
intros n L B i0 i1 Hi H; apply lc_two with Hi; rewrite -scalF_skip2F.
apply scalF_zero_compat_l; easy.
Qed.
Lemma lc_two_r :
∀ {n L} {B : 'E^n.+2} {i0 i1} (H : i1 ≠ i0),
skip2F B H = 0 →
lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
Proof.
intros n L B i0 i1 Hi H; apply lc_two with Hi; rewrite -scalF_skip2F.
apply scalF_zero_compat_r; easy.
Qed.
Lemma lc_insertF :
∀ {n} L (B : 'E^n) a0 x0 i0,
lin_comb (insertF L a0 i0) (insertF B x0 i0) = scal a0 x0 + lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_insertF; apply sum_insertF. Qed.
Lemma lc_insertF_l :
∀ {n} L (B : 'E^n.+1) a0 i0,
lin_comb (insertF L a0 i0) B = scal a0 (B i0) + lin_comb L (skipF B i0).
Proof.
intros n L B a0 i0; rewrite -{1}(insertF_skipF B i0) lc_insertF; easy.
Qed.
Lemma lc_insertF_r :
∀ {n} L (B : 'E^n) x0 i0,
lin_comb L (insertF B x0 i0) = scal (L i0) x0 + lin_comb (skipF L i0) B.
Proof.
intros n L B x0 i0; rewrite -{1}(insertF_skipF L i0) lc_insertF; easy.
Qed.
Lemma lc_insert2F :
∀ {n} L (B : 'E^n) a0 a1 x0 x1 {i0 i1} (H : i1 ≠ i0),
lin_comb (insert2F L a0 a1 H) (insert2F B x0 x1 H) =
scal a0 x0 + scal a1 x1 + lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_insert2F; apply sum_insert2F. Qed.
Lemma lc_replaceF :
∀ {n} L (B : 'E^n) a0 x0 i0,
scal (L i0) (B i0) + lin_comb (replaceF L a0 i0) (replaceF B x0 i0) =
scal a0 x0 + lin_comb L B.
Proof.
intros [| n] L B a0 x0 i0; [destruct i0; easy |].
unfold lin_comb; rewrite scalF_replaceF -scalF_correct; apply sum_replaceF.
Qed.
Lemma lc_replace2F :
∀ {n} L (B : 'E^n.+2) a0 a1 x0 x1 {i0 i1},
i1 ≠ i0 →
scal (L i0) (B i0) + scal (L i1) (B i1) +
lin_comb (replace2F L a0 a1 i0 i1) (replace2F B x0 x1 i0 i1) =
scal a0 x0 + scal a1 x1 + lin_comb L B.
Proof.
intros; unfold lin_comb; rewrite scalF_replace2F -!scalF_correct;
apply sum_replace2F; easy.
Qed.
Lemma lc_replace2F_eq :
∀ {n} L (B : 'E^n.+2) a0 a1 x0 x1 {i0 i1},
i1 = i0 →
scal (L i1) (B i1) +
lin_comb (replace2F L a0 a1 i0 i1) (replace2F B x0 x1 i0 i1) =
scal a1 x1 + lin_comb L B.
Proof.
intros; unfold lin_comb; rewrite scalF_replace2F -scalF_correct;
apply sum_replace2F_eq; easy.
Qed.
Lemma lc_permutF :
∀ {n p L} {B : 'E^n}, injective p →
lin_comb (permutF p L) (permutF p B) = lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_permutF sum_permutF; easy. Qed.
Lemma lc_permutF_l :
∀ {n p q L} {B : 'E^n}, cancel q p →
lin_comb (permutF p L) B = lin_comb L (permutF q B).
Proof.
intros n p q L B H.
rewrite -{2}(permutF_can p q L)// (lc_permutF (can_inj H)); easy.
Qed.
Lemma lc_permutF_r :
∀ {n p q L} {B : 'E^n}, cancel p q →
lin_comb L (permutF p B) = lin_comb (permutF q L) B.
Proof. intros; apply eq_sym, lc_permutF_l; easy. Qed.
Lemma lc_revF :
∀ {n} L (B : 'E^n), lin_comb (revF L) (revF B) = lin_comb L B.
Proof. intros; apply lc_permutF, rev_ord_inj. Qed.
Lemma lc_revF_l :
∀ {n} L (B : 'E^n), lin_comb (revF L) B = lin_comb L (revF B).
Proof. intros; apply lc_permutF_l, rev_ordK. Qed.
Lemma lc_revF_r :
∀ {n} L (B : 'E^n), lin_comb L (revF B) = lin_comb (revF L) B.
Proof. intros; apply eq_sym, lc_revF_l. Qed.
Lemma lc_moveF :
∀ {n} L (B : 'E^n.+1) i0 i1,
lin_comb (moveF L i0 i1) (moveF B i0 i1) = lin_comb L B.
Proof. intros; apply lc_permutF, move_ord_inj. Qed.
Lemma lc_moveF_l :
∀ {n} L (B : 'E^n.+1) i0 i1,
lin_comb (moveF L i0 i1) B = lin_comb L (moveF B i1 i0).
Proof. intros; apply lc_permutF_l, move_ord_orth. Qed.
Lemma lc_moveF_r :
∀ {n} L (B : 'E^n.+1) i0 i1,
lin_comb L (moveF B i0 i1) = lin_comb (moveF L i1 i0) B.
Proof. intros; apply eq_sym, lc_moveF_l. Qed.
Lemma lc_transpF :
∀ {n} L (B : 'E^n) i0 i1,
lin_comb (transpF L i0 i1) (transpF B i0 i1) = lin_comb L B.
Proof. intros; apply lc_permutF, transp_ord_inj. Qed.
Lemma lc_transpF_l :
∀ {n} L (B : 'E^n) i0 i1,
lin_comb (transpF L i0 i1) B = lin_comb L (transpF B i0 i1).
Proof. intros; apply lc_permutF_l, transp_ord_invol. Qed.
Lemma lc_transpF_r :
∀ {n} L (B : 'E^n) i0 i1,
lin_comb L (transpF B i0 i1) = lin_comb (transpF L i0 i1) B.
Proof. intros; apply eq_sym, lc_transpF_l. Qed.
Lemma lc_splitPF :
∀ {n} P L (B : 'E^n),
lin_comb (splitPF P L) (splitPF P B) = lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_splitPF sum_splitPF; easy. Qed.
Lemma lc_itemF_l :
∀ {n} a (B : 'E^n) i0, lin_comb (itemF n a i0) B = scal a (B i0).
Proof.
intros [| n] a B i0; [now destruct i0 |].
erewrite → lc_one, itemF_diag; try easy.
rewrite scalF_itemF_l skipF_itemF_diag; easy.
Qed.
Lemma lc_itemF_r :
∀ {n} L (u : E) i0, lin_comb L (itemF n u i0) = scal (L i0) u.
Proof.
intros [| n] L u i0; [now destruct i0 |].
erewrite → lc_one, itemF_diag; try easy.
rewrite scalF_itemF_r skipF_itemF_diag; easy.
Qed.
Lemma lc_split0F_l :
∀ {n} L (B : 'E^n),
lin_comb (split0F L) (split0F_gen L B) = lin_comb L B.
Proof. intros; apply lc_splitPF. Qed.
Lemma lc_split0F_r :
∀ {n} L (B : 'E^n),
lin_comb (split0F_gen B L) (split0F B) = lin_comb L B.
Proof. intros; apply lc_splitPF. Qed.
Lemma lc_filter_n0F_l :
∀ {n} L (B : 'E^n),
lin_comb (filter_n0F L) (filter_n0F_gen L B) = lin_comb L B.
Proof.
intros n L B; rewrite -(lc_split0F_l L) -(plus_zero_l (lin_comb _ _)).
rewrite split0F_correct split0F_gen_correct lc_concatF; f_equal.
rewrite lc_zero_compat_l// filter0F_correct//.
Qed.
Lemma lc_filter_n0F_l_ex :
∀ {n} L B', ∃ (B : 'E^n),
lin_comb (filter_n0F L) B' = lin_comb L B.
Proof.
intros n L B'; ∃ (unfun0F filterP_ord B').
rewrite -(lc_filter_n0F_l L); f_equal.
rewrite filter_n0F_gen_eq_funF funF_unfun0F; [easy | apply filterP_ord_inj].
Qed.
Lemma lc_filter_n0F_r :
∀ {n} L (B : 'E^n),
lin_comb (filter_n0F_gen B L) (filter_n0F B) = lin_comb L B.
Proof.
intros n L B; rewrite -(lc_split0F_r L) -(plus_zero_l (lin_comb _ _)).
rewrite split0F_correct split0F_gen_correct lc_concatF; f_equal.
rewrite lc_zero_compat_r// filter0F_correct//.
Qed.
Lemma lc_filter_n0F_r_ex :
∀ {n} (B : 'E^n) L', ∃ L,
lin_comb L' (filter_n0F B) = lin_comb L B.
Proof.
intros n B L'; ∃ (unfun0F filterP_ord L').
rewrite -(lc_filter_n0F_r _ B); f_equal.
rewrite filter_n0F_gen_eq_funF funF_unfun0F; [easy | apply filterP_ord_inj].
Qed.
Lemma lc_unfun0F :
∀ {n1 n2} {f : '('I_n2)^n1} L1 (B1 : 'E^n1),
injective f → lin_comb (unfun0F f L1) (unfun0F f B1) = lin_comb L1 B1.
Proof. intros; unfold lin_comb; rewrite scalF_unfun0F sum_unfun0F; easy. Qed.
Lemma lc_squeezeF :
∀ {n} L (B : 'E^n.+1) {i0 i1},
i1 ≠ i0 → B i1 = B i0 →
lin_comb (squeezeF L i0 i1) (skipF B i1) = lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_squeezeF// sum_squeezeF//. Qed.
Lemma lc_concatnF :
∀ {n} {b : 'nat^n} L (B : ∀ i, 'E^(b i)),
lin_comb (concatnF L) (concatnF B) = sum (fun i ⇒ lin_comb (L i) (B i)).
Proof. intros; unfold lin_comb; rewrite scalF_concatnF; apply sum_assoc. Qed.
Lemma lcT_r :
∀ {n1 n2} L1 (B12 : 'E^{n1,n2}),
lin_comb L1 B12 = mapF (lin_comb L1) (flipT B12).
Proof. intros; apply extF; intro; rewrite fct_lc_r_eq; easy. Qed.
Lemma lc_flipT_r :
∀ {n1 n2} L2 (B12 : 'E^{n1,n2}),
lin_comb L2 (flipT B12) = mapF (lin_comb L2) B12.
Proof. intros; rewrite -lcT_r; easy. Qed.
Lemma lc_skipTc_r :
∀ {n1 n2} L1 (B12 : 'E^{n1,n2.+1}) i20,
lin_comb L1 (skipTc B12 i20) = skipF (lin_comb L1 B12) i20.
Proof. intros; rewrite -sum_skipTc -scalF_skipTc_r; easy. Qed.
Lemma lc_row_r :
∀ {n1 n2} L1 (B12 : 'E^{n1,n2}) i1,
lin_comb L1 (row B12 i1) = lin_comb L1 (col B12) i1.
Proof.
intros n1 n2 L1 B12 i1; induction n2; try now rewrite !lc_nil.
rewrite !lc_ind_l fct_plus_eq fct_lc_r_eq; f_equal.
Qed.
Lemma lc_col_r :
∀ {n1 n2} L1 (B12 : 'E^{n1,n2}) i1,
lin_comb L1 (col B12 i1) = lin_comb L1 (row B12) i1.
Proof.
intros n1 n2 L1 B12 i1; induction n1; try now rewrite !lc_nil.
rewrite !lc_ind_l fct_plus_eq fct_lc_r_eq; f_equal.
Qed.
End Lin_comb_Facts1.
Section Lin_comb_Facts2.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Lemma lc_opp_l :
∀ {n} L (B : 'E^n), lin_comb (- L) B = - lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_opp_l sum_opp; easy. Qed.
Lemma lc_opp_r :
∀ {n} L (B : 'E^n), lin_comb L (- B) = - lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_opp_r sum_opp; easy. Qed.
Lemma lc_minus_l :
∀ {n} L1 L2 (B : 'E^n),
lin_comb (L1 - L2) B = lin_comb L1 B - lin_comb L2 B.
Proof. intros; unfold lin_comb; rewrite scalF_minus_l sum_minus; easy. Qed.
Lemma lc_minus_r :
∀ {n} L (B1 B2 : 'E^n),
lin_comb L (B1 - B2) = lin_comb L B1 - lin_comb L B2.
Proof. intros; unfold lin_comb; rewrite scalF_minus_r sum_minus; easy. Qed.
Lemma lc_minus_zero_l_equiv :
∀ {n} L1 L2 (B : 'E^n),
lin_comb (L1 - L2) B = 0 ↔ lin_comb L1 B = lin_comb L2 B.
Proof.
intros; unfold lin_comb; rewrite scalF_minus_l sum_minus_zero_equiv; easy.
Qed.
Lemma lc_minus_zero_r_equiv :
∀ {n} L (B1 B2 : 'E^n),
lin_comb L (B1 - B2) = 0 ↔ lin_comb L B1 = lin_comb L B2.
Proof.
intros; unfold lin_comb; rewrite scalF_minus_r sum_minus_zero_equiv; easy.
Qed.
Lemma lc_scal_l :
∀ {n} x L (B : 'E^n), lin_comb (scal x L) B = scal x (lin_comb L B).
Proof.
intros; unfold lin_comb; rewrite scalF_scal_l scal_sum_distr_l; easy.
Qed.
Lemma scal_lc_l :
∀ {n} (L L' : 'K^n) (u : E),
scal (lin_comb L L') u = lin_comb L (scalF L' (constF n u)).
Proof.
intros n L L' u; induction n.
rewrite lc_nil scal_zero_l; apply eq_sym, lc_nil.
rewrite !lc_ind_l scal_distr_r IHn; f_equal.
rewrite scal_assoc; easy.
Qed.
Lemma scal_lc_r :
∀ {n} a L (B : 'E^n), scal a (lin_comb L B) = lin_comb (scal a L) B.
Proof. intros; apply eq_sym, lc_scal_l. Qed.
Lemma lc_sum_l :
∀ {n1 n2} (L12 : 'K^{n1,n2}) (B1 : 'E^n1),
lin_comb (fun i1 ⇒ sum (L12 i1)) B1 =
sum (fun i2 ⇒ lin_comb (L12^~ i2) B1).
Proof.
intros; unfold lin_comb; rewrite scalF_sum_rr sumT_sym; f_equal.
apply extF; intro; rewrite fct_sum_eq; easy.
Qed.
Lemma lc_sum_r :
∀ {n1 n2} L1 (B12 : 'E^{n1,n2}),
lin_comb L1 (fun i1 ⇒ sum (B12 i1)) =
sum (fun i2 ⇒ lin_comb L1 (B12^~ i2)).
Proof.
intros; unfold lin_comb; rewrite scalF_sum_lr sumT_sym; f_equal.
apply extF; intro; rewrite fct_sum_eq; easy.
Qed.
Lemma lc_scal_sum_r :
∀ {n1 n2} (L1 : 'K^n1) (L12 : 'K^{n1,n2}) (B2 : 'E^n2),
lin_comb L1 (fun i1 ⇒ scal (sum (L12 i1)) B2) =
scal (sum (lin_comb L1 L12)) B2.
Proof.
intros n1; induction n1 as [| n1 Hn1].
intros; rewrite !lc_nil sum_zero scal_zero_l; easy.
intros; rewrite 2!lc_ind_l Hn1 scal_assoc sum_plus
scal_distr_r -scal_sum_distr_l; easy.
Qed.
Lemma lc2_l :
∀ {n1 n2} (L1 : 'K^n1) L12 (B2 : 'E^n2),
lin_comb (lin_comb L1 L12) B2 = lin_comb L1 (mapF (lin_comb^~ B2) L12).
Proof.
intros n1; induction n1 as [| n1 Hn1].
intros; rewrite !lc_nil lc_zero_l; easy.
intros; rewrite !lc_ind_l lc_plus_l Hn1 lc_scal_l; easy.
Qed.
Lemma lc2_l_alt :
∀ {n1 n2} {L1} {B1: 'E^n1} {L12} {B2 : 'E^n2},
(∀ i1, B1 i1 = lin_comb (L12 i1) B2) →
lin_comb L1 B1 = lin_comb (mapF (lin_comb L1) (flipT L12)) B2.
Proof.
move=>> HB; rewrite -lcT_r lc2_l; f_equal; apply extF; intro; rewrite HB; easy.
Qed.
Lemma lc_ones_l : ∀ {n} (B : 'E^n), lin_comb ones B = sum B.
Proof. intros; unfold lin_comb; rewrite scalF_ones_l; easy. Qed.
Lemma lc_ones_r : ∀ {n} (L : 'K^n), lin_comb L ones = sum L.
Proof. intros; unfold lin_comb; rewrite scalF_ones_r; easy. Qed.
End Lin_comb_Facts2.
Section Lin_comb_Facts3.
Context {K : Ring}.
Context {E F : ModuleSpace K}.
Context {T : Type}.
Lemma lc_compF_rl :
∀ {n} (L : 'K^n) (B : '(E → F)^n) (f : T → E),
lin_comb L (compF_l B f) = lin_comb L B \o f.
Proof. intros; unfold lin_comb; rewrite scalF_compF_rl -sum_compF_l; easy. Qed.
End Lin_comb_Facts3.
Section Lin_comb_Kron_Facts1.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Note that second "_l" suffix is relative to kron.
Lemma lc_kron_l_in_l :
∀ {n} (j : 'I_n) (B : 'E^n), lin_comb (kron K ^~ j) B = B j.
Proof.
intros [| n] j B; [now destruct j | rewrite (lc_one_l j)].
rewrite kron_is_1// scal_one_l; easy.
apply kron_skipF_diag_r.
Qed.
∀ {n} (j : 'I_n) (B : 'E^n), lin_comb (kron K ^~ j) B = B j.
Proof.
intros [| n] j B; [now destruct j | rewrite (lc_one_l j)].
rewrite kron_is_1// scal_one_l; easy.
apply kron_skipF_diag_r.
Qed.
Note that second "_l" suffix is relative to kron.
Lemma lc_kron_l_out_l :
∀ {n} j (B : 'E^n), ¬(j < n)%nat → lin_comb (kron K ^~ j) B = 0.
Proof.
intros n j B Hj; apply lc_zero_compat_l, extF; intro.
rewrite kron_is_0; [| contradict Hj; rewrite -Hj]; easy.
Qed.
∀ {n} j (B : 'E^n), ¬(j < n)%nat → lin_comb (kron K ^~ j) B = 0.
Proof.
intros n j B Hj; apply lc_zero_compat_l, extF; intro.
rewrite kron_is_0; [| contradict Hj; rewrite -Hj]; easy.
Qed.
Note that "_r" suffix is relative to kron.
Lemma lc_kron_l_in_r :
∀ {n} (i : 'I_n) (B : 'E^n), lin_comb (kron K i) B = B i.
Proof.
intros [| n] i B; [now destruct i | rewrite (lc_one_l i)].
rewrite kron_is_1// scal_one_l; easy.
apply kron_skipF_diag_l.
Qed.
∀ {n} (i : 'I_n) (B : 'E^n), lin_comb (kron K i) B = B i.
Proof.
intros [| n] i B; [now destruct i | rewrite (lc_one_l i)].
rewrite kron_is_1// scal_one_l; easy.
apply kron_skipF_diag_l.
Qed.
Note that "_r" suffix is relative to kron.
Lemma lc_kron_l_out_r :
∀ {n} i (B : 'E^n), ¬(i < n)%nat → lin_comb (kron K i) B = 0.
Proof.
intros n i B Hi; apply lc_zero_compat_l, extF; intro.
rewrite kron_is_0; [| contradict Hi; rewrite Hi]; easy.
Qed.
Lemma lc_plus_kron_l :
∀ {n} L (B : 'E^n) a (i : 'I_n),
lin_comb (scal a (kron K i : 'K^n) + L) B = scal a (B i) + lin_comb L B.
Proof.
intros n L B a i; rewrite lc_plus_l; f_equal.
rewrite lc_scal_l lc_kron_l_in_r; easy.
Qed.
End Lin_comb_Kron_Facts1.
Section Lin_comb_Kron_Facts2.
Context {K : Ring}.
Lemma lc_kron2 :
∀ {n} (i : 'I_n) j,
lin_comb (fun k : 'I_n ⇒ kron K i k) (kron K ^~ j) = kron K i j.
Proof. intros; apply: lc_kron_l_in_r. Qed.
∀ {n} i (B : 'E^n), ¬(i < n)%nat → lin_comb (kron K i) B = 0.
Proof.
intros n i B Hi; apply lc_zero_compat_l, extF; intro.
rewrite kron_is_0; [| contradict Hi; rewrite Hi]; easy.
Qed.
Lemma lc_plus_kron_l :
∀ {n} L (B : 'E^n) a (i : 'I_n),
lin_comb (scal a (kron K i : 'K^n) + L) B = scal a (B i) + lin_comb L B.
Proof.
intros n L B a i; rewrite lc_plus_l; f_equal.
rewrite lc_scal_l lc_kron_l_in_r; easy.
Qed.
End Lin_comb_Kron_Facts1.
Section Lin_comb_Kron_Facts2.
Context {K : Ring}.
Lemma lc_kron2 :
∀ {n} (i : 'I_n) j,
lin_comb (fun k : 'I_n ⇒ kron K i k) (kron K ^~ j) = kron K i j.
Proof. intros; apply: lc_kron_l_in_r. Qed.
Note that "_l" suffix is relative to kron.
Lemma lc_kron_r_in_l :
∀ {n} (L : 'K^n) (j : 'I_n), lin_comb L (kron K ^~ j) = L j.
Proof.
intros [| n] L j; [now destruct j | rewrite (lc_one_r j)].
rewrite kron_is_1// scal_one_r; easy.
apply kron_skipF_diag_r.
Qed.
∀ {n} (L : 'K^n) (j : 'I_n), lin_comb L (kron K ^~ j) = L j.
Proof.
intros [| n] L j; [now destruct j | rewrite (lc_one_r j)].
rewrite kron_is_1// scal_one_r; easy.
apply kron_skipF_diag_r.
Qed.
Note that "_l" suffix is relative to kron.
Lemma lc_kron_r_out_l :
∀ {n} (L : 'K^n) j, ¬(j < n)%nat → lin_comb L (kron K ^~ j) = 0.
Proof.
intros n L j Hj; apply lc_zero_compat_r, extF; intro.
rewrite kron_is_0; [| contradict Hj; rewrite -Hj]; easy.
Qed.
∀ {n} (L : 'K^n) j, ¬(j < n)%nat → lin_comb L (kron K ^~ j) = 0.
Proof.
intros n L j Hj; apply lc_zero_compat_r, extF; intro.
rewrite kron_is_0; [| contradict Hj; rewrite -Hj]; easy.
Qed.
Note that second "_r" suffix is relative to kron.
Lemma lc_kron_r_in_r :
∀ {n} (L : 'K^n) (i : 'I_n), lin_comb L (kron K i) = L i.
Proof.
intros [| n] L i; [now destruct i | rewrite (lc_one_r i)].
rewrite kron_is_1// scal_one_r; easy.
apply kron_skipF_diag_l.
Qed.
∀ {n} (L : 'K^n) (i : 'I_n), lin_comb L (kron K i) = L i.
Proof.
intros [| n] L i; [now destruct i | rewrite (lc_one_r i)].
rewrite kron_is_1// scal_one_r; easy.
apply kron_skipF_diag_l.
Qed.
Note that second "_r" suffix is relative to kron.
Lemma lc_kron_r_out_r :
∀ {n} (L : 'K^n) i, ¬(i < n)%nat → lin_comb L (kron K i) = 0.
Proof.
intros n L i Hi; apply lc_zero_compat_r, extF; intro.
rewrite kron_is_0; [| contradict Hi; rewrite Hi]; easy.
Qed.
Lemma lc_kron_r :
∀ {n} (L : 'K^n), lin_comb L (fun i j : 'I_n ⇒ kron K i j) = L.
Proof.
intros; apply extF; intro; rewrite fct_lc_r_eq; apply lc_kron_r_in_l.
Qed.
End Lin_comb_Kron_Facts2.
Section Dot_product_Def.
Context {K : Ring}.
Definition dot_product {n} (u v : 'K^n) : K := lin_comb u v.
End Dot_product_Def.
Declare Scope ModuleSpace_scope.
Delimit Scope ModuleSpace_scope with MS.
Notation "u ⋅ v" := (dot_product u v) (at level 40) : ModuleSpace_scope.
Local Open Scope ModuleSpace_scope.
Section Dot_product_Facts.
Context {K : Ring}.
Lemma dot_product_nil : ∀ (u v : 'K^0), u ⋅ v = 0.
Proof. apply: lc_nil. Qed.
Lemma dot_product_1 : ∀ (u v : 'K^1), u ⋅ v = u ord0 × v ord0.
Proof. apply: lc_1. Qed.
Lemma dot_product_2 :
∀ (u v : 'K^2), u ⋅ v = u ord0 × v ord0 + u ord_max × v ord_max.
Proof. apply: lc_2. Qed.
Lemma dot_product_3 :
∀ (u v : 'K^3),
u ⋅ v = u ord0 × v ord0 + u ord1 × v ord1 + u ord_max × v ord_max.
Proof. apply: lc_3. Qed.
Lemma dot_product_singleF :
∀ (u0 v0 : K), singleF u0 ⋅ singleF v0 = u0 × v0.
Proof. apply: lc_singleF. Qed.
Lemma dot_product_coupleF :
∀ (u0 u1 v0 v1 : K),
coupleF u0 u1 ⋅ coupleF v0 v1 = u0 × v0 + u1 × v1.
Proof. apply: lc_coupleF. Qed.
Lemma dot_product_tripleF :
∀ (u0 u1 u2 v0 v1 v2 : K),
tripleF u0 u1 u2 ⋅ tripleF v0 v1 v2 = u0 × v0 + u1 × v1 + u2 × v2.
Proof. apply: lc_tripleF. Qed.
Lemma dot_product_castF :
∀ {n1 n2} (H : n1 = n2) (u1 v1 : 'K^n1),
castF H u1 ⋅ castF H v1 = u1 ⋅ v1.
Proof. intros; apply lc_castF. Qed.
Lemma dot_product_concatF_l :
∀ {n1 n2} (u1 : 'K^n1) (u2 : 'K^n2) (v : 'K^(n1 + n2)),
concatF u1 u2 ⋅ v = u1 ⋅ firstF v + u2 ⋅ lastF v.
Proof. intros; apply: lc_splitF_r. Qed.
Lemma dot_product_concatF_r :
∀ {n1 n2} (u : 'K^(n1 + n2)) (v1 : 'K^n1) (v2 : 'K^n2),
u ⋅ concatF v1 v2 = firstF u ⋅ v1 + lastF u ⋅ v2.
Proof. intros; apply: lc_splitF_l. Qed.
Lemma dot_product_scal_l :
∀ {n} (u v : 'K^n) a, scal a u ⋅ v = a × (u ⋅ v).
Proof. intros; unfold dot_product; rewrite lc_scal_l; easy. Qed.
Lemma dot_product_plus_l :
∀ {n} (u v w : 'K^n), (u + v) ⋅ w = u ⋅ w + v ⋅ w.
Proof. intros; unfold dot_product; rewrite lc_plus_l; easy. Qed.
Lemma dot_product_ind_l :
∀ {n} (u v : 'K^n.+1),
u ⋅ v = scal (u ord0) (v ord0) + liftF_S u ⋅ liftF_S v.
Proof. intros; unfold dot_product; rewrite lc_ind_l; easy. Qed.
Lemma dot_product_insertF :
∀ {n} (u v : 'K^n) a b i0,
insertF u a i0 ⋅ insertF v b i0 = a × b + u ⋅ v.
Proof. intros; unfold dot_product; rewrite lc_insertF; easy. Qed.
Lemma dot_product_skipF :
∀ {n} (u v : 'K^n.+1) i0,
u ⋅ v = scal (u i0) (v i0) + skipF u i0 ⋅ skipF v i0.
Proof. intros; unfold dot_product; apply lc_skipF. Qed.
Lemma dot_product_zero_l : ∀ {n} (v : 'K^n), 0 ⋅ v = 0.
Proof. intros; apply: lc_zero_l. Qed.
Lemma dot_product_zero_r : ∀ {n} (u : 'K^n), u ⋅ 0 = 0.
Proof. intros; apply: lc_zero_r. Qed.
End Dot_product_Facts.
∀ {n} (L : 'K^n) i, ¬(i < n)%nat → lin_comb L (kron K i) = 0.
Proof.
intros n L i Hi; apply lc_zero_compat_r, extF; intro.
rewrite kron_is_0; [| contradict Hi; rewrite Hi]; easy.
Qed.
Lemma lc_kron_r :
∀ {n} (L : 'K^n), lin_comb L (fun i j : 'I_n ⇒ kron K i j) = L.
Proof.
intros; apply extF; intro; rewrite fct_lc_r_eq; apply lc_kron_r_in_l.
Qed.
End Lin_comb_Kron_Facts2.
Section Dot_product_Def.
Context {K : Ring}.
Definition dot_product {n} (u v : 'K^n) : K := lin_comb u v.
End Dot_product_Def.
Declare Scope ModuleSpace_scope.
Delimit Scope ModuleSpace_scope with MS.
Notation "u ⋅ v" := (dot_product u v) (at level 40) : ModuleSpace_scope.
Local Open Scope ModuleSpace_scope.
Section Dot_product_Facts.
Context {K : Ring}.
Lemma dot_product_nil : ∀ (u v : 'K^0), u ⋅ v = 0.
Proof. apply: lc_nil. Qed.
Lemma dot_product_1 : ∀ (u v : 'K^1), u ⋅ v = u ord0 × v ord0.
Proof. apply: lc_1. Qed.
Lemma dot_product_2 :
∀ (u v : 'K^2), u ⋅ v = u ord0 × v ord0 + u ord_max × v ord_max.
Proof. apply: lc_2. Qed.
Lemma dot_product_3 :
∀ (u v : 'K^3),
u ⋅ v = u ord0 × v ord0 + u ord1 × v ord1 + u ord_max × v ord_max.
Proof. apply: lc_3. Qed.
Lemma dot_product_singleF :
∀ (u0 v0 : K), singleF u0 ⋅ singleF v0 = u0 × v0.
Proof. apply: lc_singleF. Qed.
Lemma dot_product_coupleF :
∀ (u0 u1 v0 v1 : K),
coupleF u0 u1 ⋅ coupleF v0 v1 = u0 × v0 + u1 × v1.
Proof. apply: lc_coupleF. Qed.
Lemma dot_product_tripleF :
∀ (u0 u1 u2 v0 v1 v2 : K),
tripleF u0 u1 u2 ⋅ tripleF v0 v1 v2 = u0 × v0 + u1 × v1 + u2 × v2.
Proof. apply: lc_tripleF. Qed.
Lemma dot_product_castF :
∀ {n1 n2} (H : n1 = n2) (u1 v1 : 'K^n1),
castF H u1 ⋅ castF H v1 = u1 ⋅ v1.
Proof. intros; apply lc_castF. Qed.
Lemma dot_product_concatF_l :
∀ {n1 n2} (u1 : 'K^n1) (u2 : 'K^n2) (v : 'K^(n1 + n2)),
concatF u1 u2 ⋅ v = u1 ⋅ firstF v + u2 ⋅ lastF v.
Proof. intros; apply: lc_splitF_r. Qed.
Lemma dot_product_concatF_r :
∀ {n1 n2} (u : 'K^(n1 + n2)) (v1 : 'K^n1) (v2 : 'K^n2),
u ⋅ concatF v1 v2 = firstF u ⋅ v1 + lastF u ⋅ v2.
Proof. intros; apply: lc_splitF_l. Qed.
Lemma dot_product_scal_l :
∀ {n} (u v : 'K^n) a, scal a u ⋅ v = a × (u ⋅ v).
Proof. intros; unfold dot_product; rewrite lc_scal_l; easy. Qed.
Lemma dot_product_plus_l :
∀ {n} (u v w : 'K^n), (u + v) ⋅ w = u ⋅ w + v ⋅ w.
Proof. intros; unfold dot_product; rewrite lc_plus_l; easy. Qed.
Lemma dot_product_ind_l :
∀ {n} (u v : 'K^n.+1),
u ⋅ v = scal (u ord0) (v ord0) + liftF_S u ⋅ liftF_S v.
Proof. intros; unfold dot_product; rewrite lc_ind_l; easy. Qed.
Lemma dot_product_insertF :
∀ {n} (u v : 'K^n) a b i0,
insertF u a i0 ⋅ insertF v b i0 = a × b + u ⋅ v.
Proof. intros; unfold dot_product; rewrite lc_insertF; easy. Qed.
Lemma dot_product_skipF :
∀ {n} (u v : 'K^n.+1) i0,
u ⋅ v = scal (u i0) (v i0) + skipF u i0 ⋅ skipF v i0.
Proof. intros; unfold dot_product; apply lc_skipF. Qed.
Lemma dot_product_zero_l : ∀ {n} (v : 'K^n), 0 ⋅ v = 0.
Proof. intros; apply: lc_zero_l. Qed.
Lemma dot_product_zero_r : ∀ {n} (u : 'K^n), u ⋅ 0 = 0.
Proof. intros; apply: lc_zero_r. Qed.
End Dot_product_Facts.