Library FEM.poly_LagPd1_ref
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 poly_Pdk geom_simplex.
Local Open Scope R_scope.
Section Poly_LagPd1_ref.
Context {d : nat}.
[RR9557v1]
Def 1541, p. 81.
For simplices (P1 in dim d), with x = (x_i)_{i=1..d}:
For simplices (P1 in dim d), with x = (x_i)_{i=1..d}:
- LagPd1_ref 0 x = 1 - \sum{i=1}^d x_i,
- LagPd1_ref i x = x(i-1), for i=1..d.
Definition LagPd1_ref : '(FRd d)^d.+1 :=
fun j x ⇒ match (ord_eq_dec j ord0) with
| left _ ⇒ 1 - sum x
| right Hj ⇒ x (lower_S Hj)
end.
Lemma LagPd1_ref_0 :
∀ {j}, j = ord0 → LagPd1_ref j = fun x ⇒ (1 - sum x)%G.
Proof. intros; unfold LagPd1_ref; case (ord_eq_dec _ _); easy. Qed.
Lemma LagPd1_ref_S :
∀ {j} (Hj : j ≠ ord0), LagPd1_ref j = fun x ⇒ x (lower_S Hj).
Proof.
intros; unfold LagPd1_ref; case (ord_eq_dec _ _);
[| intros; apply fun_ext; intros; f_equal; apply ord_inj]; easy.
Qed.
Lemma LagPd1_ref_liftF_S : ∀ x, liftF_S (LagPd1_ref^~ x) = x.
Proof.
intros; apply extF; intros j; unfold liftF_S.
rewrite (LagPd1_ref_S (lift_S_not_first _)) lower_lift_S; easy.
Qed.
Lemma LagPd1_ref_liftF_S_alt : liftF_S LagPd1_ref = fun j : 'I_d ⇒ @^~ j.
Proof.
apply extF; intros j; unfold liftF_S.
rewrite (LagPd1_ref_S (lift_S_not_first _)) lower_lift_S; easy.
Qed.
Lemma LagPd1_ref_of_liftF_S :
∀ i (x : 'R^d.+1), sum x = 1 → LagPd1_ref i (liftF_S x) = x i.
Proof.
intros i x Hx; destruct (ord_eq_dec i ord0) as [-> | Hi].
rewrite LagPd1_ref_0// -Hx sum_ind_l minus_plus_r; easy.
rewrite LagPd1_ref_S liftF_lower_S; easy.
Qed.
fun j x ⇒ match (ord_eq_dec j ord0) with
| left _ ⇒ 1 - sum x
| right Hj ⇒ x (lower_S Hj)
end.
Lemma LagPd1_ref_0 :
∀ {j}, j = ord0 → LagPd1_ref j = fun x ⇒ (1 - sum x)%G.
Proof. intros; unfold LagPd1_ref; case (ord_eq_dec _ _); easy. Qed.
Lemma LagPd1_ref_S :
∀ {j} (Hj : j ≠ ord0), LagPd1_ref j = fun x ⇒ x (lower_S Hj).
Proof.
intros; unfold LagPd1_ref; case (ord_eq_dec _ _);
[| intros; apply fun_ext; intros; f_equal; apply ord_inj]; easy.
Qed.
Lemma LagPd1_ref_liftF_S : ∀ x, liftF_S (LagPd1_ref^~ x) = x.
Proof.
intros; apply extF; intros j; unfold liftF_S.
rewrite (LagPd1_ref_S (lift_S_not_first _)) lower_lift_S; easy.
Qed.
Lemma LagPd1_ref_liftF_S_alt : liftF_S LagPd1_ref = fun j : 'I_d ⇒ @^~ j.
Proof.
apply extF; intros j; unfold liftF_S.
rewrite (LagPd1_ref_S (lift_S_not_first _)) lower_lift_S; easy.
Qed.
Lemma LagPd1_ref_of_liftF_S :
∀ i (x : 'R^d.+1), sum x = 1 → LagPd1_ref i (liftF_S x) = x i.
Proof.
intros i x Hx; destruct (ord_eq_dec i ord0) as [-> | Hi].
rewrite LagPd1_ref_0// -Hx sum_ind_l minus_plus_r; easy.
rewrite LagPd1_ref_S liftF_lower_S; easy.
Qed.
[RR9557v1]
Lem 1543, Eq (9.32), p. 81.
Lemma LagPd1_ref_kron_vtx :
∀ (i j : 'I_d.+1), LagPd1_ref j (vtx_ref i) = kronR i j.
Proof.
intros i j.
destruct (ord_eq_dec j ord0) as [-> | Hj];
[rewrite LagPd1_ref_0// | rewrite LagPd1_ref_S//];
(destruct (ord_eq_dec i ord0) as [-> | Hi];
[rewrite vtx_ref_0// | rewrite vtx_ref_kron//]).
rewrite sum_zero_compat// minus_zero_r kronR_is_1; easy.
rewrite sum_kron_r// minus_eq_zero kronR_is_0;
[| contradict Hi; apply ord_inj]; easy.
rewrite kronR_is_0; [| contradict Hj; apply ord_inj]; easy.
simpl; apply kron_pred_eq;
[contradict Hi | contradict Hj]; apply ord_inj; easy.
Qed.
Lemma LagPd1_ref_S_sum : ∀ x, sum (liftF_S (LagPd1_ref^~ x)) = sum x.
Proof. intros; rewrite LagPd1_ref_liftF_S; easy. Qed.
∀ (i j : 'I_d.+1), LagPd1_ref j (vtx_ref i) = kronR i j.
Proof.
intros i j.
destruct (ord_eq_dec j ord0) as [-> | Hj];
[rewrite LagPd1_ref_0// | rewrite LagPd1_ref_S//];
(destruct (ord_eq_dec i ord0) as [-> | Hi];
[rewrite vtx_ref_0// | rewrite vtx_ref_kron//]).
rewrite sum_zero_compat// minus_zero_r kronR_is_1; easy.
rewrite sum_kron_r// minus_eq_zero kronR_is_0;
[| contradict Hi; apply ord_inj]; easy.
rewrite kronR_is_0; [| contradict Hj; apply ord_inj]; easy.
simpl; apply kron_pred_eq;
[contradict Hi | contradict Hj]; apply ord_inj; easy.
Qed.
Lemma LagPd1_ref_S_sum : ∀ x, sum (liftF_S (LagPd1_ref^~ x)) = sum x.
Proof. intros; rewrite LagPd1_ref_liftF_S; easy. Qed.
[RR9557v1]
Lem 1543, Eq (9.33), p. 81.
Lemma LagPd1_ref_sum : ∀ x, sum (LagPd1_ref^~ x) = 1.
Proof.
intros; rewrite sum_ind_l LagPd1_ref_0// LagPd1_ref_S_sum plus_minus_l; easy.
Qed.
Lemma LagPd1_ref_am :
∀ i, aff_map (LagPd1_ref i : fct_ModuleSpace → R_ModuleSpace).
Proof.
intros i; apply am_lm_0; destruct (ord_eq_dec i ord0) as [-> | Hi].
apply (lm_ext (- fun x ⇒ sum x)%G); [| apply lm_fct_opp, lm_component_sum].
intros; rewrite fct_minus_eq LagPd1_ref_0// sum_zero minus_zero_r minus2_l//.
apply (lm_ext (fun x ⇒ x (lower_S Hi))); [| apply lm_component].
intros; rewrite LagPd1_ref_S fct_zero_eq minus_zero_r; easy.
Qed.
Lemma LagPd1_ref_lc :
∀ L i, sum L = 1 → LagPd1_ref i (lin_comb L vtx_ref) = L i.
Proof.
intros L i HL; rewrite am_ac_compat//; [| apply LagPd1_ref_am].
rewrite (lc_ext_r (kronR i));
[| intros; rewrite kronR_sym; apply LagPd1_ref_kron_vtx].
apply lc_kron_r_in_r.
Qed.
Lemma LagPd1_ref_ge_0 :
∀ i (x : 'R^d), convex_envelop vtx_ref x → 0 ≤ LagPd1_ref i x.
Proof. intros i x [L HL1 HL2]; rewrite LagPd1_ref_lc; easy. Qed.
Lemma LagPd1_ref_le_1 :
∀ i (x : 'R^d), convex_envelop vtx_ref x → LagPd1_ref i x ≤ 1.
Proof.
intros i x [L HL1 HL2]; rewrite LagPd1_ref_lc// -HL2.
apply sum_nonneg_ub_R; easy.
Qed.
Lemma LagPd1_ref_surj :
∀ (L : 'R^d.+1), sum L = 1 → ∃ x, LagPd1_ref^~ x = L.
Proof.
intros L HL; ∃ (liftF_S L); apply extF; intros i;
destruct (ord_eq_dec i ord0) as [-> | Hi].
rewrite LagPd1_ref_0// -HL sum_ind_l; apply: minus_plus_r.
rewrite LagPd1_ref_S; apply liftF_lower_S.
Qed.
Lemma LagPd1_ref_inj :
∀ (x y : 'R^d), (∀ i, LagPd1_ref i x = LagPd1_ref i y) → x = y.
Proof.
intros x y H; apply extF; intro;
rewrite -(LagPd1_ref_liftF_S x) -(LagPd1_ref_liftF_S y); apply H.
Qed.
Proof.
intros; rewrite sum_ind_l LagPd1_ref_0// LagPd1_ref_S_sum plus_minus_l; easy.
Qed.
Lemma LagPd1_ref_am :
∀ i, aff_map (LagPd1_ref i : fct_ModuleSpace → R_ModuleSpace).
Proof.
intros i; apply am_lm_0; destruct (ord_eq_dec i ord0) as [-> | Hi].
apply (lm_ext (- fun x ⇒ sum x)%G); [| apply lm_fct_opp, lm_component_sum].
intros; rewrite fct_minus_eq LagPd1_ref_0// sum_zero minus_zero_r minus2_l//.
apply (lm_ext (fun x ⇒ x (lower_S Hi))); [| apply lm_component].
intros; rewrite LagPd1_ref_S fct_zero_eq minus_zero_r; easy.
Qed.
Lemma LagPd1_ref_lc :
∀ L i, sum L = 1 → LagPd1_ref i (lin_comb L vtx_ref) = L i.
Proof.
intros L i HL; rewrite am_ac_compat//; [| apply LagPd1_ref_am].
rewrite (lc_ext_r (kronR i));
[| intros; rewrite kronR_sym; apply LagPd1_ref_kron_vtx].
apply lc_kron_r_in_r.
Qed.
Lemma LagPd1_ref_ge_0 :
∀ i (x : 'R^d), convex_envelop vtx_ref x → 0 ≤ LagPd1_ref i x.
Proof. intros i x [L HL1 HL2]; rewrite LagPd1_ref_lc; easy. Qed.
Lemma LagPd1_ref_le_1 :
∀ i (x : 'R^d), convex_envelop vtx_ref x → LagPd1_ref i x ≤ 1.
Proof.
intros i x [L HL1 HL2]; rewrite LagPd1_ref_lc// -HL2.
apply sum_nonneg_ub_R; easy.
Qed.
Lemma LagPd1_ref_surj :
∀ (L : 'R^d.+1), sum L = 1 → ∃ x, LagPd1_ref^~ x = L.
Proof.
intros L HL; ∃ (liftF_S L); apply extF; intros i;
destruct (ord_eq_dec i ord0) as [-> | Hi].
rewrite LagPd1_ref_0// -HL sum_ind_l; apply: minus_plus_r.
rewrite LagPd1_ref_S; apply liftF_lower_S.
Qed.
Lemma LagPd1_ref_inj :
∀ (x y : 'R^d), (∀ i, LagPd1_ref i x = LagPd1_ref i y) → x = y.
Proof.
intros x y H; apply extF; intro;
rewrite -(LagPd1_ref_liftF_S x) -(LagPd1_ref_liftF_S y); apply H.
Qed.
[RR9557v1]
Lem 1543, p. 81.
Lemma LagPd1_ref_lin_indep : lin_indep LagPd1_ref.
Proof.
intros L; rewrite lc_ind_l LagPd1_ref_0// LagPd1_ref_liftF_S_alt; intros HL.
apply extF; intros i; destruct (ord_eq_dec i ord0) as [-> | Hi].
move: (fun_ext_rev HL 0%M).
rewrite fct_plus_eq fct_scal_r_eq fct_lc_r_eq.
rewrite sum_zero minus_zero_r scal_one_r// lc_zero_r plus_zero_r; easy.
move: (fun_ext_rev HL (kronR (lower_S Hi))).
rewrite fct_plus_eq fct_scal_r_eq fct_lc_r_eq.
rewrite sum_kron_r// minus_eq_zero scal_zero_r plus_zero_l.
rewrite lc_kron_r_in_r liftF_lower_S; easy.
Qed.
End Poly_LagPd1_ref.
Section Pd1_Facts.
Context {d : nat}.
Lemma LagPd1_ref_S_Monom_d1 :
liftF_S (Monom_dk d 1) = liftF_S (castF (eq_sym (pbinomS_1_r d)) LagPd1_ref).
Proof.
apply extF; intros i; unfold liftF_S; rewrite castF_eq_sym.
move: (lift_S_not_first i) ⇒ Hi0.
assert (Hi1 : cast_ord (pbinomS_1_r d) (lift_S i) ≠ ord0)
by now apply cast_ordS_n0.
rewrite LagPd1_ref_S Monom_d1_S.
apply fun_ext; intros x; do 2 f_equal; easy.
Qed.
Proof.
intros L; rewrite lc_ind_l LagPd1_ref_0// LagPd1_ref_liftF_S_alt; intros HL.
apply extF; intros i; destruct (ord_eq_dec i ord0) as [-> | Hi].
move: (fun_ext_rev HL 0%M).
rewrite fct_plus_eq fct_scal_r_eq fct_lc_r_eq.
rewrite sum_zero minus_zero_r scal_one_r// lc_zero_r plus_zero_r; easy.
move: (fun_ext_rev HL (kronR (lower_S Hi))).
rewrite fct_plus_eq fct_scal_r_eq fct_lc_r_eq.
rewrite sum_kron_r// minus_eq_zero scal_zero_r plus_zero_l.
rewrite lc_kron_r_in_r liftF_lower_S; easy.
Qed.
End Poly_LagPd1_ref.
Section Pd1_Facts.
Context {d : nat}.
Lemma LagPd1_ref_S_Monom_d1 :
liftF_S (Monom_dk d 1) = liftF_S (castF (eq_sym (pbinomS_1_r d)) LagPd1_ref).
Proof.
apply extF; intros i; unfold liftF_S; rewrite castF_eq_sym.
move: (lift_S_not_first i) ⇒ Hi0.
assert (Hi1 : cast_ord (pbinomS_1_r d) (lift_S i) ≠ ord0)
by now apply cast_ordS_n0.
rewrite LagPd1_ref_S Monom_d1_S.
apply fun_ext; intros x; do 2 f_equal; easy.
Qed.
[RR9557v1]
Lem 1543, p. 81.
Lemma LagPd1_ref_poly : inclF LagPd1_ref (Pdk d 1).
Proof.
intros i; destruct (ord_eq_dec i ord0) as [-> | Hi]; apply lin_span_ex.
∃ (replaceF (- ones)%G 1 ord0); apply fun_ext; intros x.
rewrite fct_lc_r_eq LagPd1_ref_0// (lc_skipF ord0); unfold minus.
rewrite replaceF_correct_l// scal_one_l// Monom_d1_0 -LagPd1_ref_S_sum.
rewrite skipF_replaceF skipF_opp lc_opp_l skipF_constF lc_constF_l scal_one.
do 2 f_equal; rewrite skipF_first !fct_liftF_S_eq LagPd1_ref_S_Monom_d1.
rewrite liftF_S_castF -!fct_sum_eq; apply fun_ext_rev.
eapply sum_castF_compat; easy.
pose (ipk := cast_ord (eq_sym (pbinom_1_r d)) (lower_S Hi)).
∃ (insertF (kronR ipk) 0%M ord0).
rewrite (lc_skipF ord0) insertF_correct_l// scal_zero_l plus_zero_l.
rewrite skipF_insertF !skipF_first LagPd1_ref_S_Monom_d1 lc_kron_l_in_r.
rewrite liftF_S_castF LagPd1_ref_S LagPd1_ref_liftF_S_alt.
apply fun_ext; intros x; unfold ipk, castF; f_equal; apply ord_inj; easy.
Qed.
Proof.
intros i; destruct (ord_eq_dec i ord0) as [-> | Hi]; apply lin_span_ex.
∃ (replaceF (- ones)%G 1 ord0); apply fun_ext; intros x.
rewrite fct_lc_r_eq LagPd1_ref_0// (lc_skipF ord0); unfold minus.
rewrite replaceF_correct_l// scal_one_l// Monom_d1_0 -LagPd1_ref_S_sum.
rewrite skipF_replaceF skipF_opp lc_opp_l skipF_constF lc_constF_l scal_one.
do 2 f_equal; rewrite skipF_first !fct_liftF_S_eq LagPd1_ref_S_Monom_d1.
rewrite liftF_S_castF -!fct_sum_eq; apply fun_ext_rev.
eapply sum_castF_compat; easy.
pose (ipk := cast_ord (eq_sym (pbinom_1_r d)) (lower_S Hi)).
∃ (insertF (kronR ipk) 0%M ord0).
rewrite (lc_skipF ord0) insertF_correct_l// scal_zero_l plus_zero_l.
rewrite skipF_insertF !skipF_first LagPd1_ref_S_Monom_d1 lc_kron_l_in_r.
rewrite liftF_S_castF LagPd1_ref_S LagPd1_ref_liftF_S_alt.
apply fun_ext; intros x; unfold ipk, castF; f_equal; apply ord_inj; easy.
Qed.
[RR9557v1]
Lem 1543, p. 81.
Lemma LagPd1_ref_basis : basis (Pdk d 1) LagPd1_ref.
Proof.
apply lin_indep_basis; [..| apply LagPd1_ref_lin_indep].
eapply has_dim_ext; [| apply Pdk_has_dim]; rewrite pbinom_1_r; easy.
apply LagPd1_ref_poly.
Qed.
Lemma Pd1_has_dim : has_dim (Pdk d 1) d.+1.
Proof. apply (Dim _ _ _ LagPd1_ref_basis). Qed.
End Pd1_Facts.
Proof.
apply lin_indep_basis; [..| apply LagPd1_ref_lin_indep].
eapply has_dim_ext; [| apply Pdk_has_dim]; rewrite pbinom_1_r; easy.
apply LagPd1_ref_poly.
Qed.
Lemma Pd1_has_dim : has_dim (Pdk d 1) d.+1.
Proof. apply (Dim _ _ _ LagPd1_ref_basis). Qed.
End Pd1_Facts.