Library Algebra.AffineSpace.AffineSpace_baryc

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

Support barycenters in affine spaces.

Description

Let K : Ring, V : ModuleSpace K and E : AffineSpace V. Let L : 'K^n, A : 'E^n and G : E.
Lemmas about aff_comb have "ac" in their names, mostly as prefix "ac_". Lemmas about barycenter have "baryc" in their names, usually as prefix "baryc_", sometimes as suffix "_baryc".
Let A B C D : E.

Bibliography

[GostiauxT4] Bernard Gostiaux, Cours de mathématiques spéciales - 4. Géométrie affine et métrique Mathématiques, Presses Universitaires de France, Paris, 1995, https://www.puf.com/cours-de-mathematiques-speciales-tome-4-geometrie-affine-et-metrique.

Used logic axioms

Usage

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

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 ModuleSpace.
From Algebra Require Import AffineSpace_def AffineSpace_FF.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Local Open Scope AffineSpace_scope.

Section Barycenter_Def.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

[GostiauxT4] p. 4.
Lemma lc_vectF_uniq :
   {n L} (A : 'E^n) O1 O2,
    sum L = 0 lin_comb L (vectF O1 A) = lin_comb L (vectF O2 A).
Proof.
intros n L A O1 O2 HL; rewrite (vectF_change_orig O1 O2).
rewrite lc_plus_r lc_constF_r HL scal_zero_l plus_zero_l; easy.
Qed.

Definition aff_comb {n} L (A : 'E^n) G : Prop := lin_comb L (vectF G A) = 0.

Lemma ac_w_zero_struct_r :
   {n} L (A : 'E^n) G, zero_struct K aff_comb L A G.
Proof.
move=>> HK; move: (@ms_w_zero_struct_r _ V HK) ⇒ HV.
unfold aff_comb; rewrite vectF_w_zero_struct_r; easy.
Qed.

Lemma ac_compat_l :
   {n} L1 L2 (A : 'E^n) G,
    L1 = L2 aff_comb L1 A G aff_comb L2 A G.
Proof. intros; subst; easy. Qed.

Lemma ac_compat_r :
   {n} L (A1 A2 : 'E^n) G,
    A1 = A2 aff_comb L A1 G aff_comb L A2 G.
Proof. intros; subst; easy. Qed.

Lemma ac_uniq :
   {n} L (A : 'E^n) G1 G2,
    invertible (sum L) aff_comb L A G1 aff_comb L A G2 G1 = G2.
Proof.
unfold aff_comb; intros n L A G1 G2 HL HG1 HG2.
apply eq_sym, vect_zero_equiv, (scal_zero_reg_r (sum L)); try easy.
rewrite -lc_constF_r -(minus_eq_zero 0) -{1}HG1 -HG2 -lc_minus_r; f_equal.
rewrite -plus_minus_r_equiv plus_comm; apply vectF_change_orig.
Qed.

Lemma ac_homogeneous :
   {n} L a (A : 'E^n) G,
    invertible a aff_comb L A G aff_comb (scal a L) A G.
Proof.
intros; unfold aff_comb; rewrite lc_scal_l; split; intros HG.
rewrite HG scal_zero_r; easy.
destruct (scal_zero_rev _ _ HG); easy.
Qed.

Lemma ac_orig_compat :
   {n L} {A : 'E^n} {G} O,
    scal (sum L) (O --> G) = lin_comb L (vectF O A) aff_comb L A G.
Proof.
unfold aff_comb; intros n L A G O HG.
rewrite (vectF_change_orig O) lc_plus_r lc_constF_r.
rewrite -HG vect_sym scal_opp_r plus_opp_l; easy.
Qed.

Lemma ac_orig_reg :
   {n} L (A : 'E^n) G,
    aff_comb L A G
     O, scal (sum L) (O --> G) = lin_comb L (vectF O A).
Proof.
unfold aff_comb; move=>> HG O; move: HG.
rewrite (vectF_change_orig O) lc_plus_r -lc_constF_r.
rewrite vect_sym constF_opp lc_opp_r plus_is_zero_r_equiv opp_opp; easy.
Qed.

Lemma ac_ex :
   {n L} (A : 'E^n), invertible (sum L) G, aff_comb L A G.
Proof.
intros n L A [sLm1 [_ HL]]; destruct (inhabited_as E) as [O].
pose (u := scal sLm1 (lin_comb L (vectF O A))).
destruct (vect_l_bij_ex O u) as [G [HG _]]; G.
apply (ac_orig_compat O); rewrite HG; unfold u.
rewrite scal_assoc HL scal_one; easy.
Qed.

Lemma ac_permutF :
   {n} p {L} (A : 'E^n) G,
    injective p invertible (sum L)
    aff_comb L A G aff_comb (permutF p L) (permutF p A) G.
Proof.
intros; unfold aff_comb; rewrite vectF_permutF lc_permutF//.
Qed.

Lemma ac_revF :
   {n} {L} (A : 'E^n) G,
    invertible (sum L) aff_comb L A G aff_comb (revF L) (revF A) G.
Proof. move=>>; apply ac_permutF, rev_ord_inj. Qed.

Lemma ac_moveF :
   {n} {L} (A : 'E^n.+1) i0 i1 G,
    invertible (sum L)
    aff_comb L A G aff_comb (moveF L i0 i1) (moveF A i0 i1) G.
Proof. move=>>; apply ac_permutF, move_ord_inj. Qed.

Lemma ac_transpF :
   {n} {L} (A : 'E^n) i0 i1 G,
    invertible (sum L)
    aff_comb L A G aff_comb (transpF L i0 i1) (transpF A i0 i1) G.
Proof. move=>>; apply ac_permutF, transp_ord_inj. Qed.

Lemma ac_squeezeF :
   {n} {L} {A : 'E^n.+1} {i0 i1} G,
    i1 i0 A i1 = A i0
    aff_comb L A G aff_comb (squeezeF L i0 i1) (skipF A i1) G.
Proof.
move=>> Hi HA HG; unfold aff_comb.
rewrite vectF_skipF lc_squeezeF// !vectF_correct HA; easy.
Qed.

Lemma baryc_EX :
   {n L} (A : 'E^n), invertible (sum L) { G | aff_comb L A G }.
Proof. intros; apply ex_EX, ac_ex; easy. Qed.

Definition barycenter {n} L (A : 'E^n) : E :=
  match invertible_dec (sum L) with
  | left HLproj1_sig (baryc_EX A HL)
  | right _point_of_as E
  end.

Definition isobarycenter {n} (A : 'E^n) : E := barycenter ones A.

Definition middle (A B : E) : E := isobarycenter (coupleF A B).

Lemma baryc_correct :
   {n L} (A : 'E^n),
    invertible (sum L) aff_comb L A (barycenter L A).
Proof.
intros n L A HL; unfold barycenter;
    destruct (invertible_dec (sum L)) as [HL' | ]; try easy.
apply (proj2_sig (baryc_EX A HL')).
Qed.

Lemma baryc_correct_equiv :
   {n} {L} (A : 'E^n) {G},
    invertible (sum L) G = barycenter L A aff_comb L A G.
Proof.
intros n L A G HL; split.
intros; subst; apply baryc_correct; easy.
intros HG; apply (ac_uniq L A); try apply baryc_correct; easy.
Qed.

Lemma baryc_correct_orig :
   O {n} {L} (A : 'E^n),
    invertible (sum L)
    scal (sum L) (O --> barycenter L A) = lin_comb L (vectF O A).
Proof. intros; apply ac_orig_reg, baryc_correct; easy. Qed.

Lemma baryc_correct_orig_equiv :
   O {n} {L} (A : 'E^n) {G},
    invertible (sum L)
    G = barycenter L A scal (sum L) (O --> G) = lin_comb L (vectF O A).
Proof.
intros O n L A G HL; split.
intros; subst; apply baryc_correct_orig; easy.
intros HG; apply (ac_uniq L A); try easy.
apply (ac_orig_compat _ HG).
apply baryc_correct; easy.
Qed.

Lemma baryc_eq_l :
   {n} {L} M {A : 'E^n}, L = M barycenter L A = barycenter M A.
Proof. intros; f_equal; easy. Qed.

Lemma baryc_eq_r :
   {n} {L A} (B : 'E^n), A = B barycenter L A = barycenter L B.
Proof. intros; f_equal; easy. Qed.

Lemma baryc_eq :
   {n} {L} M {A} (B : 'E^n),
    L = M A = B barycenter L A = barycenter M B.
Proof. intros; f_equal; easy. Qed.

End Barycenter_Def.

Section Barycenter_Facts.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

Lemma baryc_w_zero_struct_r :
   {n} L (A : 'E^n) G, zero_struct K G = barycenter L A.
Proof.
intros; apply baryc_correct_equiv.
apply invertible_zero_struct; easy.
apply ac_w_zero_struct_r; easy.
Qed.

Lemma transl_lc :
   {n} i0 (A : E) L (u : 'V^n),
    A +++ lin_comb L u =
      barycenter (insertF L (1 - sum L) i0) (insertF (translF A u) A i0).
Proof.
intros n i0 A L u; apply (baryc_correct_orig_equiv A);
  rewrite sum_insertF_baryc; try apply invertible_one.
rewrite scal_one transl_correct_r vectF_insertF lc_insertF.
rewrite vect_zero scal_zero_r plus_zero_l vectF_translF; easy.
Qed.

Lemma baryc_insertF :
   {n} i0 O (A : 'E^n) L,
    barycenter (insertF L (1 - sum L) i0) (insertF A O i0) =
      O +++ lin_comb L (vectF O A).
Proof. intros; rewrite (transl_lc i0) translF_vectF; easy. Qed.

Lemma lc_vectF :
   {n} i0 O (A : 'E^n) L,
    lin_comb L (vectF O A) =
      O --> barycenter (insertF L (1 - sum L) i0) (insertF A O i0).
Proof.
intros n i0 O A L; apply (transl_l_inj O).
rewrite -(baryc_insertF i0) transl_correct_l; easy.
Qed.

Lemma lc_vectF_skipF :
   {n} i0 (A : 'E^n.+1) L,
    lin_comb L (vectF (A i0) A) =
      lin_comb (skipF L i0) (vectF (A i0) (skipF A i0)).
Proof.
intros n i0 A L; rewrite (lc_skipF i0) vectF_correct vect_zero
    scal_zero_r plus_zero_l; easy.
Qed.

Lemma lc_vectF_0 :
   {n} (A : 'E^n.+1) L,
    lin_comb L (vectF (A ord0) A) =
      lin_comb (liftF_S L) (vectF (A ord0) (liftF_S A)).
Proof. intros; rewrite -!skipF_first; apply lc_vectF_skipF. Qed.

Lemma lc_vectF_max :
   {n} (A : 'E^n.+1) L,
    lin_comb L (vectF (A ord_max) A) =
      lin_comb (widenF_S L) (vectF (A ord_max) (widenF_S A)).
Proof. intros; rewrite -!skipF_last; apply lc_vectF_skipF. Qed.

Lemma barycenter2_r :
   {n1 n2} L1 (A1 : 'E^n1) M12 (A2 : 'E^n2),
    invertible (sum L1) ( i1, sum (M12 i1) = 1)
    ( i1, A1 i1 = barycenter (M12 i1) A2)
    barycenter L1 A1 = barycenter (fun i2lin_comb L1 (M12^~ i2)) A2.
Proof.
intros n1 n2 L1 A1 M12 A2 HL1 HM12 HA1; pose (O := point_of_as E).
assert (HLM : sum (fun i2lin_comb L1 (M12^~ i2)) = sum L1).
  rewrite -lc_sum_r (lc_ext_r ones).
  apply lc_ones_r.
  intros i1; rewrite (HM12 i1); easy.
apply (baryc_correct_orig_equiv O); rewrite HLM; try easy.
assert (HA1' : i1, O --> A1 i1 = lin_comb (M12 i1) (vectF O A2)).
  intros i1; rewrite -(scal_one (O --> _)) -(HM12 i1).
  apply baryc_correct_orig_equiv; try easy.
  rewrite HM12; apply invertible_one.
rewrite -(lc2_l_alt HA1'); apply baryc_correct_orig; easy.
Qed.

Lemma baryc_kron_l :
   {n} (A : 'E^n) (j : 'I_n), barycenter (kron K ^~ j) A = A j.
Proof.
intros [| n] A j; [now destruct j |].
apply eq_sym, (baryc_correct_orig_equiv (A ord0)); rewrite sum_kron_l//.
apply invertible_one.
rewrite scal_one lc_kron_l_in_l; easy.
Qed.

Lemma baryc_kron_r :
   {n} (A : 'E^n) (i : 'I_n), barycenter (kron K i) A = A i.
Proof.
intros [| n] A i; [now destruct i |].
apply eq_sym, (baryc_correct_orig_equiv (A ord0)); rewrite sum_kron_r//.
apply invertible_one.
rewrite scal_one lc_kron_l_in_r; easy.
Qed.

Lemma baryc_singleF_equiv :
   L0 (A0 : E) G,
    invertible (sum (singleF L0))
    G = barycenter (singleF L0) (singleF A0) scal L0 (G --> A0) = 0.
Proof.
intros; rewrite baryc_correct_equiv; unfold aff_comb; try easy.
rewrite lc_1; easy.
Qed.

Lemma baryc_coupleF_equiv :
   L0 L1 (A0 A1 : E) G,
    invertible (sum (coupleF L0 L1))
    G = barycenter (coupleF L0 L1) (coupleF A0 A1)
    scal L0 (G --> A0) + scal L1 (G --> A1) = 0.
Proof.
intros; rewrite baryc_correct_equiv; unfold aff_comb; try easy.
rewrite lc_2 2!vectF_correct 2!coupleF_0 2!coupleF_1; easy.
Qed.

Lemma baryc_tripleF_equiv :
   L0 L1 L2 (A0 A1 A2 : E) G,
    invertible (sum (tripleF L0 L1 L2))
    G = barycenter (tripleF L0 L1 L2) (tripleF A0 A1 A2)
    scal L0 (G --> A0) + scal L1 (G --> A1) + scal L2 (G --> A2) = 0.
Proof.
intros; rewrite baryc_correct_equiv; unfold aff_comb; try easy.
rewrite lc_3 3!vectF_correct 2!tripleF_0 2!tripleF_1 2!tripleF_2; easy.
Qed.

Lemma isobaryc_correct :
   {n} (A : 'E^n),
    invertible (plusn1 K n) aff_comb ones A (isobarycenter A).
Proof. intros; apply baryc_correct; easy. Qed.

Lemma isobaryc_correct_orig :
   {n} (A : 'E^n) O,
    invertible (plusn1 K n)
    scal (plusn1 K n) (O --> isobarycenter A) = sum (vectF O A).
Proof.
intros; rewrite -lc_ones_l; apply baryc_correct_orig; easy.
Qed.

Lemma isobaryc_correct_equiv :
   {n} (A : 'E^n) G,
    invertible (plusn1 K n)
    G = isobarycenter A aff_comb ones A G.
Proof. intros; apply baryc_correct_equiv; easy. Qed.

Lemma middle_correct :
   (A B : E), let M := middle A B in
    invertible (2 : K) (M --> A) + (M --> B) = 0.
Proof.
rewrite -plusn1_2; intros A B M H2;
    generalize (isobaryc_correct (coupleF A B) H2).
unfold aff_comb; rewrite lc_2 !scal_one
    !vectF_correct coupleF_0 coupleF_1; easy.
Qed.

Lemma middle_correct_orig :
   (A B O : E), let M := middle A B in
    invertible (2 : K) scal 2 (O --> M) = (O --> A) + (O --> B).
Proof.
rewrite -plusn1_2; intros A B O M H2;
    generalize (isobaryc_correct_orig (coupleF A B) O H2).
rewrite sum_2 !vectF_correct coupleF_0 coupleF_1; easy.
Qed.

Lemma middle_correct_equiv :
   (A B M : E), invertible (2 : K)
    M = middle A B (M --> A) + (M --> B) = 0.
Proof.
intros A B M H2; rewrite -plusn1_2 in H2;
    generalize (isobaryc_correct_equiv (coupleF A B) M H2).
unfold aff_comb; rewrite lc_2 !scal_one
    !vectF_correct coupleF_0 coupleF_1; easy.
Qed.

Lemma baryc_homogeneous :
   {n a L} (A : 'E^n),
    invertible a invertible (sum L)
    barycenter L A = barycenter (scal a L) A.
Proof.
intros n a L A Ha HL; apply (ac_uniq L A); try easy.
apply baryc_correct; easy.
apply (ac_homogeneous _ a); try easy.
apply baryc_correct, sum_scal_invertible_compat; easy.
Qed.

Lemma baryc_normalized :
   {n} L (A : 'E^n) G, let L1 := scal (inv (sum L)) L in
    invertible (sum L) G = barycenter L A
    sum L1 = 1 G = barycenter L1 A.
Proof.
intros n L A G L1 HL; generalize HL; intros [a Ha];
    generalize Ha; intros [Ha1 Ha2] HG; rewrite HG.
unfold L1; rewrite (inv_correct Ha); split.
rewrite -scal_sum_distr_l -Ha1; easy.
apply baryc_homogeneous; try easy.
apply (is_inverse_invertible_r (sum L)); easy.
Qed.

Lemma baryc_normal :
   {n} L1 (A : 'E^n) G,
    sum L1 = 1 aff_comb L1 A G G = barycenter L1 A.
Proof.
intros n L1 A G HL1 HG; apply (ac_uniq L1 A); try easy.
2: apply baryc_correct.
1,2: apply invertible_eq_one; easy.
Qed.

Lemma baryc_skip_zero :
   {n} L (A : 'E^n.+1) i0,
    invertible (sum L) L i0 = 0
    barycenter L A = barycenter (skipF L i0) (skipF A i0).
Proof.
intros n L A i0 HL Hi0; apply baryc_correct_equiv; unfold aff_comb.
rewrite -(plus_zero_l (sum _)) -Hi0 -sum_skipF; easy.
rewrite -(plus_zero_l (lin_comb _ _))
    -{1}(scal_zero_l (barycenter L A --> A i0))
    -{1}Hi0 vectF_skipF -lc_skipF.
fold (aff_comb L A (barycenter L A)).
apply baryc_correct; easy.
Qed.

Lemma baryc_squeezeF :
   {n} {L} {A : 'E^n.+1} {i0 i1},
    invertible (sum L) i1 i0 A i1 = A i0
    barycenter L A = barycenter (squeezeF L i0 i1) (skipF A i1).
Proof.
intros n L A i0 i1 HL Hia Hib; apply baryc_correct_equiv.
apply invertible_sum_squeezeF; easy.
apply ac_squeezeF; try easy.
apply baryc_correct; easy.
Qed.

Lemma baryc_injF_ex :
   {n} L (A : 'E^n), invertible (sum L)
     m M (B : 'E^m), invertible (sum M)
      injective B invalF B A barycenter L A = barycenter M B.
Proof.
intros n L A HL; induction n as [| n Hn].
rewrite sum_nil in HL; move: (invertible_zero HL) ⇒ HK.
move: (@as_w_zero_struct_r _ _ E HK) ⇒ [O HE].
0, 0, (constF 0 O); repeat split.
apply invertible_zero_struct; easy.
1,2: intros [i Hi]; easy.
apply baryc_w_zero_struct_r; easy.
destruct (classic (injective A)) as [HA | HA].
n.+1, L, A; repeat split; try apply invalF_refl; easy.
move: HA ⇒ /not_all_ex_not [i1 /not_all_ex_not [i0 Hi]].
move: Hi ⇒ /not_imp_and_equiv [Hia Hib].
destruct (Hn (squeezeF L i0 i1) (skipF A i1)) as [m [M [B [H1 [H2 [H3 H4]]]]]];
    try now apply invertible_sum_squeezeF.
m, M, B; repeat split; try easy.
apply (skipF_monot_r _ _ i1); easy.
rewrite (baryc_squeezeF _ Hib); easy.
Qed.

Lemma baryc_filter_n0F :
   {n} L (A : 'E^n),
    invertible (sum L)
    barycenter L A = barycenter (filter_n0F L) (filter_n0F_gen L A).
Proof.
intros n L A HL. pose (G := barycenter L A); fold G.
apply baryc_correct_equiv; try rewrite -invertible_sum_equiv//.
unfold aff_comb; rewrite vectF_filterPF lc_filter_n0F_l.
apply baryc_correct; easy.
Qed.

Lemma baryc_normalized_n0_ex :
   {n} L (A : 'E^n), invertible (sum L)
     n1 L1 (A1 : 'E^n1), sum L1 = 1 ( i, L1 i 0)
      invalF A1 A barycenter L A = barycenter L1 A1.
Proof.
intros n L A HL.
destruct (baryc_normalized
    (filter_n0F L) (filter_n0F_gen L A) (barycenter L A)) as [HL1 HA1].
rewrite -invertible_sum_equiv//.
apply baryc_filter_n0F; easy.
eexists; (scal (/ sum (filter_n0F L)) (filter_n0F L)),
    (filter_n0F_gen L A); repeat split; try easy.
2: apply filterPF_invalF.
intros; rewrite fct_scal_r_eq; unfold scal; simpl; apply mult_not_zero_l.
apply inv_invertible; rewrite -invertible_sum_equiv//.
apply filter_n0F_correct.
Qed.

Lemma baryc_constF :
   {n} A L (B : 'E^n),
    invertible (sum L) B = constF n A barycenter L B = A.
Proof.
intros n A L B HL HB; subst; symmetry.
apply baryc_correct_equiv, (ac_orig_compat A); try easy.
rewrite vectF_constF -lc_constF_r; easy.
Qed.

Lemma baryc_singleF :
   a A L (B : 'E^1),
    invertible a L = singleF a B = singleF A barycenter L B = A.
Proof.
intros; apply baryc_constF; subst; try now apply sum_singleF_invertible.
apply eq_sym, constF_1.
Qed.

Lemma baryc_permutF :
   {n} p L (A : 'E^n),
    injective p invertible (sum L)
    barycenter (permutF p L) (permutF p A) = barycenter L A.
Proof.
intros n p L A Hp HL; apply eq_sym, baryc_correct_equiv.
rewrite sum_permutF; easy.
apply ac_permutF; try easy.
apply baryc_correct; easy.
Qed.

Lemma baryc_revF :
   {n} L (A : 'E^n),
    invertible (sum L) barycenter (revF L) (revF A) = barycenter L A.
Proof. intros; apply baryc_permutF; [apply rev_ord_inj | easy]. Qed.

Lemma baryc_moveF :
   {n} L (A : 'E^n.+1) i0 i1,
    invertible (sum L)
    barycenter (moveF L i0 i1) (moveF A i0 i1) = barycenter L A.
Proof. intros; apply baryc_permutF; [apply move_ord_inj | easy]. Qed.

Lemma baryc_transpF :
   {n} L (A : 'E^n) i0 i1,
    invertible (sum L)
    barycenter (transpF L i0 i1) (transpF A i0 i1) = barycenter L A.
Proof. intros; apply baryc_permutF; [apply transp_ord_inj | easy]. Qed.

Lemma baryc_unfun0F :
   {n1 n2} L1 (A1 : 'E^n1) (A2 : 'E^n2),
    invertible (sum L1) injective A1 invalF A1 A2
     L2, invalF L1 L2
      invertible (sum L2) barycenter L1 A1 = barycenter L2 A2.
Proof.
moven1 n2 L1 A1 A2 HL1 HA1 HA.
move: (baryc_correct A1 HL1) ⇒ HG1; unfold aff_comb in HG1.
pose (G1 := barycenter L1 A1); fold G1 in HG1; fold G1.
destruct (invalF_fun HA) as [f Hf]; move: (invalF_fun_inj _ HA1 HA Hf) ⇒ Hf'.
assert (HL2 : invertible (sum (unfun0F f L1))) by now rewrite sum_unfun0F.
(unfun0F f L1); repeat split; try easy.
apply unfun0F_ub; easy.
apply baryc_correct_equiv; try easy; unfold aff_comb.
rewrite -lc_filter_n0F_l filter_n0F_unfun0F.
pose (q1 := proj1_sig (injF_restr_bij_EX Hf')); fold q1.
pose (Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf'))); fold q1 in Hq1a.
pose (Hq1b := bij_inj Hq1a).
rewrite 2!lc_castF_l.
rewrite -(lc_permutF Hq1b) -lc_filter_n0F_l in HG1.
rewrite -HG1; f_equal; rewrite -castF_sym_equiv.
apply eq_sym; rewrite -castF_sym_equiv.
rewrite filter_n0F_gen_unfun0F_l; repeat f_equal.
apply extF; intros i1; rewrite !vectF_correct Hf; easy.
Qed.

[GostiauxT4] Th 1.18, pp. 6-7.
Lemma baryc_assoc :
   {n} (b : 'nat^n) L (A : i, 'E^(b i)),
    ( i, invertible (sum (L i)))
    invertible (sum (concatnF L))
    barycenter (concatnF L) (concatnF A) =
      barycenter (fun isum (L i)) (fun ibarycenter (L i) (A i)).
Proof.
intros n b L A HLi HL; destruct (inhabited_as E) as [B].
apply baryc_correct_equiv; try now rewrite -sum_assoc.
apply (ac_orig_compat B).
rewrite -sum_assoc baryc_correct_orig; try easy.
rewrite vectF_concatnF lc_concatnF.
unfold lin_comb; f_equal; apply extF; intros i.
rewrite scalF_correct baryc_correct_orig; easy.
Qed.

Lemma fct_baryc_eq :
   {T : Type} {n} L (fA : '(T E)^n) t,
    invertible (sum L) barycenter L fA t = barycenter L (fA^~ t).
Proof.
intros T n L fA t HL; pose (G := barycenter L fA); fold G.
assert (HG : G = barycenter L fA) by easy.
apply baryc_correct_equiv in HG; try easy.
apply baryc_correct_equiv; try easy; unfold aff_comb in ×.
rewrite -fct_vectF_eq -fct_lc_r_eq HG; easy.
Qed.

End Barycenter_Facts.

Section Barycenter_R_Facts.

Context {V : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.

Lemma baryc_comm_R :
   {n1 n2} L1 L2 (A : 'E^{n1,n2}),
    sum L1 0 sum L2 0
    barycenter L2 (barycenter L1 A) = barycenter L1 (mapF (barycenter L2) A).
Proof.
intros n1 n2 L1 L2 A HL1 HL2; generalize HL1 HL2.
move⇒ /invertible_equiv_R HL1' /invertible_equiv_R HL2'.
pose (G1 := mapF (barycenter L2) A); fold G1.
assert (HG1' : i1, aff_comb L2 (A i1) (G1 i1))
    by now intros; apply baryc_correct_equiv.
unfold aff_comb in HG1'; pose (G1A := fun i1vectF (G1 i1) (A i1)).
assert (HG1 : mapF (lin_comb L2) G1A = 0)
    by now apply extF; intro; rewrite mapF_correct; unfold G1A. clear HG1'.
pose (G2 := barycenter L1 A).
generalize (baryc_correct A HL1'); fold G2; intros HG2.
pose (G := barycenter L2 G2).
generalize (baryc_correct G2 HL2'); fold G; intros HG.
apply baryc_correct_equiv; try easy; unfold aff_comb in ×.
pose (G1s := fun i1constF n2 (G1 i1)).
assert (HGa :
      (fun i1lin_comb L2 (vectF G (G1s i1))) +
      (fun i1lin_comb L2 ((G1s i1) --> G2)) = 0)
    by now apply extF; intro; rewrite fct_plus_eq -lc_plus_r vectF_chasles.
apply (lc_eq_r L1) in HGa.
rewrite lc_plus_r lc_zero_r in HGa.
apply (scal_zero_reg_r_R (sum L2)); try easy.
rewrite -(plus_zero_r (scal _ _)) -{2}HGa; f_equal; clear HGa HG.
rewrite -lc_scal_r; f_equal; apply extF; intro.
rewrite -lc_constF_r fct_lc_r_eq; easy.
symmetry; rewrite (lc_eq_r _ _
    (fun i1lin_comb L2 (vectF (G1 i1) (A i1) +
                            (fun i2(A i1 i2) --> (G2 i2))))).
2: apply extF; intros i1; f_equal; unfold G1s; rewrite vectF_chasles; easy.
rewrite (lc_eq_r _ _
    ((fun i1lin_comb L2 (vectF (G1 i1) (A i1))) +
     (fun i1lin_comb L2 (fun i2A i1 i2 --> G2 i2)))).
2: apply extF; intros i1; rewrite fct_plus_eq; apply lc_plus_r.
rewrite lc_plus_r -(plus_zero_r 0); f_equal.
apply lc_zero_compat_r; rewrite -HG1; apply extF; intros i1.
rewrite mapF_correct; easy.
generalize (lc2_r_sym L1 L2 (fun i1A i1 --> G2));
    rewrite lc_flipT_r; move=>> <-.
apply lc_zero_compat_r.
rewrite opp_zero_equiv -lc_opp_r (lc_eq_r _ _ (vectF G2 A)); try easy.
apply extT; intros i1 i2; rewrite !fct_opp_eq -vect_sym; easy.
Qed.

End Barycenter_R_Facts.

Section Parallelogram.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

Definition parallelogram (A B C D : E) : Prop := A --> B = D --> C.

Lemma parallelogram_shift :
   A B C D, parallelogram A B C D parallelogram B C D A.
Proof.
intros A B C D; unfold parallelogram.
rewrite -(vect_chasles D B C) -(vect_chasles B A D) (plus_comm (B --> D)).
rewrite -plus_compat_r_equiv; easy.
Qed.

Lemma parallelogram_rev :
   A B C D, parallelogram A B C D parallelogram D C B A.
Proof. easy. Qed.

Lemma parallelogram_relation :
   A B C D, parallelogram A B C D parallelogram A D C B.
Proof. intros; rewrite parallelogram_rev -parallelogram_shift; easy. Qed.

Lemma parallelogram_transl_vect :
   O A B, parallelogram O A B (O +++ (A --> B)).
Proof.
intros; apply parallelogram_relation.
unfold parallelogram; rewrite transl_correct_r; easy.
Qed.

Lemma parallelogram_equiv_def :
   A B C D,
    invertible (2 : K) parallelogram A B C D middle A C = middle B D.
Proof.
intros A B C D H; unfold parallelogram; rewrite (middle_correct_equiv _ _ _ H).
rewrite -(vect_chasles A (middle _ _) B) -(vect_chasles C (middle _ _) D).
rewrite plus_assoc (plus_comm (_ --> A)) -(plus_assoc (A --> B)).
rewrite (middle_correct _ _ H) plus_zero_r (vect_sym D) plus_is_zero_l_equiv; easy.
Qed.

Lemma parallelogram_equiv_def_baryc :
   A B C D,
    parallelogram A B C D
    D = barycenter (tripleF 1 (- (1 : K)) 1) (tripleF A B C).
Proof.
intros A B C D; unfold parallelogram.
rewrite baryc_tripleF_equiv; try apply sum_alt_ones_3_invertible.
rewrite scal_opp_l !scal_one -vect_sym (plus_comm (D --> A)) vect_chasles
    plus_comm (vect_sym B) minus_zero_equiv; easy.
Qed.

Lemma transl_vect_baryc :
   (O A B : E),
    O +++ (A --> B) = barycenter (tripleF 1 (- (1 : K)) 1) (tripleF O A B).
Proof.
intros; apply parallelogram_equiv_def_baryc, parallelogram_transl_vect.
Qed.

Lemma transl_vect_baryc_alt :
   (O A B : E),
    B = barycenter (tripleF 1 (- (1 : K)) 1) (tripleF A O (O +++ (A --> B))).
Proof.
intros; apply parallelogram_equiv_def_baryc, parallelogram_shift.
unfold parallelogram; rewrite transl_correct_r; easy.
Qed.

Lemma transl_plus_baryc :
   (O : E) u v,
    O +++ (u + v) =
      barycenter (tripleF 1 (- (1 : K)) 1) (tripleF (O +++ v) O (O +++ u)).
Proof.
intros; apply parallelogram_equiv_def_baryc, parallelogram_shift.
unfold parallelogram; rewrite plus_comm -transl_assoc 2!transl_correct_r; easy.
Qed.

Lemma transl_plus_baryc_alt :
   (O : E) u v,
    O +++ u =
      barycenter (tripleF 1 (- (1 : K)) 1) (tripleF O (O +++ v) (O +++ (u + v))).
Proof.
intros; apply parallelogram_equiv_def_baryc, parallelogram_shift.
unfold parallelogram. rewrite plus_comm -transl_assoc 2!transl_correct_r; easy.
Qed.

Lemma transl_scal_baryc :
   (O : E) a u,
    O +++ scal a u = barycenter (coupleF (1 - a) a) (coupleF O (O +++ u)).
Proof.
intros O a u; apply (baryc_correct_orig_equiv O);
    rewrite sum_coupleF plus_minus_l.
apply invertible_one.
rewrite scal_one vectF_coupleF lc_coupleF
    vect_zero scal_zero_r plus_zero_l.
apply vect_transl_scal.
Qed.

End Parallelogram.

Section ModuleSpace_AffineSpace.

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

Lemma vectF_ms_eq : {n} (O : E) (A : 'E^n), vectF O A = A - constF n O.
Proof. easy. Qed.

Lemma translF_ms_eq :
   {n} (O : E) (u : 'E^n), translF O u = constF n O + u.
Proof.
intros; apply extF; intro; rewrite translF_correct ms_transl_eq; easy.
Qed.

Lemma baryc_ms_eq :
   {n} L (A : 'E^n), sum L = 1 barycenter L A = lin_comb L A.
Proof.
intros n L A HL; apply eq_sym, baryc_correct_equiv.
rewrite HL; apply invertible_one.
unfold aff_comb; rewrite vectF_ms_eq lc_minus_r.
rewrite minus_zero_equiv lc_constF_r HL scal_one; easy.
Qed.

End ModuleSpace_AffineSpace.