Library FEM.poly_LagPd1_cur

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.

Bibliography

[RR9557v1] François Clément and Vincent Martin, Finite element method. Detailed proofs to be formalized in Coq, RR-9557, first version, Inria Paris, 2024, https://inria.hal.science/hal-04713897v1.

From Requisite Require Import stdlib_wR ssr_wMC.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Algebra Require Import Algebra_wDep.
From FEM Require Import geometry multi_index geom_simplex geom_transf_affine.
From FEM Require Import poly_Pdk poly_LagPd1_ref.

Local Open Scope R_scope.

Section Poly_LagPd1_cur.

Context {d : nat}.


Context {vtx_cur : '('R^d)^d.+1}.

Hypothesis Hvtx : affine_independent vtx_cur.

[RR9557v1] Lem 1552, p. 84.
Definition LagPd1_cur i x_cur :=
  LagPd1_ref i (T_geom_inv Hvtx x_cur).

Lemma LagPd1_cur_0 : i,
  i = ord0 LagPd1_cur i =
    (fun x : 'R^d ⇒ (1 - sum (T_geom_inv Hvtx x))%R).
Proof.
intros i Hi.
unfold LagPd1_cur.
apply fun_ext; intros x.
rewrite Hi.
rewrite LagPd1_ref_0; easy.
Qed.

Lemma LagPd1_cur_n0 : i (H : i ord0),
  LagPd1_cur i = (fun x : 'R^d ⇒ (T_geom_inv Hvtx x) (lower_S H)).
Proof.
intros i H.
unfold LagPd1_cur.
apply fun_ext; intros x.
rewrite LagPd1_ref_S; easy.
Qed.

Lemma LagPd1_cur_ge_0 : (i : 'I_d.+1) (x : 'R^d),
    convex_envelop vtx_cur x 0 LagPd1_cur i x.
Proof.
intros i x [L HL1 HL2].
unfold LagPd1_cur.
apply LagPd1_ref_ge_0.
rewrite T_geom_inv_transports_baryc; try easy.
Qed.

Lemma LagPd1_cur_le_1 : (i : 'I_d.+1) (x : 'R^d),
    convex_envelop vtx_cur x LagPd1_cur i x 1.
Proof.
intros i x [L HL1 HL2].
unfold LagPd1_cur.
apply LagPd1_ref_le_1.
rewrite T_geom_inv_transports_baryc; try easy.
Qed.

[RR9557v1] Lem 1554, Eq (9.45), p. 85.
Lemma LagPd1_cur_kron_vtx : i j,
  LagPd1_cur j (vtx_cur i) = kronR i j.
Proof.
intros i j.
unfold LagPd1_cur.
rewrite T_geom_inv_transports_vtx; try easy.
apply LagPd1_ref_kron_vtx.
Qed.

[RR9557v1] Lem 1554, p. 85.
See also Lem 1593, p. 98.
Lemma LagPd1_cur_kron_node : (i : 'I_(pbinom d 1).+1) j,
    LagPd1_cur j (node_cur vtx_cur i) = kronR i j.
Proof.
intros; rewrite -(castF_cast_ord (pbinomS_1_r d)) -vtx_cur_node_cur_d1.
apply LagPd1_cur_kron_vtx.
Qed.

[RR9557v1] Lem 1554, Eq (9.46), p. 85.
Lemma LagPd1_cur_sum_1 : x,
  sum (fun iLagPd1_cur i x) = 1.
Proof.
intros x.
unfold LagPd1_cur.
apply LagPd1_ref_sum.
Qed.

Lemma LagPd1_cur_lin_indep : lin_indep LagPd1_cur.
Proof.
unfold LagPd1_cur.
intros L HL.
apply LagPd1_ref_lin_indep.
apply fun_ext; intros x.
rewrite fct_lc_r_eq.
rewrite -(T_geom_inv_can_l Hvtx x).
apply trans_eq with ((lin_comb L
       (fun (i : 'I_d.+1) (x_cur : 'R^d) ⇒
        LagPd1_ref i (T_geom_inv Hvtx x_cur))) (T_geom vtx_cur x)).
rewrite fct_lc_r_eq; easy.
rewrite HL.
easy.
Qed.

Lemma LagPd1_cur_decomp_unique : (x : 'R^d) L,
    x = lin_comb L vtx_cur sum L = 1 L = LagPd1_cur^~ x.
Proof.
intros x L H1 H2.
unfold LagPd1_cur.
rewrite H1.
rewrite T_geom_inv_transports_baryc; try easy.
apply extF; intros i.
rewrite -LagPd1_ref_lc; easy.
Qed.

Lemma LagPd1_cur_decomp : (x : 'R^d),
    x = lin_comb (LagPd1_cur^~ x) vtx_cur.
Proof.
intros x.
destruct (affine_independent_generator _ has_dim_Rn Hvtx x) as [L [HL1 HL2]].
rewrite HL2.
f_equal.
rewrite -HL2.
apply LagPd1_cur_decomp_unique; easy.
Qed.

End Poly_LagPd1_cur.

Section Pd1_Facts.

Context {d : nat}.

Lemma Pd1_lin_span_LagPd1_cur : {vtx_cur}
  (Hvtx : affine_independent vtx_cur),
  Pdk d 1 = lin_span (LagPd1_cur Hvtx).
Proof.
intros v Hv.
apply trans_eq with (lin_span
    (compF_l (castF (eq_sym (pbinomS_1_r d)) LagPd1_ref) (T_geom_inv Hv))).
apply Pdk_am_comp_basis.
apply basis_castF_compat, LagPd1_ref_basis.
apply T_geom_inv_am.
apply f_inv_bij.
apply lin_span_ext; intros i.
apply lin_span_ub with (cast_ord (pbinomS_1_r d) i).
unfold castF, LagPd1_cur; now rewrite eq_sym_involutive.
apply lin_span_ub with (cast_ord (eq_sym (pbinomS_1_r d)) i).
rewrite compF_l_correct; unfold castF, LagPd1_cur.
rewrite cast_ord_comp cast_ord_id; easy.
Qed.

[RR9557v1] Lem 1554, p. 85.
Lemma LagPd1_cur_basis : {vtx_cur}
  (Hvtx:affine_independent vtx_cur),
    basis (Pdk d 1) (LagPd1_cur Hvtx).
Proof.
intros vtx_cur Hvtx.
rewrite (Pd1_lin_span_LagPd1_cur Hvtx); try easy.
apply basis_lin_span_equiv.
apply LagPd1_cur_lin_indep; easy.
Qed.

Lemma LagPd1_cur_decomp_Pd1: {vtx_cur:'('R^d)^d.+1}
   (Hvtx:affine_independent vtx_cur) p, Pdk d 1 p
   p = lin_comb (fun i ⇒ (p (vtx_cur i))) ((LagPd1_cur Hvtx)).
Proof.
intros vtx_cur Hvtx p H.
apply fun_ext;intros x.
destruct (basis_ex_decomp (LagPd1_cur_basis Hvtx) p H) as [L HL].
rewrite HL.
do 2 rewrite fct_lc_r_eq.
apply lc_ext_l.
intro i.
rewrite fct_lc_r_eq.
rewrite (lc_ext_r (fun jkronR i j)) .
rewrite lc_comm_R.
rewrite lc_kron_l_in_r;easy.
apply LagPd1_cur_kron_vtx.
Qed.

End Pd1_Facts.

Section Face_Facts.

[RR9557v1] Lem 1563, Eq (9.57), pp. 88-89.
Note that (face Hvtx i) is the face opposite to v_i
Definition face {dL} {vtx_cur : 'R^{dL.+1,dL}} (Hvtx: affine_independent vtx_cur) (i:'I_dL.+1):
   'R^dL Prop
     := fun xLagPd1_cur Hvtx i x = 0.

[RR9557v1] Def 1562, p. 88.
See also Lem 1563, pp. 88-89.
Definition face_ref {dL} (i:'I_dL.+1): 'R^dL Prop
  := face vtx_ref_affine_independent i.

[RR9557v1] Lem 1564, p. 89.
Lemma face_ref_equiv : {dL} (i:'I_dL.+1) x,
  face_ref i x LagPd1_ref i x = 0.
Proof.
intros dL i x; unfold face_ref, face, LagPd1_cur.
now rewrite T_geom_inv_ref_id.
Qed.

[RR9557v1] Lem 1563, Eq (9.56), p. 88.
Lemma face_equiv : {dL} {vtx_cur : 'R^{dL.+1,dL}}
  (Hvtx: affine_independent vtx_cur) (i:'I_dL.+1) (x : 'R^dL),
  face Hvtx i x
    ( L : 'R^dL, sum L = 1 x = lin_comb L (skipF vtx_cur i)).
Proof.
intros dL vtx_cur Hvtx i x.
split; intros H.
(skipF (LagPd1_cur Hvtx^~ x) i).
split.
apply (plus_reg_l (LagPd1_cur Hvtx i x)).
rewrite -sum_skipF.
rewrite H.
rewrite plus_zero_l.
apply LagPd1_cur_sum_1.
rewrite {1}(LagPd1_cur_decomp Hvtx x).
rewrite (lc_skipF i).
rewrite H scal_zero_l plus_zero_l; easy.
destruct H as [L [HL1 HL2]]; unfold face.
pose (L1 := insertF L 0 i).
assert (Y0 : L1 i = 0) by now apply insertF_correct_l.
assert (Y1 : skipF L1 i = L) by now rewrite skipF_insertF.
assert (H1 : L1 = (LagPd1_cur Hvtx)^~ x).
apply LagPd1_cur_decomp_unique.
rewrite (lc_skipF i) Y0 Y1 -HL2.
now rewrite scal_zero_l plus_zero_l.
now rewrite (sum_skipF _ i) Y0 Y1 HL1 plus_zero_l.
rewrite -(fun_ext_rev H1 i); easy.
Qed.

[RR9557v1] Lem 1605, Eq (9.95), p. 101.
a_alpha \in face_0 <-> alpha \in Cdk.
Lemma node_face0_in_Cdk : {dL kL} {vtx_cur : '('R^dL)^dL.+1}
  (Hvtx: affine_independent vtx_cur) (ipk : 'I_((pbinom dL kL).+1)),
  (0 < dL)%coq_nat (0 < kL)%coq_nat
   ((pbinom dL kL.-1).+1 ipk)%coq_nat
    face Hvtx ord0 (node_cur vtx_cur ipk).
Proof.
intros dL kL vtx_cur Hvtx ipk HdL HkL.
rewrite -Adk_last_layer; try easy.
unfold face, LagPd1_cur.
rewrite -T_geom_transports_node; try easy.
rewrite T_geom_inv_transports_baryc.
2: apply LagPd1_ref_sum.
rewrite LagPd1_ref_0; try easy.
split; intros H1.
apply Rminus_diag_eq, eq_sym.
rewrite lc_ind_l.
rewrite LagPd1_ref_0; try easy.
rewrite (lc_eq_r (liftF_S
        ((LagPd1_ref)^~ (node_ref ipk)))
  (liftF_S vtx_ref) kronR).
rewrite lc_kron_r.
2 :{ unfold vtx_ref, liftF_S.
apply fun_ext; intros i.
destruct (ord_eq_dec (lift_S i) ord0) as [H | H]; try easy.
apply fun_ext; intros j; simpl; f_equal;
auto with zarith. }
rewrite (sum_eq _ (0 + liftF_S
     ((LagPd1_ref)^~ (node_ref ipk)))%M).
rewrite plus_zero_l.
rewrite LagPd1_ref_liftF_S.
unfold node_ref.
rewrite -mult_sum_distr_r -inv_eq_R -one_eq_R; apply div_one_compat.
apply invertible_equiv_R, not_eq_sym, Rlt_not_eq, lt_0_INR; easy.
rewrite sum_INR; f_equal; easy.
f_equal; unfold vtx_ref.
destruct (ord_eq_dec ord0 ord0) as [H | H]; try easy.
rewrite scal_zero_r; easy.
apply Rminus_diag_uniq_sym in H1.
rewrite lc_ind_l in H1.
rewrite LagPd1_ref_0 in H1; try easy.
rewrite (lc_eq_r (liftF_S
        ((LagPd1_ref)^~ (node_ref ipk)))
  (liftF_S vtx_ref) kronR) in H1.
rewrite lc_kron_r in H1.
2 :{ unfold vtx_ref, liftF_S.
apply fun_ext; intros i.
destruct (ord_eq_dec (lift_S i) ord0) as [H | H]; try easy.
apply fun_ext; intros j; simpl; f_equal;
auto with zarith. }
rewrite (sum_eq _ (0 + liftF_S
     ((LagPd1_ref)^~ (node_ref ipk)))%M) in H1.
2 : {f_equal.
unfold vtx_ref.
destruct (ord_eq_dec ord0 ord0) as [H | H]; try easy.
rewrite scal_zero_r; easy. }
rewrite plus_zero_l in H1.
rewrite LagPd1_ref_liftF_S in H1.
unfold node_ref in H1.
rewrite -mult_sum_distr_r -inv_eq_R -one_eq_R in H1; apply div_one_reg in H1.
rewrite sum_mapF in H1; try apply INR_mm.
apply INR_eq; easy.
apply invertible_equiv_R, not_eq_sym, Rlt_not_eq, lt_0_INR; easy.
Qed.

Lemma node_face0_in_Cdk_contra : {dL kL} {vtx_cur : '('R^dL)^dL.+1}
   (Hvtx: affine_independent vtx_cur) (ipk : 'I_((pbinom dL kL).+1)),
  (0 < dL)%coq_nat (0 < kL)%coq_nat
  ¬ face Hvtx ord0 (node_cur vtx_cur ipk)
       (ipk < ((pbinom dL kL.-1).+1))%coq_nat.
Proof.
intros dL kL vtx_cur Hvtx ipk HdL HkL.
apply iff_trans with (B := ¬ ((pbinom dL kL.-1).+1 ipk)%coq_nat).
apply not_iff_compat.
rewrite node_face0_in_Cdk; try easy.
split; intros H.
apply not_ge; easy.
apply Nat.nle_gt; easy.
Qed.

Lemma sub_node_out_face0 : {dL kL} {vtx_cur : '('R^dL)^dL.+1}
  (Hvtx: affine_independent vtx_cur) (ipk : 'I_((pbinom dL kL).+1)),
  (0 < dL)%coq_nat (0 < kL)%coq_nat
  ¬ face Hvtx ord0 (sub_node kL.+1 vtx_cur ipk).
Proof.
intros dL kL vtx_cur Hvtx ipk HdL HkL.
rewrite sub_node_cur_eq; auto with zarith.
apply node_face0_in_Cdk_contra; auto with zarith.
simpl; apply /ltP; easy.
Qed.

[RR9557v1] Lem 1605, Eq (9.96), p. 101.
For j between 0 and d-1, we have node alpha \in face{j+1} iff alpha_j = 0.
Lemma node_faceSj_in_Adkj : {dL kL} {vtx_cur : '('R^dL)^dL.+1}
  (Hvtx: affine_independent vtx_cur) (ipk : 'I_((pbinom dL kL).+1)) (j:'I_dL),
  (0 < dL)%coq_nat (0 < kL)%coq_nat
   Adk dL kL ipk j = O
    face Hvtx (lift_S j) (node_cur vtx_cur ipk).
Proof.
intros dL kL vtx_cur Hvtx ipk j HdL HkL.
unfold face, LagPd1_cur.
rewrite -T_geom_transports_node; try easy.
rewrite T_geom_inv_transports_baryc.
2: apply LagPd1_ref_sum.
rewrite LagPd1_ref_lc.
2: apply LagPd1_ref_sum.
generalize (fun_ext_rev (LagPd1_ref_liftF_S (node_ref ipk)) j); unfold liftF_S; intros T; rewrite T; clear T.
unfold node_ref; split; intros H.
rewrite H; simpl; unfold Rdiv; apply Rmult_0_l.
apply INR_eq.
apply Rmult_eq_reg_r with (/ (INR kL)).
rewrite Rmult_0_l -H; easy.
apply Rinv_neq_0_compat, not_0_INR; auto with zarith.
Qed.

End Face_Facts.

Section T_geom_face_Facts.

Context {d1 : nat}.
Variable vtx_cur : 'R^{d1.+2,d1.+1}.

[RR9557v1] Def 1578, p. 92
(with l=d-1=d1 and pi_l = theta^d_i (i>0) from Lem 1368, p. 41
theta^d_i j = j if j < i, and = j+1 otherwise).
Definition T_geom_face : 'I_d1.+2 'R^d1 'R^d1.+1 := fun i x_ref
    lin_comb (fun j : 'I_d1.+1LagPd1_ref j x_ref) (skipF vtx_cur i).

[RR9557v1] Lem 1584, Eq (9.72), pp. 94-95.
See also Lem 1581, Eq (9.67) first part, p. 93
(with l=d-1=d1 and pi_l = theta^d_0 from Lem 1368, p. 41).
Lemma T_geom_face0_eq : x_ref,
    T_geom_face ord0 x_ref = (vtx_cur ord1 +
         lin_comb x_ref (liftF_S (liftF_S vtx_cur) -
             constF d1 (vtx_cur ord1))%G)%M.
Proof.
unfold T_geom_face; intros x.
rewrite lc_ind_l.
rewrite LagPd1_ref_0; try easy.
rewrite skipF_first.
rewrite liftF_S_0.
rewrite (lc_eq_l _ x _).
rewrite scal_minus_l scal_one.
rewrite lc_minus_r.
unfold lin_comb at 3.
unfold scalF, map2F.
rewrite -scal_sum_distr_r.
rewrite plus_comm 2!plus_assoc; f_equal.
rewrite plus_comm; easy.
apply LagPd1_ref_liftF_S.
Qed.

[RR9557v1] Lem 1584, Eq (9.73), pp. 94-95.
See also Lem 1581, Eq (9.67) first part, p. 93
(with l=d-1=d1 and pi_l = theta^d_i (i>0) from Lem 1368, p. 41).
Lemma T_geom_faceS_eq : i x_ref, i ord0
    T_geom_face i x_ref = (vtx_cur ord0 +
         lin_comb x_ref (liftF_S (skipF vtx_cur i) -
             constF d1 (vtx_cur ord0))%G)%M.
Proof.
intros i x_ref Hi; unfold T_geom_face.
rewrite lc_ind_l.
rewrite LagPd1_ref_0; try easy.
rewrite skipF_correct_l.
2: now apply ord_n0_gt_equiv.
replace (widenF_S vtx_cur ord0) with (vtx_cur ord0).
2: unfold widenF_S; f_equal; apply ord_inj; easy.
rewrite scal_minus_l scal_one.
rewrite -plus_assoc; f_equal.
rewrite scal_sum_distr_r.
unfold lin_comb; rewrite plus_comm.
rewrite -minus_eq -sum_minus.
apply sum_ext; intros j.
rewrite LagPd1_ref_liftF_S.
rewrite -scalF_minus_r; easy.
Qed.

[RR9557v1] Lem 1584, pp. 94-95.
Lemma T_geom_face_am : i, aff_map (T_geom_face i : fct_ModuleSpace fct_ModuleSpace).
Proof.
intros i; case (ord_eq_dec i ord0); intros Hi.
subst; eapply am_ext.
intros x; rewrite T_geom_face0_eq.
rewrite plus_comm; easy.
apply: am_lm_ms.
apply lc_lm_l.
eapply am_ext.
intros x; rewrite (T_geom_faceS_eq _ _ Hi).
rewrite plus_comm; easy.
apply: am_lm_ms.
apply lc_lm_l.
Qed.

[RR9557v1] Lem 1584, Eq (9.73), pp. 94-95.
See also Lem 1581, Eq (9.67) with B{pi_l}, p. 93
(with l=d-1=d1 and pi_l = theta^d_i (i>0) from Lem 1368, p. 41).
Lemma T_geom_face0_fct_lm_eq : (x_ref : 'R^d1),
  fct_lm (T_geom_face ord0 : fct_ModuleSpace fct_ModuleSpace) 0%M x_ref =
    lin_comb x_ref (liftF_S (liftF_S vtx_cur) -
        constF d1 (vtx_cur ord1))%G.
Proof.
intros x_ref.
pose (c2 := vtx_cur ord1); fold c2.
pose (lf := fun x_ref : fct_ModuleSpacelin_comb x_ref (liftF_S (liftF_S vtx_cur) - constF d1 c2)%G : fct_ModuleSpace).
rewrite (fct_lm_ext _ (lf + (fun c2))%M).
rewrite fct_lm_ms_cst_reg.
rewrite fct_lm_ms_lin; try easy.
apply lc_lm_l.
intros x.
unfold lf.
rewrite T_geom_face0_eq plus_comm; easy.
Qed.

[RR9557v1] Lem 1584, Eq (9.73), pp. 94-95.
See also Lem 1581, Eq (9.67) with B{pi_l}, p. 93
(with l=d-1=d1 and pi_l = theta^d_i (i>0) from Lem 1368, p. 41).
Lemma T_geom_faceS_fct_lm_eq : i (x_ref : 'R^d1),
  (i ord0)
  fct_lm (T_geom_face i : fct_ModuleSpace fct_ModuleSpace) 0%M x_ref =
     lin_comb x_ref (liftF_S (skipF vtx_cur i) -
                constF d1 (vtx_cur ord0))%G.
Proof.
intros i x_ref Hi.
pose (c2 := vtx_cur ord0); fold c2.
pose (lf := fun x_ref : fct_ModuleSpace ⇒ (lin_comb x_ref (liftF_S (skipF vtx_cur i) -
                constF d1 (vtx_cur ord0)))%G).
rewrite (fct_lm_ext _ (lf + (fun c2))%M).
rewrite fct_lm_ms_cst_reg.
rewrite fct_lm_ms_lin; try easy.
apply lc_lm_l.
intros x.
unfold lf.
rewrite T_geom_faceS_eq; try easy.
rewrite fct_plus_eq plus_comm; easy.
Qed.

Lemma T_geom_face0_eq2 : (x_ref : 'R^d1),
  T_geom_face ord0 x_ref = (scal (1%R - sum x_ref)%G (vtx_cur ord1) +
     lin_comb x_ref (liftF_S (liftF_S vtx_cur)))%M.
Proof.
intros x_ref; rewrite T_geom_face0_eq.
rewrite scal_distr_r scal_one lc_minus_r lc_constF_r
 scal_opp_l.
unfold minus at 1; simpl.
rewrite -plus_assoc; symmetry; f_equal.
rewrite plus_comm; easy.
Qed.

Lemma T_geom_faceS_eq2 : i (x_ref : 'R^d1),
  i ord0
  T_geom_face i x_ref = (scal (1%R - sum x_ref)%G (vtx_cur ord0) +
     lin_comb x_ref (liftF_S (skipF vtx_cur i)))%M.
Proof.
intros i x_ref Hi; rewrite T_geom_faceS_eq; try easy.
rewrite scal_distr_r scal_one lc_minus_r lc_constF_r
 scal_opp_l.
unfold minus at 1; simpl.
rewrite -plus_assoc; symmetry; f_equal.
rewrite plus_comm; easy.
Qed.

[RR9557v1] Lem 1585, p. 95.
Lemma T_geom_face_comp : i k (p : FRd d1.+1),
    (Pdk d1.+1 k) p
      (Pdk d1 k) (p \o T_geom_face i).
Proof.
intros i k p Hp.
apply Pdk_comp_am; try easy.
apply T_geom_face_am.
Qed.

[RR9557v1] Lem 1607, p. 102, case i=0.
See also Rem 1606.
Lemma T_geom_face0_map_node :
   k (ipk : 'I_(pbinom d1 k).+1), (0 < k)%coq_nat
    T_geom_face ord0 (node_ref ipk) =
      node_cur vtx_cur
         (Adk_inv d1.+1 k (T_node_face_0 ipk)).
Proof.
intros k ipk Hk.
unfold node_cur, node_ref.
rewrite Adk_inv_correct_r.
2: rewrite T_node_face_0_sum; easy.
rewrite -scal_sum_distr_l.
replace (sum (mapF _ _)) with (INR k).
2 : {rewrite sum_INR; f_equal.
rewrite T_node_face_0_sum; easy. }
rewrite lc_scal_l.
unfold scal; simpl.
unfold fct_scal, mult; simpl.
rewrite Rinv_l.
rewrite minus_eq_zero.
unfold plus; simpl.
unfold fct_plus, scal, zero; simpl.
unfold mult, plus; simpl.
apply extF; intros i.
unfold T_node_face_0, Slice_op.
rewrite Rmult_0_l Rplus_0_l mapF_castF castF_id mapF_concatF.
rewrite (lc_splitF_r (mapF INR (singleF (k - sum (Adk d1 k ipk))%coq_nat))
      (mapF INR (Adk d1 k ipk))).
rewrite lc_1 mapF_singleF singleF_0.
rewrite T_geom_face0_eq2.
rewrite Rmult_plus_distr_l fct_plus_eq.
unfold plus, Rdiv; simpl; f_equal.
rewrite -mult_sum_distr_r mult_comm_R fct_scal_r_eq.
assert (H : (a b : R),
  a 0%R
  (1%R - ((/ a)%R × b)%K)%G = (/a × (a - b)%G)%R).
intros a b Ha.
unfold mult, minus, plus, opp; simpl.
field_simplify; easy.
rewrite H.
rewrite -scal_assoc.
unfold scal at 1; simpl.
rewrite sum_INR minus_INR.
unfold mult; simpl; f_equal.
rewrite fct_scal_r_eq; f_equal.
rewrite -liftF_S_0.
unfold firstF; f_equal.
unfold first_ord, lshift.
apply ord_inj; easy.
apply Adk_sum.
apply not_0_INR, nat_neq_0_equiv; easy.
rewrite -lastF_S1p.
unfold castF_S1p.
rewrite castF_id.
rewrite 2!fct_lc_r_eq.
unfold mapF, mapiF, Rdiv.
rewrite (lc_eq_l (fun i0 : 'I_d1
   (INR (Adk d1 k ipk i0) × / INR k)%R)
  (fun i0 : 'I_d1scal (/ INR k)%R
   (INR (Adk d1 k ipk i0))%R) _).
rewrite lc_scal_l.
unfold scal; simpl.
unfold mult; simpl; f_equal.
apply extF; intros j.
unfold scal; simpl.
rewrite Rmult_comm.
unfold mult; simpl; easy.
apply not_0_INR, nat_neq_0_equiv; easy.
Qed.

[RR9557v1] Lem 1607, p. 102, case i>0.
See also Rem 1606.
Lemma T_geom_faceS_map_node :
   k (i:'I_d1.+1) (ipk : 'I_(pbinom d1 k).+1), (0 < k)%coq_nat
    T_geom_face (lift_S i) (node_ref ipk) =
      node_cur vtx_cur
         (Adk_inv d1.+1 k (T_node_face_S i ipk)).
Proof.
intros k i ipk Hk.
rewrite node_cur_eq.
rewrite Adk_inv_correct_r.
2: rewrite T_node_face_S_sum.
2: apply Adk_sum.
rewrite T_geom_faceS_eq; try easy.
f_equal.
rewrite (lc_skipF i).
rewrite mapF_correct fct_scal_eq.
replace (T_node_face_S i ipk i) with O.
2: unfold T_node_face_S.
2: now rewrite insertF_correct_l.
rewrite scal_zero_r scal_zero_l plus_zero_l.
apply lc_ext.
intros j; unfold node_ref.
unfold skipF, scal; simpl; unfold fct_scal; simpl.
unfold scal; simpl; unfold mult; simpl.
unfold Rdiv; rewrite Rmult_comm; f_equal; f_equal.
unfold T_node_face_S.
rewrite -{1}(skipF_insertF (Adk d1 k ipk) O i); easy.
intros j.
unfold liftF_S, skipF, constF; simpl.
unfold minus, plus, opp; simpl.
unfold fct_plus, fct_opp; simpl; f_equal; f_equal.
case (lt_dec j i); intros Hij.
rewrite skip_ord_correct_l.
rewrite skip_ord_correct_l; try easy.
apply ord_inj; easy.
rewrite 2!lift_S_correct; auto with zarith.
rewrite skip_ord_correct_r.
rewrite skip_ord_correct_r; try easy.
rewrite 2!lift_S_correct; auto with zarith.
Qed.

End T_geom_face_Facts.

Section T_geom_face_inv_Facts.

Context {d1 : nat}.

Context {vtx_cur : 'R^{d1.+2,d1.+1}}.

Variable Hvtx : affine_independent vtx_cur.

[RR9557v1] Lem 1584, pp. 94-95.
See also Lem 1581, Eq (9.69), p. 93
(with pi_l = theta^d_i (i>0) from Lem 1368, p. 41).
Lemma T_geom_face_in_face : i,
  funS fullset (face Hvtx i) (T_geom_face vtx_cur i).
Proof.
intros i H1 [x H2].
rewrite face_equiv; try easy.
(fun iLagPd1_ref i x).
split; try easy.
apply LagPd1_ref_sum.
Qed.

[RR9557v1] Lem 1584, case i>0, pp. 94-95.
Lemma T_geom_face_bijS : i,
    bijS fullset (face Hvtx i) (T_geom_face vtx_cur i).
Proof.
intros i; case (ord_eq_dec i ord0); intros Hi.
subst.
apply (injS_surjS_bijS inhabited_fct_ms).
apply T_geom_face_in_face; easy.
rewrite (injS_aff_lin_equiv_alt invertible_2 cas_fullset
  (T_geom_face_am vtx_cur ord0) 0%M); try easy.
intros x [_ Hx].
apply (affine_independent_skipF ord0 Hvtx).
rewrite skipF_first liftF_S_0.
rewrite -T_geom_face0_fct_lm_eq; easy.
intros y Hy.
rewrite (face_equiv Hvtx ord0 y) in Hy.
destruct Hy as [L [H1 H2]].
(liftF_S L).
split; try easy.
rewrite H2; unfold T_geom_face.
apply lc_eq_l.
apply extF; intros i.
rewrite LagPd1_ref_of_liftF_S; easy.
apply (injS_surjS_bijS inhabited_fct_ms).
apply T_geom_face_in_face; try easy.
rewrite (injS_aff_lin_equiv_alt invertible_2 cas_fullset
  (T_geom_face_am vtx_cur i) 0%M); try easy.
intros x [_ Hx].
apply (affine_independent_skipF i Hvtx).
rewrite skipF_correct_l.
2: now apply ord_n0_gt_equiv.
rewrite widenF_S_0.
rewrite -T_geom_faceS_fct_lm_eq; easy.
intros y Hy.
rewrite (face_equiv Hvtx i y) in Hy.
destruct Hy as [L [H1 H2]].
(liftF_S L).
split; try easy.
rewrite H2; unfold T_geom_face.
apply lc_eq_l.
apply extF; intros j.
rewrite LagPd1_ref_of_liftF_S; easy.
Qed.

Definition T_geom_face_inv (i:'I_d1.+2) : 'R^d1.+1 'R^d1 :=
   f_invS (T_geom_face_bijS i).

End T_geom_face_inv_Facts.

Section T_geom_d_0_Def.

Context {d : nat}.
Variable vtx_cur : 'R^{d.+1,d}.

[RR9557v1] Lem 1586, p. 96
(with pi^d = tau^d_0 from Lem 1367, p. 40, the transposition exchanging 0 and d).
Definition T_geom_d_0 : fct_ModuleSpace fct_ModuleSpace :=
    T_geom (transpF vtx_cur ord_max ord0).

End T_geom_d_0_Def.

Section T_geom_d_0_Facts.

Context {d : nat}.
Context {vtx_cur : 'R^{d.+1,d}}.
Hypothesis Hvtx: affine_independent vtx_cur.

[RR9557v1] Lem 1586, p. 96
(with pi^d = tau^d_0 from Lem 1367, p. 40, the transposition exchanging 0 and d).
[RR9557v1] Lem 1586, p. 96
(with pi^d = tau^d_0 from Lem 1367, p. 40, the transposition exchanging 0 and d).
Lemma T_geom_d_0_am : aff_map (T_geom_d_0 vtx_cur).
Proof. apply T_geom_am. Qed.

Lemma T_geom_d_0_inv_am : aff_map T_geom_d_0_inv.
Proof.
apply am_bij_compat.
apply T_geom_d_0_am.
Qed.

Lemma T_geom_d_0_comp : k (p : FRd d),
    (Pdk d k) p
    (Pdk d k) (p \o (T_geom_d_0 vtx_cur)).
Proof.
intros k p Hp.
apply Pdk_comp_am; try easy.
apply T_geom_d_0_am; easy.
Qed.

Lemma T_geom_d_0_inv_comp : k (p : FRd d),
   (Pdk d k) p
      (Pdk d k) (p \o T_geom_d_0_inv).
Proof.
intros k p Hp.
apply Pdk_comp_am; try easy.
apply T_geom_d_0_inv_am.
Qed.

Lemma LagPd1_cur_T_geom_d_0_inv : i x,
  LagPd1_cur Hvtx i x =
    transpF LagPd1_ref ord0 ord_max i (T_geom_d_0_inv x).
Proof.
intros i x; unfold LagPd1_cur.
generalize i; apply fun_ext_equiv.
assert (H : sum
  ((transpF LagPd1_ref ord0 ord_max)^~ (T_geom_d_0_inv x)) = 1%K).
rewrite -sum_fun_compat sum_transpF sum_fun_compat.
apply LagPd1_ref_sum; easy.
eapply baryc_coord_uniq.
apply (affine_independent_equiv vtx_cur); easy.
apply LagPd1_ref_sum.
easy.
rewrite !baryc_ms_eq; try easy.
2: apply LagPd1_ref_sum.
apply trans_eq with (T_geom vtx_cur (T_geom_inv Hvtx x)); try easy.
rewrite T_geom_inv_can_r; try easy.
apply trans_eq with
  (T_geom_d_0 vtx_cur (T_geom_d_0_inv x)).
apply T_geom_d_0_inv_correct_r.
unfold T_geom_d_0, T_geom; rewrite -lc_transpF_l; f_equal.
unfold transpF, permutF; apply extF; intros j; f_equal.
rewrite transp_ord_sym; easy.
Qed.

[RR9557v1] Lem 1586, Eq (9.77), pp. 96-97
(with pi^d = tau^d_0 from Lem 1367, p. 40,
the transposition exchanging 0 and d).
Lemma LagPd1_ref_T_geom_d_0 : i x,
  transpF LagPd1_ref ord0 ord_max i x =
    LagPd1_cur Hvtx i (T_geom_d_0 vtx_cur x).
Proof.
intros i x.
rewrite LagPd1_cur_T_geom_d_0_inv.
f_equal; apply T_geom_d_0_inv_correct_l.
Qed.

[RR9557v1] Lem 1586, Eq (9.78), pp. 96-97
(with pi^d = tau^d_0 from Lem 1367, p. 40,
the transposition exchanging 0 and d).
Lemma T_geom_d_0_in_face0: x_ref,
  face_ref ord_max x_ref
  face Hvtx ord0 (T_geom_d_0 vtx_cur x_ref).
Proof.
intros x_ref; unfold face.
replace 0 with (@zero R_AbelianMonoid) by easy.
rewrite -(Ker_comp_l_alt (transpF (LagPd1_ref) ord0 ord_max ord0)).
2 : apply bij_surj, T_geom_d_0_bij.
2 : { apply fun_ext; intros x.
rewrite comp_correct.
rewrite -LagPd1_ref_T_geom_d_0; easy. }
rewrite transpF_correct_l0; try easy.
rewrite -RgS_ex.
rewrite face_ref_equiv.
split; try easy.
intros H; inversion H as [y Hy1 Hy2].
replace x_ref with y; try easy.
apply (bij_inj T_geom_d_0_bij); easy.
Qed.

End T_geom_d_0_Facts.