Add LagP1_is_affine and LagQ1_is_LagP1 lemmas.

FEM/poly_Lagrange.v

@@ -105,7 +105,6 @@ contradict H.
 admit.
 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), 
   convex_envelop d.+1 vtxP1 x -> 0 <= LagP1 i x.
 Proof.
@@ -119,6 +118,36 @@ intros.
 unfold comb_lin.
 Admitted.
 
+Lemma LagP1_is_affine: forall i,
+  is_affine (LagP1 i).
+Proof.
+intros i.
+pose (L := fun x => minus (LagP1 i x) (LagP1 i zero)).
+apply is_affine_ext with 
+  (fun x => plus (L x) (LagP1 i zero)).
+intros x.
+unfold L.
+admit. (* easy*)
+apply (Is_affine L).
+unfold L, LagP1.
+case (eq_nat_dec i 0); intros Hi.
+rewrite bigop_op_idx; try easy.
+apply is_linear_mapping_ext with 
+    (fun x : 'R^d => \big[+%R/0]_(i < d) x i).
+intros x.
+admit. (* easy *)
+apply is_linear_mapping_ext with 
+    (fun x : 'R^d => comb_lin (fun => 1) x).
+admit. (* easy *)
+apply component_sum_is_linear_mapping.
+(* *)
+apply is_linear_mapping_ext with 
+    (fun x : 'R^d => 
+        (x (Ordinal (n:=d) (m:=i - 1) (lt_minus_1 i Hi)))).
+admit. (* easy *)
+apply component_is_linear_mapping.
+Admitted.
+
 End Poly_Lagrange_Simplex.
 
 
@@ -174,3 +203,16 @@ unfold comb_lin.
 Admitted.
 
 End Poly_Lagrange_Quad.
+
+Section LagPQ.
+
+(* TODO Faut le phi *)
+Lemma LagQ1_is_LagP1 : forall (i : 'I_2) x,
+  LagQ1 1 i x = LagP1 1 i x.
+Proof.
+intros i x.
+unfold LagQ1.
+Admitted.
+
+
+End LagPQ.
\ No newline at end of file