WIP: add prop of LagP1.

FEM/poly_Lagrange.v

@@ -8,7 +8,7 @@ Require Import Rstruct.
 
 From mathcomp Require Import bigop vector ssrfun tuple fintype ssralg.
 From mathcomp Require Import ssrbool eqtype ssrnat.
-From mathcomp Require Import seq path poly matrix all_ssreflect.
+From mathcomp Require Import seq path poly matrix ssreflect.
 
 Add LoadPath "../LM" as LM.
 From LM Require Import linear_map check_sub_structure.
@@ -37,39 +37,65 @@ move => [j Hj] /=.
 (* lia. does not work *)
 Admitted.
 
-(* Why specify _simplex in the name? *)
-Definition LagP1 : '('R^d -> R)^(S d). :=
+(* Drop the suffix _simplex. Is it a problem? *)
+Definition LagP1 : '('R^d -> R)^(S d) :=
   fun j x => match (eq_nat_dec j (@ord0 d)) with
-    | left _ => 1 - \big[+%R/0]_(i < d) (x i)
+    | left _ => 1 - (*comb_lin x (fun _ => 1)*) \big[+%R/0]_(i < d) (x i)
     | right H => x (Ordinal (lt_minus_1 j))
     end.
 
-End Poly_Lagrange_Simplex
+Definition vtxP1 : '('R^d)^(S d) :=
+  fun j i => match (eq_nat_dec j (@ord0 d)) with
+    | left _ => 0
+    | right H => kronecker (Ordinal (lt_minus_1 j)) i
+    end.
 
+Lemma LagP1_kron : forall i j,
+  LagP1 j (vtxP1 i) = kronecker i j.
+Proof.
+intros i j.
+unfold LagP1, vtxP1.
+destruct (eq_nat_dec j (@ord0 d)) as [Hj | Hj];
+  destruct (eq_nat_dec i (@ord0 d)) as [Hi | Hi]; simpl.
+(* *)
+rewrite Hi Hj big1_eq kronecker_is_1; try lra; easy.
+(* *)
+rewrite Hj kronecker_is_0; try easy.
+(*rewrite (bigD1 (i - 1)%nat).*)
+admit.
+(* *)
+rewrite Hi kronecker_is_0; try apply not_eq_sym; easy.
+(* *)
+unfold kronecker; destruct (Nat.eq_dec i j) as [H | H];
+  destruct (Nat.eq_dec (i - 1) (j - 1)) as [H1 | H1]; try easy.
+rewrite H in H1; easy.
+contradict H.
+(*apply <- (N.add_cancel_r (i0 - 1)%N) in H1.*)
+(*rewrite (N.add_sub_eq_r i) in H1.*)
+admit.
+Admitted.
 
-Section Poly_Lagrange_Quad.
+End Poly_Lagrange_Simplex.
 
-(* For quad-like (Q1 in dim d), 
-  LagQ1 i x = \Pi_{j=1}^d (1 - x_j) or x_j  (num = 2^d)
 
-Geometries using Q2 or higher are left aside... *)
+Section Poly_Lagrange_Quad.
 
-Definition LagP1_1d : (i : nat) (x : R) : R := LagP1 1.
-  match (eq_nat_dec i 0) with
-    | left _  => x 
-    | right _ => 1 - x 
-    end.
+(* For simplices (P1 in dim d), with x = (x_i)_{i=1..d}:
+  LagP1 0 x = 1 - \sum_{i=1}^d x_i
+  LagP1 i x = x_(i-1)
 
-(* TODO: change d.-tupleR into 'R^d... *)
+ For quad-like (Q1 in dim d), 
+  LagQ1 i x = \Pi_{j=1}^d (1 - x_j) or x_j  (num = 2^d)
 
-Definition LagQ1 : d.-tuple R -> (S d).-tuple R := 
-  fun x => cons_tuple (\big[*%R/1]_(i < d) (tnth x i))
-(mktuple (fun i => tnth x i)).
+Geometries using P2/Q2 or higher are left aside... *)
 
-Definition LagQ1_aux1 : 2.-tuple R -> 4.-tuple R := 
-  fun x => mktuple (fun i => \big[*%R/1]_(j < 2) Poly_interp_lag i (tnth x j)).
+Variable d : nat.
+
+Definition phi : 'I_(Nat.pow 2 d) -> '('I_2)^d.
+Proof.
+Admitted.
 
-Definition LagQ1_aux2 : d.-tuple R -> (S d).-tuple R := 
-  fun x => mktuple (fun i => \big[*%R/1]_(j < d) Poly_interp_lag i (tnth x j)).
+Definition LagQ1 : '('R^d -> R)^(Nat.pow 2 d) :=
+  fun j x => \big[*%R/1]_(i < d) LagP1 1 (phi j i) (fun _ => x i).
 
-End Poly_Lagrange_basis.
\ No newline at end of file
+End Poly_Lagrange_Quad.