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.
[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.
Bibliography
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.
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.
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.
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.
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 i ⇒ LagPd1_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.
sum (fun i ⇒ LagPd1_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 j ⇒ kronR 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.
(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 j ⇒ kronR 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
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 x ⇒ LagPd1_cur Hvtx i x = 0.
'R^dL → Prop
:= fun x ⇒ LagPd1_cur Hvtx i x = 0.
[RR9557v1]
Def 1562, p. 88.
See also Lem 1563, pp. 88-89.
See also Lem 1563, pp. 88-89.
[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.
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.
(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.
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.
(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.
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}.
(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).
(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.+1 ⇒ LagPd1_ref j x_ref) (skipF vtx_cur i).
lin_comb (fun j : 'I_d1.+1 ⇒ LagPd1_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).
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.
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).
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.
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.
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).
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_ModuleSpace ⇒ lin_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.
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_ModuleSpace ⇒ lin_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).
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.
(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.
(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.
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_d1 ⇒ scal (/ 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.
∀ 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_d1 ⇒ scal (/ 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.
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.
∀ 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).
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 i ⇒ LagPd1_ref i x).
split; try easy.
apply LagPd1_ref_sum.
Qed.
funS fullset (face Hvtx i) (T_geom_face vtx_cur i).
Proof.
intros i H1 [x H2].
rewrite face_equiv; try easy.
∃ (fun i ⇒ LagPd1_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}.
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).
(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.
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).
(with pi^d = tau^d_0 from Lem 1367, p. 40, the transposition exchanging 0 and d).
Lemma T_geom_d_0_bij : bijective (T_geom_d_0 vtx_cur).
Proof.
apply T_geom_bij.
apply affine_independent_transpF_equiv; easy.
Qed.
Definition T_geom_d_0_inv : fct_ModuleSpace → fct_ModuleSpace :=
f_inv (T_geom_d_0_bij).
Lemma T_geom_d_0_inv_correct_r : ∀ x_cur : 'R^d,
x_cur = T_geom_d_0 vtx_cur (T_geom_d_0_inv x_cur).
Proof.
intros x_cur; apply esym, f_inv_can_r.
Qed.
Lemma T_geom_d_0_inv_correct_l : ∀ x_ref : 'R^d,
x_ref = T_geom_d_0_inv (T_geom_d_0 vtx_cur x_ref).
Proof.
intros x_ref; apply esym, f_inv_can_l.
Qed.
Proof.
apply T_geom_bij.
apply affine_independent_transpF_equiv; easy.
Qed.
Definition T_geom_d_0_inv : fct_ModuleSpace → fct_ModuleSpace :=
f_inv (T_geom_d_0_bij).
Lemma T_geom_d_0_inv_correct_r : ∀ x_cur : 'R^d,
x_cur = T_geom_d_0 vtx_cur (T_geom_d_0_inv x_cur).
Proof.
intros x_cur; apply esym, f_inv_can_r.
Qed.
Lemma T_geom_d_0_inv_correct_l : ∀ x_ref : 'R^d,
x_ref = T_geom_d_0_inv (T_geom_d_0 vtx_cur x_ref).
Proof.
intros x_ref; apply esym, f_inv_can_l.
Qed.
[RR9557v1]
Lem 1586, p. 96
(with pi^d = tau^d_0 from Lem 1367, p. 40, the transposition exchanging 0 and d).
(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.
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).
(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.
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).
(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.
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.