Skip to content
Snippets Groups Projects
Commit 81687d55 authored by Mouhcine's avatar Mouhcine
Browse files

Prove vtx_in_convex_envelop lemma.

move the comment to FE.v
parent ef72d37e
No related branches found
No related tags found
No related merge requests found
......@@ -52,72 +52,17 @@ intros i.
replace (vtx i) with
(comb_lin (kronecker i) vtx).
apply Cvx.
(*; unfold elt_geom.
exists (kronecker i).
repeat split*)
replace (vtx i) with (\big[plus/zero]_(j < nvtx) (scal (kronecker i j) (vtx j))).
(*
apply Cvx.
intros j; apply kronecker_bound.*)
(*
apply kronecker_sum_r; easy.
(* *)
induction nvtx; try easy.
rewrite sum_pn_Sn.
case (lt_dec i n); intros Hn.
(*case1*)
rewrite <- IHn; try easy.
replace (kronecker i n) with (@zero R_Ring).
rewrite (scal_zero_l).
rewrite plus_zero_r; easy.
unfold kronecker.
case (eq_nat_dec i n); try easy.
intros; lia.
(*case2*)
unfold kronecker at 2.
case (eq_nat_dec i n); try lia.
intros H1.
replace (sum_pn _ _) with (@zero E).
replace 1 with (@one R_Ring) by easy.
rewrite scal_one.
rewrite H1.
rewrite plus_zero_l; easy.
rewrite sum_pn_zero; try easy.
intros m Hm.
unfold kronecker.
case (eq_nat_dec i m); try lia.
intros; replace 0 with (@zero R_Ring) by easy.
apply (scal_zero_l (vtx m)).
intros j; apply kronecker_bound.
apply comb_lin_kronecker_r.
apply comb_lin_kronecker_in_r.
Qed.
*)
Admitted.
(* TODO: hypothesis on vertices : geometrical form not degenerate *)
(* TODO: define basic geometric shapes:
(simplices) Seg Tria, Tetra,
(others) Quad, Hexa, Prism?...
Define the geometric transformation T_geom (from the reference mesh to the current mesh)
for all previous geometric shapes, and its Jacobian matrix and Jacobian determinant.
For the simplex in dim E = d, T_geom is affine : x^ -> x = a0 + J_geom x^
where J_geom = (a1-a0 a2-a0 ... ad-a0) is the Jacobian matrix of T_geom, made of the
column vectors ai-a0, where (a0,a1...ad) are the vertices of the current mesh.
The vertices of the reference mesh are a0^ = (0,0...0), a1^ = (1,0...0),
a2^ = (0,1,0...0),..., ad^ = (0,...0, 1).
In each case, prove that J_geom is indeed the Jacobian matrix of T_geom.
Prove that T_geom is invertible, ie its Jacobian determinant is nonzero.
Then, in the simple cases, T_geom{-1} : x -> x^ = J_geom{-1} (x-a0).
(others) Quad, Hexa, Prism?...*)
Maybe prove correction lemmas of the form:
forall x^, K_geom (T_geom x^) <-> K_geom^ x^, ie image T_geom K_geom^ = K_geom.
forall x, K_geom x <-> K_geom^ (T_geom{-1} x), ie image T_geom{-1} K_geom = K_geom^. *)
End Geometry.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment