Library FEM.FE_transf

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

[Ern] Alexandre Ern, Éléments finis, Aide-mémoire, Dunod/L'Usine Nouvelle, 2005, https://www.dunod.com/sciences-techniques/aide-memoire-elements-finis.

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 xf (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 xf (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 pSigma 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 : FE :=
  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 itransf 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_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_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_can_r.
rewrite FE_in_is_ref.
rewrite T_geom_ref_id; easy.
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.