Updates

FEM/finite_element_1.v

@@ -146,7 +146,7 @@ Record FE : Type := mk_FE {
   ndof_pos : (0 < ndof)%nat ;
   nvtx_pos : (0 < nvtx)%nat ;
 
-  vtx : 'I_nvtx -> Rd ; (* vertices of geometrical element *)
+  vtx : 'I_nvtx -> Rd (* -> E R_MS *) ; (* vertices of geometrical element *)
   K_geom : Rd -> Prop (* := convex_envelop nvtx vtx TODO *) ;
                         (* geometrical element *)
 
@@ -388,18 +388,18 @@ Section FE_Reference_Def.
 (** construct the FE_reference *)
 Variable fe_ref : FE. 
 
-Local Definition K_ref := K_geom fe_ref.
+Local Definition K_ref : Rd fe_ref -> Prop := K_geom fe_ref.
 
-(*Local Definition P_ref_new := PolySpace n fe_ref.*)
+(*Local Definition P_approx_ref_new := PolySpace n fe_ref.*)
 
-Local Definition P_ref : F (d fe_ref) -> Prop := P_approx fe_ref.
+Local Definition P_approx_ref : F (d fe_ref) -> Prop := P_approx fe_ref.
 
 Local Definition sigma_ref : 'I_(ndof fe_ref) -> F (d fe_ref) -> R
   := sigma fe_ref.
 
 Local Definition nvtx_ref : nat := nvtx fe_ref.
 
-Local Definition vtx_ref : 'I_(nvtx fe_ref) -> Rd fe_ref:= vtx fe_ref.
+Local Definition vtx_ref : 'I_(nvtx_ref) -> Rd fe_ref := vtx fe_ref.
 
 (* before we had this basis for E generi
 Variable Lag_ref_old : 'I_(nvtx_ref) -> E -> R. (* The poly Lagrange basis *)*)
@@ -407,11 +407,15 @@ Variable Lag_ref_old : 'I_(nvtx_ref) -> E -> R. (* The poly Lagrange basis *)*)
 (* Lagrange basis *)
  (* SB: doute de type de Lag_ref *)
 (* Fonctions de formes géométriques *)
+
+(* Lag_ref' : 'I_(nvtx_ref) ->  F (d fe_ref).?*)
 Variable Lag_ref : 'I_(nvtx_ref) ->  Rd fe_ref (*F (d fe_ref)*) -> R. 
 
 Context {Rmu : NormedModule R_AbsRing}.
 
 (* Why Rmu ? *)
+(* 'I_(nvtx_ref) -> F (d fe_ref) ? *)
+Variable theta_ref' : 'I_(nvtx_ref) -> F (d fe_ref).
 Variable theta_ref : 'I_(nvtx_ref) -> F (d fe_ref) -> Rmu.
 
 Hypothesis H_Lag_ref : forall (i j : 'I_(nvtx_ref)),
@@ -424,9 +428,10 @@ Definition interp_op_local_ref := fun v : F (d fe_ref) =>
   interp_op_local fe_ref v.
 
 (** construct the FE_current *)
-Variable vtx_cur : 'I_(nvtx_ref) -> F (d fe_ref). (*vertices of current geometrical element*)
+(* vtx_cur_old : 'I_(nvtx_ref) -> F (d fe_ref) (* E MS *) ? *)
+Variable vtx_cur : 'I_(nvtx_ref) -> Rd fe_ref. (*vertices of current geometrical element*)
 
-Local Definition ndof_cur := ndof fe_ref.
+Local Definition ndof_cur : nat := ndof fe_ref.
 
 Definition T_geom  (*: F (d fe_ref)-> F (d fe_ref)*) := fun x_ref =>
   \big[plus%R/zero]_(i < nvtx_ref) scal (Lag_ref i x_ref) (vtx_cur i).
@@ -507,7 +512,7 @@ Definition cur_to_ref : fct_ModuleSpace -> F (d fe_ref) (* E *) -> Rmu :=
 Lemma is_linear_mapping_cur_to_ref : is_linear_mapping cur_to_ref.
 Proof. easy. Qed.
 (*
-Definition P_cur := preimage_FD cur_to_ref P_ref is_linear_mapping_cur_to_ref.*)
+Definition P_cur := preimage_FD cur_to_ref P_approx_ref is_linear_mapping_cur_to_ref.*)
 
 Definition sigma_cur : 'I_(ndof fe_ref) -> fct_ModuleSpace -> R := fun i pol => sigma_ref i (cur_to_ref pol).
 
@@ -606,6 +611,7 @@ Variable node_lagrange : 'I_(nb_node_lagrange) -> E. (* nodes of geometrical ele
 
 (* Variable k_lagrange : nat. (* maximum degree of polynomial. *) *)
 
+(* FiniteDim has to be replaced *)
 Variable P_lagrange : @FiniteDim (@fct_ModuleSpace E R_ModuleSpace). (* Should be Rd? *)
 
 Hypothesis H : nb_node_lagrange = dim P_lagrange.
@@ -614,7 +620,7 @@ Hypothesis Hcard : (dimE < nvtx)%nat.*)
 
 Definition ndof_lagrange := nb_node_lagrange.
 
-Definition sigma_lagrange := fun i (p : E -> R) => p (node_lagrange i).
+Definition sigma_lagrange : 'I_nb_node_lagrange -> (E -> R) -> R := fun i (p : E -> R) => p (node_lagrange i).
 
 (* TODO: move elsewhere... *)
 Lemma is_linear_mapping_pt_value : forall a, 
@@ -634,7 +640,7 @@ apply is_linear_mapping_pt_value.
 Qed.
 
 (* TODO: apply lemma is_unisolvant_equiv and prove it's lin indep *)
-Lemma FE_lagrange_is_unisolvant : is_unisolvant nb_node_lagrange ndof_lagrange sigma_lagrange ndof_lagrange.
+Lemma FE_lagrange_is_unisolvant : is_unisolvant P_lagrange sigma_lagrange ndof_lagrange.
 Proof.
 apply is_unisolvant_equiv.
 intros p; split.