DeriveF : ça avance...

FEM/P_approx_k.v

@@ -1070,9 +1070,6 @@ Lemma DeriveF_ind_r :
 Proof. intros; apply comp_n_ind_r. Qed.
 
 
-(* WIP *)
-(* manque hypothèses is_Poly *)
-
 (* f1 does not depend upon (x i) therefore is a constant when deriving *)
 Lemma Derive_multii_scal_fun :  forall {n} (i:'I_n) j f1 f2,
     (forall x y, f1 x = f1 (replaceF x y i)) ->
@@ -1087,42 +1084,79 @@ now rewrite Derive_n_scal_l.
 Qed.
 
 
+Definition narrow_ord_max := fun {n:nat} (f:'R^n.+1 -> R) (x:'R^n) => 
+   f (castF (sym_eq (addn1_sym n)) (concatF x (singleF 0))).
+
+Lemma narrow_ord_max_correct : forall {n:nat} f,
+   (forall (x:'R^n.+1) y, f x = f (replaceF x y ord_max)) ->
+   (forall x:'R^n.+1, f x = narrow_ord_max f (widenF_S x)).
+Proof.
+intros n f H x; rewrite (H x 0).
+unfold narrow_ord_max; f_equal.
+apply extF; intros i; unfold replaceF.
+case (ord_eq_dec _ _); intros Hi.
+subst; unfold castF; rewrite concatF_correct_r; easy.
+unfold castF; rewrite concatF_correct_l; simpl; try easy.
+destruct i as (j,Hj); simpl.
+apply ord_neq_compat in Hi; simpl in Hi.
+assert (j < n.+1)%coq_nat; [ now apply /ltP | now lia].
+intros H1; unfold widenF_S; f_equal; apply ord_inj; now simpl.
+Qed.
+
+
+Lemma DeriveF_part_scal_fun : forall {n} i (alpha:'nat^n.+1) (Hi: i<>ord_max) (g1:R->R) (g2: 'R^n.+1 -> R),
+  (forall (x:'R^n.+1) y, g2 x = g2 (replaceF x y ord_max)) ->
+  DeriveF_part alpha i (fun x:'R^n.+1 => g1 (x ord_max) * g2 x)
+     = (fun x:'R^n.+1 => g1 (x ord_max) 
+          * DeriveF_part (widenF_S alpha) (narrow_S Hi) (narrow_ord_max g2) (widenF_S x)).
+Proof.
+Admitted.
+
+
+
+
+(*
 Lemma DeriveF_scal_fun : forall {n} i (alpha:'nat^n.+1) (Hi: i<>ord_max) (g1:R->R) (g2: 'R^n -> R),
   DeriveF_part alpha i (fun x:'R^n.+1 => g1 (x ord_max) * g2 (widenF_S x))
      = (fun x:'R^n.+1 => g1 (x ord_max) * DeriveF_part (widenF_S alpha) (narrow_S Hi) g2 (widenF_S x)).
 Proof.
 intros n (i,Hi); induction i.
-intros alpha Hi0 g1 g2.
-apply fun_ext; intros x.
-rewrite DeriveF_part_0.
-rewrite DeriveF_part_0; try easy.
+intros alpha Hi0 g1 g2; apply fun_ext; intros x.
+rewrite DeriveF_part_0; try rewrite DeriveF_part_0; try easy.
 apply ord_inj; simpl; easy.
 apply ord_inj; simpl; easy.
 intros alpha Hi0 g1 g2.
 assert (Hi' : (i < n.+1)%nat).
-admit.
+apply /ltP; apply Arith_prebase.lt_S_n.
+now apply /ltP.
 replace (@Ordinal (n.+2) (i.+1) Hi) with (lift_S (Ordinal Hi')) at 1.
 2: apply ord_inj; easy.
-rewrite DeriveF_part_ind_r.
-rewrite comp_correct.
-unfold Derive_alp.
-rewrite Derive_multii_scal_fun.
-assert (Hi'' : (i < n.+2)%nat).
+rewrite DeriveF_part_ind_r comp_correct.
+unfold Derive_alp; rewrite Derive_multii_scal_fun.
 admit.
+intros x y.
+rewrite replaceF_correct_r; try easy.
+apply ord_neq, sym_not_eq; simpl.
+apply Nat.lt_neq.
+
+assert (Hi'' : (i < n.+2)%nat).
+apply ltn_trans with (1:=Hi'); apply ltnSn.
 assert (Hi1 :  Ordinal (n:=n.+2) (m:=i)  Hi'' <> ord_max).
-admit.
+apply ord_neq; simpl.
+apply Nat.lt_neq; apply /ltP; easy.
 replace ((widen_S (Ordinal (n:=n.+1) (m:=i) Hi'))) with (Ordinal (n:=n.+2) (m:=i) Hi'').
-assert (Hi2 : (i < n)%nat ).
-admit.
-specialize (IHi Hi'' alpha Hi1 g1 (Derive_multii
-     (Ordinal Hi2)
-     (alpha (Ordinal Hi')) g2)).
+specialize (IHi Hi'' alpha Hi1 g1 (fun t => Derive_multii
+     (Ordinal Hi')
+     (alpha (Ordinal Hi')) (fun x0 : 'R^n.+1 => g2 (widenF_S x0)) 
+     (castF (sym_eq (addn1_sym n)) (concatF t (singleF 0))))).
 eapply trans_eq.
 2: eapply eq_trans.
 2: apply IHi.
 f_equal; try easy.
 apply fun_ext; intros x; f_equal.
-unfold Derive_multii; f_equal.
+
+admit.
+(*
 apply fun_ext; intros y; f_equal.
 unfold widenF_S; apply extF; intros j; unfold replaceF.
 case (ord_eq_dec _ _); intros T1; case (ord_eq_dec _ _); intros T2; try easy.
@@ -1134,7 +1168,7 @@ exfalso; apply T1.
 apply ord_inj; simpl.
 rewrite T2; easy.
 unfold widenF_S; f_equal.
-apply ord_inj; simpl; easy.
+apply ord_inj; simpl; easy.*)
 apply fun_ext; intros x; f_equal.
 replace (narrow_S Hi0) with (lift_S (Ordinal Hi2)).
 2: apply ord_inj; simpl; easy.
@@ -1225,9 +1259,27 @@ intros alpha g1 g2.
 rewrite comp_n_ind_r comp_correct.
 
 rewrite {2}DeriveF_ind_r.
-*)
+*)*)
 
 
+Lemma DeriveF_ind_r_scal_fun : forall {n} (alpha : 'nat^n.+1) f (g1:R->R) (g2: 'R^n.+1 -> R),
+   (forall (x:'R^n.+1), Derive_alp alpha ord_max f x = g1 (x ord_max) * g2 x) ->
+   (forall (x:'R^n.+1) y, g2 x = g2 (replaceF x y ord_max)) ->
+   DeriveF alpha f = fun x => g1 (x ord_max) * DeriveF (widenF_S alpha) (narrow_ord_max g2) (widenF_S x).
+Proof.
+intros n alpha f g1 g2 H1 H2.
+rewrite DeriveF_correct.
+rewrite -lift_S_max.
+rewrite DeriveF_part_ind_r comp_correct.
+apply fun_ext_equiv in H1; rewrite H1.
+rewrite DeriveF_part_scal_fun; try easy.
+apply ord_neq; simpl; easy.
+intros H; apply fun_ext; intros x; f_equal.
+rewrite DeriveF_correct; f_equal.
+apply ord_inj; easy.
+Qed.
+
+(*
 Lemma DeriveF_ind_r_prout : forall {n} (alpha : 'nat^n.+1) f (g1:R->R) (g2: 'R^n -> R),
    (forall (x:'R^n.+1), Derive_alp alpha ord_max f x = g1 (x ord_max) * g2 (widenF_S x)) ->
   DeriveF alpha f = fun x => g1 (x ord_max) * DeriveF (widenF_S alpha)  g2 (widenF_S x).
@@ -1251,7 +1303,7 @@ rewrite DeriveF_part_full.
 easy.
 apply ord_inj; simpl; easy.*)
 Admitted.
-
+*)
 
 
 Definition is_Poly {n} (f: 'R^n -> R) := exists k, P_approx_k_d n k f.
@@ -1479,8 +1531,7 @@ Lemma DeriveF_f_mono : forall {n} (alpha B :'nat^n), exists C,
   DeriveF alpha (fun x => f_mono x B) 
      = (fun x => C* f_mono x (fun i => (B i- alpha i)%coq_nat))
    /\ (C = 0 <-> brEF lt B alpha).
-(* (exists i, (B i < alpha i)%coq_nat)).*)
-(*not (forall i, alpha i <= B i)%coq_nat).*)
+             (* (exists i, (B i < alpha i)%coq_nat)).*)
 Proof.
 intros n; induction n.
 intros alpha B; exists 1; split.
@@ -1494,27 +1545,54 @@ exfalso; apply I_0_is_empty; apply (inhabits i).
 (* *)
 intros alpha B.
 destruct (Derive_multii_f_mono B ord_max (alpha ord_max)) as
-  (C1, (Y1,Z1)).
+  (C1, (Y1,Z1)); fold (Derive_alp alpha ord_max) in Y1.
 destruct (IHn (widenF_S alpha) (widenF_S B)) as (C2,(Y2,Z2)).
 exists (C1*C2); split.
-
-
-rewrite (DeriveF_ind_r_prout alpha (f_mono^~ B) (fun t => C1 * t^(B ord_max - alpha ord_max)) 
-   ((fun t => f_mono t (widenF_S B)))).
-
-
+rewrite ->DeriveF_ind_r_scal_fun with 
+  (g1:= fun t => C1 * t^(B ord_max - alpha ord_max))
+  (g2:= fun t => f_mono (widenF_S t) (widenF_S B)).
+(* . *)
 apply fun_ext; intros x.
+rewrite 2!Rmult_assoc; f_equal.
+rewrite ->DeriveF_extf with (f2:=f_mono^~ (widenF_S B)).
 rewrite Y2.
-
-admit.
-admit.
-
-
-
-admit.
-
-
-Admitted.
+rewrite Rmult_comm Rmult_assoc; f_equal.
+unfold f_mono; rewrite prod_R_ind_r.
+unfold plus; simpl; f_equal.
+intros t; unfold narrow_ord_max, f_mono; f_equal; f_equal.
+apply extF; intros i; unfold widenF_S, castF.
+rewrite concatF_correct_l; simpl; try easy.
+apply /ltP; destruct i; easy.
+intros H0; f_equal; apply ord_inj; now simpl.
+(* . *)
+intros x; rewrite Y1.
+rewrite Rmult_assoc; f_equal.
+unfold f_mono; rewrite prod_R_ind_r.
+unfold plus; simpl; rewrite Rmult_comm; f_equal.
+unfold powF, map2F; rewrite replaceF_correct_l; try easy.
+f_equal; apply extF; intros i.
+unfold widenF_S, powF, map2F; rewrite replaceF_correct_r; try easy.
+apply widen_S_not_last.
+(* . *)
+intros x y; f_equal; apply extF; intros i.
+unfold widenF_S; f_equal.
+rewrite replaceF_correct_r; try easy.
+apply widen_S_not_last.
+(* *)
+split; intros H.
+case (Rmult_integral C1 C2 H); intros H'.
+exists ord_max; apply Z1; easy.
+destruct ((proj1 Z2) H') as (j,Hj).
+exists (widen_S j); easy.
+destruct H as (j,Hj).
+case (ord_eq_dec j ord_max); intros H'.
+replace C1 with 0; try ring.
+apply sym_eq, Z1; subst; easy.
+replace C2 with 0; try ring.
+apply sym_eq, Z2.
+exists (narrow_S H').
+unfold widenF_S; rewrite widen_narrow_S; easy.
+Qed.
 
 
 Lemma Derive_alp_scal :