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.

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 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}:
  • 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 xmatch (ord_eq_dec j ord0) with
    | left _ ⇒ 1 - sum x
    | right Hjx (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 xx (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.

[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 xsum 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 xx (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.

[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.

[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.