work on LagPQ_is_non_neg lemma

FEM/finite_element.v

@@ -462,23 +462,30 @@ apply LagQ1_kron.
 Qed.
 
 (* TODO: Not really! we should add some hypothesis on x_i *)
+(* ajouter une hyp qu'on est dans l'element de ref *)
 Lemma LagPQ_is_non_neg : forall (i : 'I_nnvtx) (x : 'R^dd), 
-  0 <= LagPQ i x.
+  K_geom_ref x -> 0 <= LagPQ i x.
 Proof.
-intros i x; unfold LagPQ.
+intros i x Hx; unfold LagPQ.
 case (nvtx_dec FE_ref); intros H.
 apply LagP1_is_non_neg.
-apply LagQ1_is_non_neg; easy.
-Qed.
-
+unfold K_geom_ref, K_geom in Hx.
+unfold dd.
+admit.
+admit.
+(*apply LagQ1_is_non_neg; easy.
+Qed.*)
+Admitted.
+ 
 (* TODO verify if this lemma is true, we apply it to T_geom_is_bij_id *)
 Lemma LagPQ_sum_1 : forall x,
   comb_lin (fun i : 'I_nnvtx => LagPQ i x)(fun _ => 1) = 1.
 Proof.
+(*
 intros x.
 unfold LagPQ.
 case (nvtx_dec FE_ref); intros H.
-admit.
+admit.*)
 (*apply LagP1_sum_1.
 apply LagQ1_sum_1.*)
 
@@ -767,6 +774,7 @@ unfold range; intros x_cur H.
 apply K_geom_ref_correct; easy.
 (* *)
 intros i; apply LagPQ_is_non_neg.
+(*
 apply LagPQ_sum_1.
 (* *)
 unfold identity; intros x_cur H; symmetry.
@@ -774,7 +782,8 @@ apply T_geom_comp; easy.
 (* *)
 unfold identity; intros x_ref H; symmetry.
 apply T_geom_inv_comp; easy.
-Qed.
+Qed.*)
+Admitted.
 
 Lemma theta_cur_correct : forall i : 'I_(ndof FE_cur), 
   theta_ref i = cur_to_ref (theta_cur i).

FEM/poly_Lagrange.v

@@ -107,9 +107,9 @@ Admitted.
 
 (* TODO: Faut des hypothèses de plus sur x_i > 0 *)
 Lemma LagP1_is_non_neg : forall (i : 'I_d.+1) (x : 'R^d), 
-  0 <= LagP1 i x.
+  convex_envelop d.+1 vtxP1 x -> 0 <= LagP1 i x.
 Proof.
-intros i x; unfold LagP1.
+intros i x Hx; unfold LagP1.
 Admitted.
 
 Lemma LagP1_sum_1 : forall x,
@@ -160,9 +160,9 @@ Proof.
 Admitted.
 
 Lemma LagQ1_is_non_neg : forall (i : 'I_(2 ^ d)) (x : 'R^d), 
-  0 <= LagQ1 i x.
+  convex_envelop (2^d) vtxQ1 x -> 0 <= LagQ1 i x.
 Proof.
-intros i x; unfold LagQ1.
+intros i x Hx; unfold LagQ1.
 
 Admitted.