Library FEM.FE_simplex
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.
[Ern]
Alexandre Ern, Éléments finis, Aide-mémoire, Dunod/L'Usine Nouvelle, 2005,
https://www.dunod.com/sciences-techniques/aide-memoire-elements-finis.
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 geom_simplex geom_transf_affine poly_Pdk FE.
Local Open Scope R_scope.
Section Transf.
Definition transf {d:nat} (phi:'R^d → 'R^d) : FRd d → FRd d :=
fun f x ⇒ f (phi x).
Context {d:nat}.
Context {phi:'R^d → 'R^d}.
Hypothesis Hphi_bij : bijective phi.
Definition transf_inv : FRd d → FRd d :=
fun f x ⇒ f (f_inv Hphi_bij x).
Lemma transf_inv_can_r : ∀ f, transf_inv (transf phi f) = f.
Proof.
intros f; unfold transf_inv, transf; apply fun_ext; intros x.
now rewrite f_inv_can_r.
Qed.
Lemma transf_inv_can_l : ∀ f, transf phi (transf_inv f) = f.
Proof.
intros f; unfold transf_inv, transf; apply fun_ext; intros x.
now rewrite f_inv_can_l.
Qed.
Lemma transf_bij : bijective (transf phi).
Proof.
apply (Bijective transf_inv_can_r transf_inv_can_l).
Qed.
Lemma transf_lm : lin_map (transf phi).
split; unfold transf.
intros f g; apply fun_ext; intros x; unfold plus; simpl; unfold fct_plus; simpl; easy.
intros f j; apply fun_ext; intros x; unfold scal; simpl; unfold fct_scal; simpl; easy.
Qed.
End Transf.
Section FE_out.
Variable FE_in : FE.
Context {phi:'R^(d FE_in) → 'R^(d FE_in)}.
Hypothesis Hphi : bijective phi.
Definition P_out : FRd (d FE_in) → Prop :=
preimage (transf phi) (P_approx FE_in).
Lemma P_out_has_dim : has_dim P_out (ndof FE_in).
Proof.
assert (H1 : has_dim (P_approx FE_in) (ndof FE_in)) by apply FE_in.
inversion H1 as (B,HB).
apply (Dim _ _ (mapF (transf_inv Hphi) B)); unfold P_out.
rewrite (lm_basis_compat_equiv (transf phi)).
apply basis_ext2 with (3:= HB).
rewrite image_of_preimage; apply sym_eq, inter_left.
intros f Hf; rewrite image_eq.
∃ (transf_inv Hphi f); split; try easy.
now rewrite transf_inv_can_l.
apply extF; intros i; rewrite mapF_correct.
now rewrite transf_inv_can_l.
apply transf_lm.
apply cms_preimage; try apply transf_lm.
eapply has_dim_cms; apply FE_in.
intros f g Hf Hg H2.
rewrite -(transf_inv_can_r Hphi f) -(transf_inv_can_r Hphi g).
now rewrite H2.
intros i; rewrite mapF_correct.
rewrite (preimage_eq (transf_inv_can_r Hphi) (transf_inv_can_l Hphi)).
apply Im; now apply basis_inclF.
Qed.
Definition Sigma_out : '(FRd (d FE_in) → R)^(ndof FE_in) :=
fun i p ⇒ Sigma FE_in i (transf phi p).
Lemma Sigma_out_lm : ∀ i : 'I_(ndof FE_in),
lin_map (Sigma_out i).
Proof.
intros i; split.
intros f g; unfold Sigma_out.
rewrite (lm_plus transf_lm).
now rewrite (lm_plus (Sigma_lm FE_in i)).
intros f l; unfold Sigma_out.
rewrite (lm_scal transf_lm).
now rewrite (lm_scal (Sigma_lm FE_in i)).
Qed.
Lemma unisolvence_inj_out : KerS0 P_out (gather Sigma_out).
Proof.
intros f Hf1 Hf2.
apply (bij_inj (transf_bij Hphi)).
apply trans_eq with 0%M; try easy.
apply (unisolvence_inj FE_in); try easy.
Qed.
Definition FE_out :=
mk_FE (d FE_in) (ndof FE_in) (d_pos FE_in) (ndof_pos FE_in) (shape FE_in)
(mapF phi (vtx FE_in)) P_out P_out_has_dim Sigma_out Sigma_out_lm
unisolvence_inj_out.
Lemma FE_out_K_geom : K_geom FE_out = convex_envelop (mapF phi (vtx FE_in)).
Proof.
easy.
Qed.
Lemma transf_bijS :
bijS P_out (P_approx FE_in) (transf phi).
Proof.
apply (BijS (transf_inv Hphi)); repeat split.
intros g; unfold RgS, P_out.
rewrite image_of_preimage; unfold inter; easy.
intros g; unfold RgS, P_out; intros Hg.
rewrite (preimage_eq (transf_inv_can_r Hphi) (transf_inv_can_l Hphi)); easy.
intros g _; apply transf_inv_can_r.
intros g _; apply transf_inv_can_l.
Qed.
Lemma shape_fun_transf : ∀ i:'I_(ndof FE_in),
shape_fun FE_out i = transf_inv Hphi (shape_fun FE_in i).
Proof.
intros i; apply (bij_inj (transf_bij Hphi)).
rewrite transf_inv_can_l.
rewrite (is_local_shape_fun_inj FE_in (shape_fun FE_in)
(fun i ⇒ transf phi (shape_fun FE_out i))); try easy.
apply shape_fun_correct.
generalize (shape_fun_correct FE_out); easy.
Qed.
[Ern]
Prop 4.5, Eq (4.13), pp. 79-80.
Lemma local_interp_transf : ∀ v,
local_interp FE_in (transf phi v) =
transf phi (local_interp FE_out v).
Proof.
intros v; unfold local_interp.
simpl (Sigma FE_out); unfold Sigma_out.
rewrite (f_lc_compat_lm transf_lm); f_equal.
apply extF; intros i; rewrite mapF_correct.
rewrite shape_fun_transf.
rewrite transf_inv_can_l; easy.
Qed.
End FE_out.
Section FE_cur.
Lemma FE_out_ext : ∀ FE_in phi1 phi2 (H1: bijective phi1) (H2: bijective phi2),
phi1 = phi2 → FE_out FE_in H1 = FE_out FE_in H2.
Proof.
intros ; subst.
f_equal; apply proof_irrelevance.
Qed.
Variable FE_in : FE.
Variable vtx_out : '('R^(d FE_in))^((d FE_in).+1).
Hypothesis Simplex_in : shape FE_in = Simplex.
Let vtx_in := castF (nvtx_Simplex _ Simplex_in) (vtx FE_in).
Hypothesis aff_ind_in : affine_independent vtx_in.
Hypothesis aff_ind_out : affine_independent vtx_out.
Let phi := (T_geom vtx_out) \o (T_geom_inv aff_ind_in).
Lemma Hphi_cur : bijective phi.
Proof.
unfold phi; apply bij_comp.
now apply T_geom_bij.
apply f_inv_bij.
Qed.
Definition FE_cur := FE_out FE_in Hphi_cur.
Lemma FE_cur_vtx : castF (nvtx_Simplex _ Simplex_in) (vtx FE_cur) = vtx_out.
Proof.
apply extF; intros i; unfold castF.
simpl; rewrite mapF_correct.
apply trans_eq with (phi (vtx_in i)); try easy.
unfold phi, ssrfun.comp.
rewrite T_geom_inv_transports_vtx.
apply T_geom_transports_vtx.
Qed.
Lemma FE_cur_K_geom :
K_geom FE_cur = convex_envelop vtx_out.
Proof.
unfold K_geom; apply convex_envelop_castF with (nvtx_Simplex _ Simplex_in).
rewrite FE_cur_vtx; easy.
Qed.
End FE_cur.
Section FE_ref_to_cur.
Variable FE_in : FE.
Variable vtx_out : '('R^(d FE_in))^((d FE_in).+1).
Hypothesis Simplex_in : shape FE_in = Simplex.
Let vtx_in := castF (nvtx_Simplex _ Simplex_in) (vtx FE_in).
Hypothesis FE_in_is_ref : vtx_in = @vtx_simplex_ref (d FE_in).
Hypothesis aff_ind_out : affine_independent vtx_out.
Definition FE_ref_to_cur := FE_out FE_in (T_geom_bij aff_ind_out).
Lemma FE_ref_to_cur_K_geom :
K_geom FE_ref_to_cur = convex_envelop vtx_out.
Proof.
unfold K_geom; apply convex_envelop_castF with (nvtx_Simplex _ Simplex_in).
simpl; rewrite -mapF_castF; fold vtx_in; rewrite FE_in_is_ref.
apply extF; intros i; rewrite mapF_correct.
rewrite T_geom_transports_vtx; easy.
Qed.
Lemma aff_ind_in : affine_independent vtx_in.
Proof.
rewrite FE_in_is_ref.
apply vtx_simplex_ref_affine_independent.
Qed.
Lemma phi_ref_to_cur_is_cur :
T_geom vtx_out = T_geom vtx_out \o T_geom_inv aff_ind_in.
Proof.
apply fun_ext; intros x; unfold ssrfun.comp.
replace (T_geom_inv aff_ind_in x) with x; try easy.
apply (bij_inj (T_geom_bij aff_ind_in)); rewrite -T_geom_inv_correct_r.
rewrite FE_in_is_ref.
apply T_geom_ref_id.
Qed.
Lemma FE_ref_to_cur_is_cur_to_cur :
FE_ref_to_cur = FE_cur FE_in vtx_out Simplex_in aff_ind_in aff_ind_out.
Proof.
apply FE_out_ext.
apply phi_ref_to_cur_is_cur.
Qed.
End FE_ref_to_cur.
local_interp FE_in (transf phi v) =
transf phi (local_interp FE_out v).
Proof.
intros v; unfold local_interp.
simpl (Sigma FE_out); unfold Sigma_out.
rewrite (f_lc_compat_lm transf_lm); f_equal.
apply extF; intros i; rewrite mapF_correct.
rewrite shape_fun_transf.
rewrite transf_inv_can_l; easy.
Qed.
End FE_out.
Section FE_cur.
Lemma FE_out_ext : ∀ FE_in phi1 phi2 (H1: bijective phi1) (H2: bijective phi2),
phi1 = phi2 → FE_out FE_in H1 = FE_out FE_in H2.
Proof.
intros ; subst.
f_equal; apply proof_irrelevance.
Qed.
Variable FE_in : FE.
Variable vtx_out : '('R^(d FE_in))^((d FE_in).+1).
Hypothesis Simplex_in : shape FE_in = Simplex.
Let vtx_in := castF (nvtx_Simplex _ Simplex_in) (vtx FE_in).
Hypothesis aff_ind_in : affine_independent vtx_in.
Hypothesis aff_ind_out : affine_independent vtx_out.
Let phi := (T_geom vtx_out) \o (T_geom_inv aff_ind_in).
Lemma Hphi_cur : bijective phi.
Proof.
unfold phi; apply bij_comp.
now apply T_geom_bij.
apply f_inv_bij.
Qed.
Definition FE_cur := FE_out FE_in Hphi_cur.
Lemma FE_cur_vtx : castF (nvtx_Simplex _ Simplex_in) (vtx FE_cur) = vtx_out.
Proof.
apply extF; intros i; unfold castF.
simpl; rewrite mapF_correct.
apply trans_eq with (phi (vtx_in i)); try easy.
unfold phi, ssrfun.comp.
rewrite T_geom_inv_transports_vtx.
apply T_geom_transports_vtx.
Qed.
Lemma FE_cur_K_geom :
K_geom FE_cur = convex_envelop vtx_out.
Proof.
unfold K_geom; apply convex_envelop_castF with (nvtx_Simplex _ Simplex_in).
rewrite FE_cur_vtx; easy.
Qed.
End FE_cur.
Section FE_ref_to_cur.
Variable FE_in : FE.
Variable vtx_out : '('R^(d FE_in))^((d FE_in).+1).
Hypothesis Simplex_in : shape FE_in = Simplex.
Let vtx_in := castF (nvtx_Simplex _ Simplex_in) (vtx FE_in).
Hypothesis FE_in_is_ref : vtx_in = @vtx_simplex_ref (d FE_in).
Hypothesis aff_ind_out : affine_independent vtx_out.
Definition FE_ref_to_cur := FE_out FE_in (T_geom_bij aff_ind_out).
Lemma FE_ref_to_cur_K_geom :
K_geom FE_ref_to_cur = convex_envelop vtx_out.
Proof.
unfold K_geom; apply convex_envelop_castF with (nvtx_Simplex _ Simplex_in).
simpl; rewrite -mapF_castF; fold vtx_in; rewrite FE_in_is_ref.
apply extF; intros i; rewrite mapF_correct.
rewrite T_geom_transports_vtx; easy.
Qed.
Lemma aff_ind_in : affine_independent vtx_in.
Proof.
rewrite FE_in_is_ref.
apply vtx_simplex_ref_affine_independent.
Qed.
Lemma phi_ref_to_cur_is_cur :
T_geom vtx_out = T_geom vtx_out \o T_geom_inv aff_ind_in.
Proof.
apply fun_ext; intros x; unfold ssrfun.comp.
replace (T_geom_inv aff_ind_in x) with x; try easy.
apply (bij_inj (T_geom_bij aff_ind_in)); rewrite -T_geom_inv_correct_r.
rewrite FE_in_is_ref.
apply T_geom_ref_id.
Qed.
Lemma FE_ref_to_cur_is_cur_to_cur :
FE_ref_to_cur = FE_cur FE_in vtx_out Simplex_in aff_ind_in aff_ind_out.
Proof.
apply FE_out_ext.
apply phi_ref_to_cur_is_cur.
Qed.
End FE_ref_to_cur.