Library FEM.poly_Pdk

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is lin_indep software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Description

This file is about defining the vector space of polynomials from R^d to R, with degree <= k, called Pdk, by defining its basis Monom_dk. Special interest for Pd0 and P1k: another basis is given.
For simplices (Pk in dim d), with x = (x_i)_{i=1..d}:
  • Pdk = lin_span (x_1^alpha_1 * x_2^alpha_2 * ... * x_d^alpha_d) such that 0 <= alpha_1, ..., alpha_d <= k /\ sum \alpha_i <= k,
  • p = lin_comb L x_i^(alpha_i) \in Pdk.
For simplices (P1 in dim d), with x = (x_i)_{i=1..d}:
  • Pd1 = lin_span (1, x_1, ..., x_d) = lin_span LagPd1_ref,
  • p = lin_comb L x \in Pd1.

Bibliography

[RR9557v1] François Clément and Vincent Martin, Finite element method. Detailed proofs to be formalized in Coq, RR-9557, first version, Inria Paris, 2024, https://inria.hal.science/hal-04713897v1.

From Requisite Require Import stdlib_wR ssr_wMC.

From Coquelicot Require Import Hierarchy Derive.
Close Scope R_scope.

From Algebra Require Import Algebra_wDep.
From FEM Require Import monomial multi_index.

Local Open Scope R_scope.

Section Pdk_Def.







[RR9557v1] Def 1503, p. 72.
Definition Monom_dk d k : '(FRd d)^((pbinom d k).+1) :=
  fun ipk xpowF_P (Adk d k ipk) x.

[RR9557v1] Def 1505, p. 72.
Definition Pdk d k : FRd d Prop := lin_span (Monom_dk d k).

[RR9557v1] Lem 1507, p. 72.
Lemma Pdk_cms : d k, compatible_ms (Pdk d k).
Proof. intros; apply lin_span_cms. Qed.

Definition Pdk_ms := fun d ksub_ModuleSpace (Pdk_cms d k).

End Pdk_Def.

Section Pkd_Facts1.

Lemma Monom_0k_eq : k, Monom_dk O k = fun _ _ ⇒ 1.
Proof.
intros k; unfold Monom_dk; rewrite A0k_eq; apply extF; intro.
apply fun_ext; intro; unfold powF_P; rewrite prod_R_nil; easy.
Qed.

Lemma P0k_eq : k p, Pdk 0 k p.
Proof.
intros k p; unfold Pdk; rewrite Monom_0k_eq; apply lin_span_ex.
(fun _p zero); apply fun_ext; intros x.
rewrite fct_lc_r_eq lc_ones_r -(sum_castF (pbinomS_0_l k)) sum_singleF.
f_equal; apply extF; intros [i Hi]; easy.
Qed.

Lemma Monom_d0_eq : d, Monom_dk d 0 = fun _ _ ⇒ 1.
Proof.
intros [| d]; unfold Monom_dk; apply extF; intros i; apply fun_ext; intros x.
rewrite A0k_eq; apply powF_P_zero_ext_r; easy.
unfold Adk; rewrite concatnF_one; [| apply inhabited_m].
rewrite CSd0_eq; unfold castF.
apply powF_P_zero_ext_r; easy.
Qed.

Lemma Pd0_eq : {d} (p:FRd d), Pdk d 0 p p = fun _p zero.
Proof.
intros d p; unfold Pdk.
rewrite Monom_d0_eq; split; intros H.
inversion H as [L HL].
apply fun_ext; intros x.
now repeat rewrite fct_lc_r_eq.
apply lin_span_ex.
(fun _p zero).
rewrite H.
apply fun_ext; intros x.
rewrite fct_lc_r_eq.
rewrite lc_ones_r.
assert (T: (S (pbinom d 0)) = S O).
apply pbinomS_0_r.
rewrite -(sum_castF T).
now rewrite sum_singleF.
Qed.

Lemma Monom_d1_0 : {d}, Monom_dk d 1 ord0 = fun _ ⇒ 1.
Proof.
intros d; unfold Monom_dk; apply fun_ext; intros x.
apply powF_P_zero_ext_r; intros i; rewrite Ad1_eq.
unfold castF; rewrite concatF_correct_l; easy.
Qed.

Lemma Monom_d1_S :
   {d} ipk (H : ipk ord0),
    Monom_dk d 1 ipk = fun xx (lower_S (cast_ordS_n0 (pbinomS_1_r d) _ H)).
Proof.
intros d ipk H; unfold Monom_dk; apply fun_ext; intros x; rewrite Ad1_S.
pose (k := cast_ord (pbinom_1_r d) (lower_S H)).
rewrite (powF_P_one _ _ 1 k)// pow_1; f_equal; apply ord_inj; easy.
Qed.

Lemma Monom_d1_S_alt :
   {d} i,
    @^~ i = Monom_dk d 1 (lift_S (cast_ord (eq_sym (pbinom_1_r d)) i)).
Proof.
intros; rewrite (Monom_d1_S _ (lift_S_not_first _)).
apply fun_ext; intros x; f_equal; rewrite lower_lift_S_cast_ord; easy.
Qed.

Lemma Monom_d1_am :
   {d} ipk,
    aff_map (Monom_dk d 1 ipk : fct_ModuleSpace R_ModuleSpace).
Proof.
intros d ipk; destruct (ord_eq_dec ipk ord0) as [-> | Hipk].
rewrite Monom_d1_0; apply: fct_cst_am.
rewrite Monom_d1_S; apply am_lm_0_equiv;
    rewrite minus_zero_r; apply lm_component.
Qed.

Lemma Pdk_ext :
   {d} k p q, ( x, p x = q x) Pdk d k p Pdk d k q.
Proof. intros d k p q H1 H2; replace q with p; [| apply fun_ext]; easy. Qed.

Lemma Pdk_lc :
   {d} {n} k p,
    ( i, Pdk d k (p i)) (L : 'R^n), Pdk d k (lin_comb L p).
Proof. intros; apply lin_span_lc_closed; easy. Qed.

Lemma Pdk_powF_P : d k ipk, Pdk d k (powF_P (Adk d k ipk)).
Proof.
intros d k ipk; apply lin_span_ex.
(itemF _ 1 ipk); rewrite lc_itemF_l scal_one; easy.
Qed.

Lemma Pdk_monot_S : {d} k p, Pdk d k p Pdk d k.+1 p.
Proof.
intros [| d] k p Hp; [apply P0k_eq |].
inversion Hp as [L HL].
apply lin_span_ex.
(castF (AdSk_eq_aux d k) (concatF L zero)).
unfold Monom_dk.
rewrite AdSk_eq.
rewrite (lc_ext_r
((castF (AdSk_eq_aux d k)
    (concatF (fun ipk : 'I_(pbinom d.+1 k).+1
               powF_P (Adk d.+1 k ipk))
        (fun ipkpowF_P (CSdk d k.+1 ipk)))))).
rewrite lc_castF.
rewrite (lc_concatF_zero_lr L); easy.
intros i; unfold castF; unfold concatF.
simpl (nat_of_ord (cast_ord _ i)).
case (lt_dec _ _); intros Hi; easy.
Qed.

Lemma Pdk_monot :
   {d} k1 k2 p, (k1 k2)%coq_nat Pdk d k1 p Pdk d k2 p.
Proof.
intros d k1 k2 p Hk H.
pose (t:= (k2-k1)%coq_nat).
assert (Ht: (k2 = k1 + t)%coq_nat) by auto with zarith.
rewrite Ht.
clear Hk Ht; generalize t; clear t k2.
induction t.
now rewrite Nat.add_0_r.
replace (k1+t.+1)%coq_nat with ((k1+t)%coq_nat.+1)%coq_nat.
2: now auto with zarith.
now apply Pdk_monot_S.
Qed.

Lemma PdSk_split_aux1 :
   {d n} k (p :'I_n FRd d.+1) L,
    ( i, p0 p1,
      Pdk d k.+1 p0 Pdk d.+1 k p1
      p i = fun xp0 (widenF_S x) + x ord_max × p1 x)
     p0 p1,
      Pdk d k.+1 p0 Pdk d.+1 k p1
      lin_comb L p = fun xp0 (widenF_S x) + x ord_max × p1 x.
Proof.
intros d n k p L H.
apply choiceF in H; destruct H as (p0,H).
apply choiceF in H; destruct H as (p1,H).
(lin_comb L p0); (lin_comb L p1); split.
apply Pdk_lc; apply H.
split.
apply Pdk_lc; apply H.
apply fun_ext; intros x.
rewrite 3!fct_lc_r_eq.
replace (_ + _) with (lin_comb L (p0^~ (widenF_S x)) +
    scal (x ord_max) (lin_comb L ((p1^~ x))))%M; try easy.
rewrite -lc_scal_r -lc_plus_r.
apply lc_ext_r.
intros i; rewrite (proj2 (proj2 (H i))); easy.
Qed.

Lemma PdSk_split_aux2 :
   {d} k (i : 'I_(pbinom d.+1 k.+1).+1),
     (p0 : FRd d) (p1 : FRd d.+1),
      Pdk d k.+1 p0 Pdk d.+1 k p1
      powF_P (Adk d.+1 k.+1 i) = fun xp0 (widenF_S x) + x ord_max × p1 x.
Proof.
intros d k i.
case (Nat.eq_dec (Adk d.+1 k.+1 i ord_max) O); intros H.
pose (j:= Adk_inv d k.+1 (widenF_S (Adk d.+1 k.+1 i))).
(powF_P (Adk d k.+1 j)).
(fun _ ⇒ 0).
split; try split.
apply Pdk_powF_P.
apply Pdk_monot with O; auto with arith.
apply Pd0_eq; easy.
apply fun_ext; intros x.
rewrite Rmult_0_r Rplus_0_r.
unfold j; rewrite Adk_inv_correct_r.
rewrite {1}(concatF_splitF_Sp1 x).
rewrite {1}(concatF_splitF_Sp1 (Adk d.+1 k.+1 i)).
rewrite powF_P_castF powF_P_concatF H.
rewrite (powF_P_zero_ext_r (singleF _)).
rewrite Rmult_1_r; easy.
intros l; rewrite singleF_0; easy.
apply Nat.add_le_mono_r with (Adk d.+1 k.+1 i ord_max).
replace (_ + _)%coq_nat with
    (sum (widenF_S (Adk d.+1 k.+1 i)) + Adk d.+1 k.+1 i ord_max)%M; try easy.
replace (k.+1 + _)%coq_nat with (k.+1 + Adk d.+1 k.+1 i ord_max)%M; try easy.
rewrite -sum_ind_r H plus_zero_r; apply Adk_sum.
(fun _ ⇒ 0).
pose (j:=Adk_inv d.+1 k
        (replaceF (Adk d.+1 k.+1 i)
                  (Adk d.+1 k.+1 i ord_max).-1 ord_max)).
(powF_P (Adk d.+1 k j)).
split; try split.
apply Pdk_monot with O; auto with arith.
apply Pd0_eq; easy.
apply Pdk_powF_P.
apply fun_ext; intros x.
rewrite Rplus_0_l.
case (Req_dec (x ord_max) 0); intros Hz.
rewrite Hz Rmult_0_l.
apply powF_P_zero_compat.
ord_max.
rewrite powF_correct.
rewrite Hz pow_i; auto with zarith.
unfold j; rewrite Adk_inv_correct_r.
apply Rmult_eq_reg_l with ((x ord_max)^(Adk d.+1 k.+1 i ord_max).-1).
rewrite -Rmult_assoc.
rewrite -{3}(pow_1 (x ord_max)) -Rdef_pow_add.
rewrite Nat.add_1_r Nat.succ_pred_pos; auto with zarith.
rewrite powF_P_replaceF_l; easy.
apply pow_nonzero; easy.
apply Nat.add_le_mono_l with (Adk d.+1 k.+1 i ord_max).
replace (_ + _)%coq_nat with (Adk d.+1 k.+1 i ord_max +
  sum (replaceF (Adk d.+1 k.+1 i) (Adk d.+1 k.+1 i ord_max).-1
       ord_max))%M; try easy.
rewrite sum_replaceF.
replace (_ + _)%M with
   ((Adk d.+1 k.+1 i ord_max).-1 + sum (Adk d.+1 k.+1 i))%coq_nat; try easy.
generalize (Adk_sum d.+1 k.+1 i); lia.
Qed.

Lemma PdSk_split :
   {d} k (p : FRd d.+1),
    Pdk d.+1 k.+1 p
     p0 p1,
      Pdk d k.+1 p0 Pdk d.+1 k p1
      p = fun xp0 (widenF_S x) + x ord_max × p1 x.
Proof.
intros d k p H; inversion H as (L,HL).
apply PdSk_split_aux1; intros; unfold Monom_dk; apply PdSk_split_aux2.
Qed.

Lemma Pdk_mult_const :
   {d} k (p q : FRd d),
    Pdk d k p (q = fun _q zero) Pdk d k (p × q)%K.
Proof.
intros d k p q H1 H2.
replace (p × q)%K with (scal (q zero) p).
apply lin_span_scal_closed; easy.
apply fun_ext; intros x; rewrite H2 fct_mult_eq mult_comm_R; easy.
Qed.

Lemma Pdk_mul_var :
   {d} k (p : FRd d.+1) i,
    Pdk d.+1 k p Pdk d.+1 k.+1 (fun xx i × p x).
Proof.
intros d k p i H; inversion H as [L HL].
apply Pdk_ext with
   (lin_comb L (fun j xx i × Monom_dk d.+1 k j x)).
intros x.
apply trans_eq with (scal (x i) (lin_comb L (Monom_dk d.+1 k) x)); try easy.
rewrite fct_lc_r_eq.
rewrite lc_scal_r.
f_equal; now rewrite fct_lc_r_eq.
apply Pdk_lc.
intros j; unfold Monom_dk.
apply Pdk_ext with
   (powF_P (Adk d.+1 k.+1
             (Adk_inv d.+1 k.+1
                 (replaceF (Adk d.+1 k j) (Adk d.+1 k j i).+1%coq_nat i)))).
2: apply Pdk_powF_P.
intros x; rewrite Adk_inv_correct_r.
case (Req_dec (x i) 0); intros Hxi.
rewrite Hxi; rewrite Rmult_0_l.
apply powF_P_zero_compat.
i; unfold powF, map2F; rewrite Hxi.
rewrite pow_ne_zero; try easy.
rewrite replaceF_correct_l; auto with arith.
apply Rmult_eq_reg_l with ((x i)^((Adk d.+1 k j i))).
rewrite powF_P_replaceF_l.
rewrite -tech_pow_Rmult; ring.
apply pow_nonzero; easy.
apply Nat.add_le_mono_l with (Adk d.+1 k j i).
replace (_ + _)%coq_nat with
   (Adk d.+1 k j i +
  sum (replaceF (Adk d.+1 k j) (Adk d.+1 k j i).+1 i))%M; try easy.
rewrite sum_replaceF.
replace (_ + _)%M with ((Adk d.+1 k j i).+1 + sum (Adk d.+1 k j))%coq_nat; try easy.
generalize (Adk_sum d.+1 k j); lia.
Qed.

Lemma Pdk_widenF_S :
   {d} k (p : FRd d), Pdk d k p Pdk d.+1 k (fun xp (widenF_S x)).
Proof.
intros d k p H; inversion H.
apply Pdk_ext with
   (lin_comb L (fun i xMonom_dk d k i (widenF_S x))).
intros x.
now rewrite 2!fct_lc_r_eq.
apply Pdk_lc.
intros i; unfold Monom_dk.
apply Pdk_ext with
   (powF_P (Adk d.+1 k
             (Adk_inv d.+1 k
                 (castF (Nat.add_1_r d) (concatF (Adk d k i) (singleF zero)))))).
2: apply Pdk_powF_P.
intros x; rewrite Adk_inv_correct_r.
assert (T: x = (castF (Nat.add_1_r d)
          (concatF (widenF_S x) (singleF (x ord_max))))).
rewrite concatF_splitF_Sp1'.
apply extF; intros j; unfold castF, castF_Sp1, castF.
f_equal; apply ord_inj; easy.
rewrite {1}T.
rewrite powF_P_castF.
rewrite powF_P_concatF.
rewrite (powF_P_zero_ext_r (singleF _)); try ring.
intros j; apply singleF_0.
rewrite sum_castF sum_concatF.
rewrite sum_singleF plus_zero_r.
apply Adk_sum.
Qed.

Lemma Pdk_mult_le :
   {d} n k l p q,
    Pdk d k p Pdk d l q (k + l n)%coq_nat Pdk d n (p × q)%K.
Proof.
intros d n ; apply nat_ind2_strong with
   (P:= fun d n k l p q,
    Pdk d k p Pdk d l q
     (k+l n)%coq_nat
      Pdk d n (p×q)%K); clear d n.
intros d; case d.
intros n Hrec k l p q H1 H2 H3.
apply P0k_eq.
clear d; intros d n Hrec k.
case k; clear k.
clear; intros l p q H1 H2 H3.
apply Pdk_monot with l; auto with arith.
replace (p×q)%K with (q×p)%K.
apply Pdk_mult_const; try easy.
apply Pd0_eq; easy.
apply fun_ext; intros x.
unfold mult; simpl; unfold fct_mult; simpl.
unfold mult; simpl; auto with real.
intros k l.
case l; clear l.
clear; intros p q H1 H2 H3.
apply Pdk_monot with k.+1.
apply Nat.le_trans with (2:=H3).
auto with arith.
apply Pdk_mult_const; try easy.
apply Pd0_eq; easy.
intros l p q Hp Hq Hn.
assert (Hn2: (1 < n)%coq_nat).
apply Nat.lt_le_trans with (2:=Hn).
case k; case l; auto with arith.
destruct (PdSk_split _ p Hp) as (p1,(p2,(Yp1,(Yp2,Yp3)))).
destruct (PdSk_split _ q Hq) as (q1,(q2,(Yq1,(Yq2,Yq3)))).
replace (p×q)%K with
     ((fun x ⇒ (p1×q1)%K (widenF_S x))
     + (fun xx ord_max × (p1 (widenF_S x) × q2 x + p2 x × q1 (widenF_S x)))
     + (fun xx ord_max × (x ord_max × (p2×q2)%K x)))%M.
repeat apply: lin_span_plus_closed.
apply Pdk_widenF_S.
apply: (Hrec d n _ _ _ k.+1 l.+1); auto with arith.
apply pair_neq_spec; left; easy.
replace n with ((n.-1).+1) by auto with zarith.
apply Pdk_mul_var.
apply: lin_span_plus_closed.
apply: (Hrec d.+1 n.-1 _ _ _ k.+1 l); auto with arith.
apply pair_neq_spec; right; auto with zarith.
apply Pdk_widenF_S; easy.
apply le_S_n; apply Nat.le_trans with n; auto with zarith.
apply Nat.le_trans with (2:=Hn); auto with arith.
apply: (Hrec d.+1 n.-1 _ _ _ k l.+1); auto with arith.
apply pair_neq_spec; right; auto with zarith.
apply Pdk_widenF_S; easy.
apply le_S_n; apply Nat.le_trans with n; auto with zarith.
replace n with ((n.-2).+2) by auto with zarith.
apply Pdk_mul_var.
apply Pdk_mul_var.
apply: (Hrec d.+1 n.-2 _ _ _ k l); auto with zarith arith.
apply pair_neq_spec; right; auto with zarith.
apply le_S_n, le_S_n; apply Nat.le_trans with n; auto with zarith.
apply Nat.le_trans with (2:=Hn); apply PeanoNat.Nat.eq_le_incl.
rewrite -PeanoNat.Nat.add_succ_r; auto with zarith arith.
apply fun_ext; intros x; unfold plus, mult; simpl.
unfold fct_plus, fct_mult; simpl.
unfold mult; simpl; unfold plus; simpl.
rewrite Yp3 Yq3; ring.
Qed.

Lemma Pdk_mult :
   {d} k l p q,
    Pdk d k p Pdk d l q Pdk d (k + l)%coq_nat (p × q)%K.
Proof. intros; apply Pdk_mult_le with k l; easy. Qed.

Lemma Pdk_mult_iter :
   {d n} (k : 'I_n nat) p m,
    ( i, Pdk d (k i) (p i))
    (sum k m)%coq_nat
    Pdk d m (fun xprod_R (fun ip i x)).
Proof.
intros d n; induction n.
intros k p m Hi Hm.
apply Pdk_monot with O; auto with arith.
apply Pd0_eq.
apply fun_ext; intros x.
unfold prod_R; now rewrite 2!sum_nil.
intros k p m Hi Hm.
apply Pdk_ext with
 ( (fun x(p^~ x) ord0) × (fun xprod_R (liftF_S (p^~ x)))%M)%K.
intros x; rewrite prod_R_ind_l; simpl; easy.
apply Pdk_mult_le with (k ord0) (sum (liftF_S k)).
apply Hi.
apply IHn with (liftF_S k); try easy.
intros i; apply Hi.
apply Nat.le_trans with (2:=Hm).
rewrite sum_ind_l; auto with arith.
Qed.

Lemma Pd1_am_1_equiv :
   {d} (f : 'R^d R),
    Pdk d 1 f aff_map (f : fct_ModuleSpace R_ModuleSpace).
Proof.
intros d f; split; intros Hf.
inversion Hf as [L HL]; apply am_f_lc; intro; apply Monom_d1_am.
destruct (proj1 (am_ms_equiv) Hf) as [lf [c [Hlf ->]]].
apply: lin_span_plus_closed.
2: apply Pdk_monot with O; [apply Nat.le_0_1 | apply Pd0_eq; easy].
rewrite (lm_decomp_1 _ Hlf). eapply Pdk_ext; [| eapply Pdk_lc].
intros x; rewrite fct_lc_r_eq; easy.
intros i; simpl; rewrite Monom_d1_S_alt; apply lin_span_inclF_diag.
Qed.

Lemma Pd1_am_equiv :
   {d n} (f : 'R^d 'R^n),
    ( l, Pdk d 1 (scatter f l))
    aff_map (f : fct_ModuleSpace fct_ModuleSpace).
Proof.
intros; split; intros Hf.
assert (H : l, aff_map (scatter f l : fct_ModuleSpace R_ModuleSpace)).
  intros; apply Pd1_am_1_equiv; easy.
apply scatter_am_compat in H; unfold scatter, swap in H.
apply (am_lm_rev (0%M : fct_ModuleSpace)) in H.
apply (am_lm (0%M : fct_ModuleSpace)); easy.
intros; apply Pd1_am_1_equiv, scatter_am_compat.
apply (am_lm_rev (0%M : fct_ModuleSpace)) in Hf.
apply (am_lm (0%M : fct_ModuleSpace)); easy.
Qed.

Lemma Pdk_pow_am :
   {d n} (f : 'R^d 'R^n) (l : 'I_n) m,
    aff_map (f : fct_ModuleSpace fct_ModuleSpace)
    Pdk d m (fun xpow (f x l) m).
Proof.
intros d n f l m Hf.
apply Pdk_ext with (fun xprod_R (fun i:'I_mf x l)).
intros x.
clear; induction m.
simpl; now rewrite prod_R_nil.
rewrite prod_R_ind_l IHm -tech_pow_Rmult; easy.
apply Pdk_mult_iter with (fun _S O).
intros j.
now apply Pd1_am_equiv.
rewrite sum_constF_nat; auto with zarith.
Qed.

Lemma Pdk_comp_am :
   {d n} k (p : FRd d) (f : 'R^n 'R^d),
    aff_map (f : fct_ModuleSpace fct_ModuleSpace)
    Pdk d k p Pdk n k (p \o f).
Proof.
intros d n k p f Hf Hp; inversion Hp as [L HL].
rewrite -lc_compF_rl; apply Pdk_lc; intros i.
apply Pdk_mult_iter with (Adk d k i); [| apply Adk_sum].
intros j; apply Pdk_pow_am; easy.
Qed.

Lemma Pdk_comp_am_rev :
   {d} k (p : FRd d) (f : 'R^d 'R^d),
    aff_map (f : fct_ModuleSpace fct_ModuleSpace) bijective f
    Pdk d k (p \o f) Pdk d k p.
Proof.
intros d k p f Hf1 Hf2 H; rewrite -(comp_id_r p) -(f_inv_id_r Hf2).
rewrite comp_assoc; apply Pdk_comp_am; [| easy].
apply: am_bij_compat; easy.
Qed.

Lemma Pdk_am_comp_basis :
   {d} k (B : '(FRd d)^(pbinom d k).+1) (f : 'R^d 'R^d),
  lin_gen (Pdk d k) B
  aff_map (f : fct_ModuleSpace fct_ModuleSpace)
  bijective (f : fct_ModuleSpace fct_ModuleSpace)
  Pdk d k = lin_span (compF_l B f).
Proof.
intros d k B f HB Hf1 Hf2; apply subset_ext_equiv; split; intros p Hp.
generalize (am_bij_compat Hf2 Hf1); intros Hfi1.
generalize (Pdk_comp_am _ _ _ Hfi1 Hp); intros H1.
rewrite HB in H1; inversion H1 as [L HL].
apply lin_span_ex; L; apply fun_ext; intros x.
rewrite -(comp_id_r p) -(f_inv_id_l Hf2) comp_assoc lc_compF_rl HL; easy.
inversion Hp as [L HL]; apply Pdk_lc; intros i.
apply Pdk_comp_am; [easy | apply (lin_gen_inclF HB)].
Qed.

End Pkd_Facts1.

Section Derive_Gen.

We here define differentials of polynomials (from Coquelicot's derivative). We have any number of derivative on a function with any number of variables. This is a limited development (on polynomials only as the only goal here is to prove Monom_dk_lin_indep, that is to say Monom_dk is a lin_indep family.

Lemma is_derive_ext':
   {K : AbsRing} {V : NormedModule K} (f : K V)
    (x : K) (l1 l2 : V),
    l1 = l2 is_derive f x l1 is_derive f x l2.
Proof.
intros ; subst; easy.
Qed.

Lemma ex_derive_lc :
   {n} (f :'I_n (RR)) (L:'R^n),
    ( i x, ex_derive (f i) x)
       x, ex_derive (lin_comb L f) x.
Proof.
intros n f L H.
assert (H0: lc_closed (fun (g:RR) ⇒ x, ex_derive g x)).
2: now apply H0.
apply cms_lc.
apply plus_scal_closed_cms.
(fun _ ⇒ 0); intros x.
apply ex_derive_const.
intros g h H1 H2 x.
apply: ex_derive_plus; easy.
intros g l H1 x.
apply ex_derive_scal; easy.
Qed.

Lemma is_derive_lc :
   {n} (f :'I_n (RR)) (L:'R^n) (d :'I_n (RR)),
    ( i x, is_derive (f i) x (d i x))
       x, is_derive (lin_comb L f) x (lin_comb L d x).
Proof.
intros n; induction n.
intros f L d H x.
rewrite 2!lc_nil fct_zero_eq.
unfold zero; simpl; unfold fct_zero.
eapply is_derive_ext';[| apply is_derive_const]; easy.
intros f L d H x.
rewrite 2!lc_ind_l.
apply: is_derive_plus.
apply is_derive_scal; easy.
apply IHn; try easy.
intros i y; unfold liftF_S; apply H.
Qed.


Definition ex_derive_onei {n} :=
  fun (i:'I_n) (f: 'R^n R) (x:'R^n) ⇒
     ex_derive (fun yf (replaceF x y i)) (x i).

Definition is_derive_onei {n} :=
  fun (i:'I_n) (f: 'R^n R) (x:'R^n) (l:R) ⇒
     is_derive (fun yf (replaceF x y i)) (x i) l.

Definition Derive_onei {n} :=
   fun (i:'I_n) (f: 'R^n R) (x:'R^n) ⇒
      Derive (fun yf (replaceF x y i)) (x i).

Definition ex_derive_multii {n} :=
  fun (i:'I_n) (j:nat) (f: 'R^n R) (x:'R^n) ⇒
      ex_derive_n (fun yf (replaceF x y i)) j (x i).

Definition is_derive_multii {n} :=
  fun (i:'I_n) (j:nat) (f: 'R^n R) (x:'R^n) (l:R) ⇒
      is_derive_n (fun yf (replaceF x y i)) j (x i) l.

Definition Derive_multii {n} (i:'I_n) (j:nat) (f: 'R^n R) (x:'R^n):=
   Derive_n (fun yf (replaceF x y i)) j (x i).

Lemma ex_derive_onei_lc :
   {n m} (j:'I_n) (f :'I_m ('R^nR)) (L:'R^m),
    ( i x, ex_derive_onei j (f i) x)
       x, ex_derive_onei j (lin_comb L f) x.
Proof.
intros n m j f L; unfold ex_derive_onei; intros H x.
apply ex_derive_ext with
 (lin_comb L (fun (i : 'I_m) (y : R) ⇒ f i (replaceF x y j))).
intros t; rewrite 2!fct_lc_r_eq; easy.
apply ex_derive_lc.
intros i y; specialize (H i (replaceF x y j)).
rewrite replaceF_correct_l in H; try easy.
apply ex_derive_ext with (2:=H).
intros t; f_equal; apply extF; intros k.
unfold replaceF; case (ord_eq_dec _ _); try easy.
Qed.

Lemma is_derive_onei_lc :
   {n m} (j:'I_n) (f :'I_m ('R^nR)) (L:'R^m) (d:'I_m ('R^n R)),
    ( i x, is_derive_onei j (f i) x (d i x))
       x, is_derive_onei j (lin_comb L f) x (lin_comb L d x).
Proof.
intros n m j f L d; unfold is_derive_onei; intros H x.
apply is_derive_ext with
 (lin_comb L (fun (i : 'I_m) (y : R) ⇒ f i (replaceF x y j))).
intros t; rewrite 2!fct_lc_r_eq; easy.
apply is_derive_ext' with (lin_comb L (fun i yd i (replaceF x y j)) (x j)).
rewrite 2! fct_lc_r_eq.
apply lc_ext_r.
intros i; f_equal.
apply replaceF_id.
apply is_derive_lc.
intros i y; specialize (H i (replaceF x y j)).
rewrite replaceF_correct_l in H; try easy.
apply is_derive_ext with (2:=H).
intros t; f_equal; apply extF; intros k.
unfold replaceF; case (ord_eq_dec _ _); try easy.
Qed.

Lemma is_derive_onei_unique : {n} i (f:'R^nR) x l,
   is_derive_onei i f x l Derive_onei i f x = l.
Proof.
intros n i f x l; unfold is_derive_onei, Derive_onei; intros H.
apply is_derive_unique; easy.
Qed.

Lemma is_derive_multii_unique : {n} (i:'I_n) j f x l,
    is_derive_multii i j f x l Derive_multii i j f x = l.
Proof.
intros n i j f x l; unfold is_derive_multii, Derive_multii; intros H.
apply is_derive_n_unique; easy.
Qed.

Lemma is_derive_multii_scal : {n} (i:'I_n) j f x l (k:R),
     is_derive_multii i j f x l
     is_derive_multii i j (scal k f) x (scal k l).
Proof.
intros; apply is_derive_n_scal_l; easy.
Qed.

Lemma Derive_multii_scal : {n} (i:'I_n) j f x (k:R),
     Derive_multii i j (scal k f) x
       = scal k (Derive_multii i j f x).
Proof.
intros n i j f x k; unfold Derive_multii.
rewrite Derive_n_scal_l; easy.
Qed.

Definition Derive_alp {n} (alpha : 'nat^n) : '(('R^nR) ('R^nR))^n :=
  fun iDerive_multii i (alpha i).

Definition DeriveF_part {n} (alpha : 'nat^n) (j:'I_n.+1) : ('R^nR) ('R^nR) :=
  comp_n_part (Derive_alp alpha) j.

Lemma DeriveF_part_ext_alp :
   {n} (alpha1 alpha2 : 'nat^n) j,
    eqAF (widenF (leq_ord j) alpha1) (widenF (leq_ord j) alpha2)
    DeriveF_part alpha1 j = DeriveF_part alpha2 j.
Proof.
move=>> H; apply comp_n_part_ext; move=>>; apply fun_ext; intro.
unfold widenF, Derive_alp in *; rewrite H; easy.
Qed.

Lemma DeriveF_part_extf : {n} (alpha:'nat^n) j f1 f2,
    same_fun f1 f2 DeriveF_part alpha j f1 = DeriveF_part alpha j f2.
Proof.
move=>> /fun_ext Hf; subst; easy.
Qed.

Lemma DeriveF_part_0 :
   {n} (alpha:'nat^n) j, j = ord0 DeriveF_part alpha j = ssrfun.id.
Proof. intros; apply comp_n_part_0; easy. Qed.

Lemma DeriveF_part_nil :
   {n} (alpha:'nat^n) j, n = 0%nat DeriveF_part alpha j = ssrfun.id.
Proof. intros; apply comp_n_part_nil; easy. Qed.

Lemma DeriveF_part_full :
   {n} (alpha:'nat^n) j,
    j = ord_max DeriveF_part alpha j = comp_n (Derive_alp alpha).
Proof. intros; apply comp_n_part_max; easy. Qed.

Lemma DeriveF_part_ind_l :
   {n} (alpha:'nat^n.+1) {j} (H : j ord0),
    DeriveF_part alpha j =
      Derive_alp alpha ord0 \o
      comp_n_part (liftF_S (Derive_alp alpha)) (lower_S H).
Proof. intros; apply comp_n_part_ind_l; easy. Qed.

Lemma DeriveF_part_ind_r :
   {n} (alpha : 'nat^n) (j:'I_n),
    DeriveF_part alpha (lift_S j) =
      DeriveF_part alpha (widen_S j) \o Derive_alp alpha j.
Proof. intros; apply comp_n_part_ind_r. Qed.

Definition DeriveF {n} (alpha : 'nat^n) : ('R^nR) ('R^nR) :=
  comp_n (Derive_alp alpha).

Lemma DeriveF_correct :
   {n} (alpha : 'nat^n), DeriveF alpha = DeriveF_part alpha ord_max.
Proof. intros; apply eq_sym, DeriveF_part_full; easy. Qed.

Lemma DeriveF_ext_alp :
   {n} (alpha1 alpha2 : 'nat^n),
    eqAF alpha1 alpha2 DeriveF alpha1 = DeriveF alpha2.
Proof.
intros; rewrite !DeriveF_correct; apply DeriveF_part_ext_alp.
rewrite !widenF_full; easy.
Qed.

Lemma DeriveF_extf : {n} (alpha : 'nat^n) f1 f2,
    same_fun f1 f2 DeriveF alpha f1 = DeriveF alpha f2.
Proof. move=>> /fun_ext Hf; subst; easy. Qed.

Lemma DeriveF_nil :
   {n} (alpha : 'nat^n), n = 0%nat DeriveF alpha = ssrfun.id.
Proof. intros; apply comp_n_nil; easy. Qed.

Lemma DeriveF_ind_l :
   {n} (alpha : 'nat^n.+1),
    DeriveF alpha =
      Derive_alp alpha ord0 \o comp_n (liftF_S (Derive_alp alpha)).
Proof. intros; apply comp_n_ind_l; easy. Qed.

Lemma DeriveF_ind_r :
   {n} (alpha : 'nat^n.+1),
    DeriveF alpha =
      comp_n (widenF_S (Derive_alp alpha)) \o Derive_alp alpha ord_max.
Proof. intros; apply comp_n_ind_r. Qed.

Lemma Derive_multii_scal_fun : {n} (i:'I_n) j f1 f2,
    ( x y, f1 x = f1 (replaceF x y i))
     Derive_multii i j (fun xf1 x× f2 x)
       = (fun xf1 x*(Derive_multii i j f2 x)).
Proof.
intros n i j f1 f2 H1.
apply fun_ext; intros x; unfold Derive_multii.
rewriteDerive_n_ext with (g:=fun yf1 x × f2 (replaceF x y i)).
2: intros t; rewrite -H1; easy.
now rewrite Derive_n_scal_l.
Qed.

Definition narrow_ord_max := fun {n:nat} (f:'R^n.+1 R) (x:'R^n) ⇒
   f (castF (eq_sym (addn1_sym n)) (concatF x (singleF 0))).

Lemma narrow_ord_max_correct : {n:nat} f,
   ( (x:'R^n.+1) y, f x = f (replaceF x y ord_max))
   ( 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 narrow_ord_max_Derive_multii :
    {n} (f:'R^n.+1R) i j (H: i ord_max),
   ( (x:'R^n.+1) y, f x = f (replaceF x y ord_max))
    (narrow_ord_max (Derive_multii i j f)) =
       Derive_multii (narrow_S H) j (narrow_ord_max f).
Proof.
intros n f i j H H1.
assert (Hi : (i < n)%coq_nat).
generalize H; destruct i as (ii, Hii); simpl.
intros T; apply ord_neq_compat in T; simpl in T.
assert (ii < n.+1)%coq_nat; [now apply /ltP | lia].
unfold narrow_ord_max, Derive_multii; apply fun_ext; intros x; f_equal.
apply fun_ext; intros y; f_equal.
apply extF; intros m; unfold replaceF.
case (ord_eq_dec m i); intros Hm.
subst; unfold castF; rewrite concatF_correct_l; try easy.
case (ord_eq_dec _ _); try easy.
intros T; apply ord_neq_compat in T; simpl in T; easy.
unfold castF, concatF.
case (lt_dec _ _); intros H2; try easy.
case (ord_eq_dec _ _); try easy.
intros T; contradict T.
apply ord_neq; simpl; apply ord_neq_compat; easy.
unfold castF; rewrite concatF_correct_l; try easy.
f_equal; apply ord_inj; now simpl.
Qed.

Lemma DeriveF_part_scal_fun : {n} i (alpha:'nat^n.+1) (Hi: iord_max) (g1:RR) (g2: 'R^n.+1 R),
  ( (x:'R^n.+1) y, g2 x = g2 (replaceF x y ord_max))
  DeriveF_part alpha i (fun x:'R^n.+1g1 (x ord_max) × g2 x)
     = (fun x:'R^n.+1g1 (x ord_max)
          × DeriveF_part (widenF_S alpha) (narrow_S Hi) (narrow_ord_max g2) (widenF_S x)).
Proof.
intros n (i,Hi); induction i.
intros alpha Hi0 g1 g2 H1; apply fun_ext; intros x.
rewrite DeriveF_part_0; try rewrite DeriveF_part_0; try easy; f_equal.
now apply narrow_ord_max_correct.
apply ord_inj; simpl; easy.
apply ord_inj; simpl; easy.
intros alpha Hi0 g1 g2 H1.
assert (Hi' : (i < n.+1)%nat).
apply /ltP; apply PeanoNat.lt_S_n.
now apply /ltP.
assert (Hi'' : (i < n)%nat).
apply /ltP; apply ord_neq_compat in Hi0; simpl in Hi0.
assert (i < n.+1)%coq_nat by now apply /ltP.
now auto with zarith.
assert (Hi0'' : (i n)).
generalize Hi''; move ⇒ /ltP; lia.
replace (@Ordinal (n.+2) (i.+1) Hi) with (lift_S (Ordinal Hi')) at 1.
2: apply ord_inj; easy.
rewrite DeriveF_part_ind_r comp_correct; unfold Derive_alp.
rewrite Derive_multii_scal_fun.
rewrite IHi.
apply ord_neq; simpl.
apply Nat.lt_neq; now apply /ltP.
intros H0; apply fun_ext; intros x; f_equal.
replace (narrow_S Hi0) with (lift_S (Ordinal Hi'')).
2: apply ord_inj; simpl; easy.
rewrite DeriveF_part_ind_r comp_correct; f_equal; try easy.
apply ord_inj; simpl; easy.
rewrite narrow_ord_max_Derive_multii; try easy.
apply ord_neq; now simpl.
intros H2; unfold Derive_alp; f_equal; try easy.
apply ord_inj; now simpl.
unfold widenF_S; f_equal; apply ord_inj; now simpl.
intros x y; unfold Derive_multii; f_equal.
apply fun_ext; intros z.
fold (replace2F x y z ord_max (Ordinal Hi')).
rewrite replace2F_equiv_def; try easy.
apply ord_neq; simpl; easy.
rewrite replaceF_correct_r; try easy.
apply ord_neq; simpl; easy.
intros x y; rewrite replaceF_correct_r; try easy.
apply ord_neq; simpl; apply sym_not_eq; easy.
Qed.

Lemma DeriveF_ind_r_scal_fun : {n} (alpha : 'nat^n.+1) f (g1:RR) (g2: 'R^n.+1 R),
   ( (x:'R^n.+1), Derive_alp alpha ord_max f x = g1 (x ord_max) × g2 x)
   ( (x:'R^n.+1) y, g2 x = g2 (replaceF x y ord_max))
   DeriveF alpha f = fun xg1 (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.

Definition is_Poly {n} (f: 'R^n R) := k, Pdk n k f.

Lemma is_Poly_ext : {n} (f1 f2 : 'R^n R),
  f1 = f2 is_Poly f1 is_Poly f2.
Proof.
intros; subst; easy.
Qed.

Lemma is_Poly_zero : {n}, @is_Poly n zero.
Proof.
intros n; O.
apply Pd0_eq; easy.
Qed.

Lemma is_Poly_scal : {n} l (f : 'R^n R),
    is_Poly f is_Poly (scal l f).
Proof.
intros n l f (k,Hk).
k; apply lin_span_scal_closed; easy.
Qed.

Lemma is_Poly_plus : {n} (f1 f2 : 'R^n R),
  is_Poly f1 is_Poly f2 is_Poly (f1+f2)%M.
Proof.
intros n f1 f2 (k1,Hk1) (k2,Hk2).
(max k1 k2).
apply: lin_span_plus_closed.
apply Pdk_monot with k1; auto with arith.
apply Pdk_monot with k2; auto with arith.
Qed.

Lemma is_Poly_lc : {n m} (f : 'I_m 'R^n R) L,
  ( i, is_Poly (f i)) is_Poly (lin_comb L f).
Proof.
intros n m; induction m.
intros f L H.
rewrite lc_nil.
apply is_Poly_zero.
intros f L H.
rewrite lc_ind_l.
apply is_Poly_plus.
apply is_Poly_scal; easy.
apply IHm.
intros i; unfold liftF_S; apply H.
Qed.

Lemma is_Poly_Monom_dk : {d k} i,
    is_Poly (Monom_dk d k i).
Proof.
intros d k i; k.
apply lin_span_inclF; intros j; now j.
Qed.

Lemma is_Poly_powF_P : {d} (beta : 'nat^d),
   is_Poly (powF_P beta).
Proof.
intros d beta.
pose (k:= sum beta).
apply is_Poly_ext with (Monom_dk d k (Adk_inv d k beta)).
2: apply is_Poly_Monom_dk.
unfold Monom_dk; rewrite Adk_inv_correct_r; easy.
Qed.

Lemma is_derive_powF_P : {n} (beta:'nat^n) i x,
    is_derive_onei i (powF_P beta) x
      (INR (beta i) × powF_P (replaceF beta (beta i).-1 i) x).
Proof.
intros n; induction n.
intros beta i; exfalso; apply I_0_is_empty; apply (inhabits i).
intros beta i x; unfold powF_P, is_derive_onei.
eapply is_derive_ext.
intros t; rewrite prod_R_ind_l; easy.
case (ord_eq_dec i ord0); intros Hi.
subst; unfold liftF_S.
apply is_derive_ext with
  (fun t ⇒ (prod_R
      (fun i : 'I_n
       powF x beta (lift_S i)) × t^(beta ord0))).
intros t; unfold plus; rewrite Rmult_comm; simpl; f_equal.
unfold powF, map2F; now rewrite replaceF_correct_l.
f_equal; apply extF; intros i.
unfold powF, map2F; rewrite replaceF_correct_r; easy.
apply is_derive_ext' with ( (prod_R (fun i : 'I_npowF x beta (lift_S i))) ×
       (INR (beta ord0)×1×x ord0^(beta ord0).-1)).
rewrite Rmult_comm Rmult_assoc Rmult_1_r.
f_equal; rewrite (prod_R_ind_l); unfold plus; simpl; f_equal.
unfold powF, map2F; rewrite replaceF_correct_l; try easy.
f_equal; apply extF; intros i.
unfold powF, map2F, liftF_S.
rewrite replaceF_correct_r; easy.
apply is_derive_scal.
apply is_derive_pow.
apply is_derive_ext' with (@one (AbsRing.Ring R_AbsRing)); try easy.
apply is_derive_id.
apply is_derive_ext with
 (fun t ⇒ ( (x ord0)^(beta ord0) ×
            (prod_R ((powF (replaceF (liftF_S x) t (lower_S Hi)) (liftF_S beta)))))).
intros t; unfold plus; simpl; f_equal.
unfold powF, map2F; rewrite replaceF_correct_r; try easy.
f_equal; apply extF; intros j.
unfold powF, map2F, liftF_S; f_equal.
unfold replaceF; case (ord_eq_dec _ _); intros Hj.
rewrite Hj lift_lower_S; case (ord_eq_dec _ _); easy.
case (ord_eq_dec _ _); intros Hj'; try easy.
absurd (lift_S j = (lift_S (lower_S Hi))).
intros H; apply Hj.
unfold lift_S in H; apply (lift_inj H).
now rewrite lift_lower_S.
apply is_derive_ext' with ( (x ord0)^(beta ord0) ×
         (INR (beta i) × prod_R (powF (liftF_S x)
                                (replaceF (liftF_S beta) (beta i).-1 (lower_S Hi))))).
rewrite Rmult_comm Rmult_assoc; f_equal; rewrite Rmult_comm.
rewrite prod_R_ind_l; unfold plus; simpl; f_equal.
unfold powF, map2F; rewrite replaceF_correct_r; try easy.
f_equal; apply extF; intros j.
unfold powF, map2F, liftF_S; f_equal.
unfold replaceF; case (ord_eq_dec _ _); intros Hj.
rewrite Hj lift_lower_S; case (ord_eq_dec _ _); easy.
case (ord_eq_dec _ _); intros Hj'; try easy.
absurd (lift_S j = (lift_S (lower_S Hi))).
intros H; apply Hj.
unfold lift_S in H; apply (lift_inj H).
now rewrite lift_lower_S.
apply is_derive_scal.
specialize (IHn (liftF_S beta) (lower_S Hi) (liftF_S x)).
unfold powF_P, is_derive_onei in IHn.
replace (liftF_S beta (lower_S Hi)) with (beta i) in IHn.
replace (liftF_S x (lower_S Hi)) with (x i) in IHn.
exact IHn.
unfold liftF_S; now rewrite lift_lower_S.
unfold liftF_S; now rewrite lift_lower_S.
Qed.

Lemma is_Poly_ex_derive : {n} (f: 'R^n R),
   is_Poly f ( i x, ex_derive_onei i f x).
Proof.
intros n f (k,Hf) i x; destruct Hf.
apply ex_derive_onei_lc.
intros j y; unfold Monom_dk; eexists.
apply is_derive_powF_P.
Qed.

Lemma is_Poly_Derive_is_Poly : {n} (f: 'R^n R),
   is_Poly f ( i, is_Poly (Derive_onei i f)).
Proof.
intros n; case n.
intros f H i.
exfalso; apply I_0_is_empty; apply (inhabits i).
clear n; intros n f (k,Hk) i; inversion Hk.
eapply is_Poly_ext.
apply eq_sym; apply fun_ext; intros x.
apply is_derive_onei_unique.
apply is_derive_onei_lc.
intros j y; unfold Monom_dk.
apply is_derive_powF_P.
k.
apply lin_span_lin_span; intros j.
apply: lin_span_scal_closed.
apply lin_span_ub with
  (Adk_inv n.+1 k (replaceF (Adk n.+1 k j) (Adk n.+1 k j i).-1 i)).
unfold Monom_dk.
rewrite Adk_inv_correct_r; try easy.
apply Nat.add_le_mono_l with (Adk n.+1 k j i).
replace (_ +_)%coq_nat with
 (Adk n.+1 k j i + sum (replaceF (Adk n.+1 k j) (Adk n.+1 k j i).-1 i))%M by easy.
rewrite sum_replaceF.
generalize (Adk_sum n.+1 k j).
unfold plus; simpl; auto with zarith.
Qed.

Lemma is_Poly_Derive_n_is_Poly : {n} (f: 'R^n R),
   is_Poly f ( i m, is_Poly (Derive_multii i m f)).
Proof.
intros n f H i; unfold Derive_multii; induction m; simpl; try easy.
apply is_Poly_ext with (2:=H).
apply fun_ext; intros x.
now rewrite replaceF_id.
eapply is_Poly_ext.
2: apply is_Poly_Derive_is_Poly.
2: apply IHm.
apply fun_ext; intros x; unfold Derive_onei.
f_equal; apply fun_ext; intros y.
rewrite replaceF_correct_l; try easy.
f_equal; apply fun_ext; intros z; f_equal.
unfold replaceF; apply extF; intros j.
case (ord_eq_dec _ _); easy.
Qed.

Lemma is_Poly_ex_derive_n : {n} (f: 'R^n R),
   is_Poly f ( i m x, ex_derive_multii i m f x).
Proof.
intros n f H i m x; unfold ex_derive_multii.
induction m; try easy; simpl.
assert (H1: ex_derive_onei i (Derive_multii i m f) x).
apply is_Poly_ex_derive.
now apply is_Poly_Derive_n_is_Poly.
apply ex_derive_ext with (2:=H1).
intros t; unfold ex_derive_onei, Derive_multii; f_equal.
apply fun_ext; intros y; f_equal.
unfold replaceF; apply extF; intros j.
case (ord_eq_dec _ _); easy.
now apply replaceF_correct_l.
Qed.

Lemma Derive_multii_powF_P : {n} (A:'nat^n) i m, C,
  Derive_multii i m (powF_P A)
     = (fun xC× powF_P (replaceF A (A i-m)%coq_nat i) x)
    (C = 0 (A i < m)%coq_nat).
Proof.
intros n A i; induction m.
1%R; split.
apply fun_ext; intros x; unfold Derive_multii, Derive_n; simpl.
rewrite Rmult_1_l; rewrite Nat.sub_0_r.
now rewrite replaceF_id replaceF_id.
split; intros H; contradict H; auto with arith.
destruct IHm as (C,(H1,H2)).
(C × INR (A i - m)%coq_nat); split.
unfold Derive_multii; unfold Derive_multii in H1.
apply fun_ext; intros x; simpl.
generalize (fun_ext_rev H1); intros H1'.
rewriteDerive_ext with
   (g:=fun zC × powF_P (replaceF A (A i - m)%coq_nat i) (replaceF x z i)).
rewrite Derive_scal.
rewrite Rmult_assoc; f_equal.
apply is_derive_unique.
eapply is_derive_ext'.
2: apply: is_derive_powF_P.
rewrite replaceF_correct_l; try easy; f_equal; try easy.
f_equal; unfold replaceF; apply extF; intros j.
case (ord_eq_dec _ _); try easy.
intros _; auto with zarith.
intros t; rewrite -H1'.
rewrite replaceF_correct_l; try easy.
f_equal; apply fun_ext; intros y; f_equal.
unfold replaceF; apply extF; intros j.
case (ord_eq_dec _ _); easy.
split; intros H3.
case (Rmult_integral _ _ H3); intros H4.
specialize (proj1 H2 H4); auto with arith.
case (Nat.le_gt_cases m.+1 (A i)); try easy.
intros H5; contradict H4; apply not_0_INR.
assert (1 A i -m)%coq_nat; auto with zarith arith.
apply PeanoNat.Nat.le_add_le_sub_l; auto with zarith.
replace (A i -m)%coq_nat with O; auto with zarith real.
Qed.

Lemma DeriveF_powF_P : {n} (alpha B :'nat^n), C,
  DeriveF alpha (powF_P B)
     = (fun xC× powF_P (fun i ⇒ (B i- alpha i)%coq_nat) x)
    (C = 0 brEF lt B alpha).
Proof.
intros n; induction n.
intros alpha B; 1; split.
rewrite DeriveF_nil; try easy.
apply fun_ext; intros x; rewrite Rmult_1_l.
unfold powF_P; rewrite 2!prod_R_nil; easy.
split; intros H.
contradict H; easy.
exfalso; destruct H as (i,Hi).
exfalso; apply I_0_is_empty; apply (inhabits i).
intros alpha B.
destruct (Derive_multii_powF_P B ord_max (alpha ord_max)) as
  (C1, (Y1,Z1)); fold (Derive_alp alpha ord_max) in Y1.
destruct (IHn (widenF_S alpha) (widenF_S B)) as (C2,(Y2,Z2)).
(C1×C2); split.
rewriteDeriveF_ind_r_scal_fun with
  (g1:= fun tC1 × t^(B ord_max - alpha ord_max))
  (g2:= fun tpowF_P (widenF_S B) (widenF_S t)).
apply fun_ext; intros x.
rewrite 2!Rmult_assoc; f_equal.
rewriteDeriveF_extf with (f2:=powF_P (widenF_S B)).
rewrite Y2.
rewrite Rmult_comm Rmult_assoc; f_equal.
unfold powF_P; rewrite prod_R_ind_r.
unfold plus; simpl; f_equal.
intros t; unfold narrow_ord_max, powF_P; 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 powF_P; 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'.
ord_max; apply Z1; easy.
destruct ((proj1 Z2) H') as (j,Hj).
(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 eq_sym, Z1; subst; easy.
replace C2 with 0; try ring.
apply eq_sym, Z2.
(narrow_S H').
unfold widenF_S; rewrite widen_narrow_S; easy.
Qed.

Lemma Derive_alp_scal :
   {n} (alpha : 'nat^n) i, f_scal_compat (Derive_alp alpha i).
Proof. move=>>; apply fun_ext; intro; apply Derive_n_scal_l. Qed.

Lemma DeriveF_part_scal :
   {n} (alpha : 'nat^n) j, f_scal_compat (DeriveF_part alpha j).
Proof. intros; apply comp_n_part_f_scal_compat, Derive_alp_scal. Qed.

Lemma DeriveF_zero : {n} (alpha:'nat^n),
     DeriveF alpha zero = zero.
Proof.
intros n; induction n.
intros alpha; unfold DeriveF.
rewrite comp_n_nil; easy.
intros alpha.
rewriteDeriveF_ind_r_scal_fun with (g1:=zero) (g2:=zero); try easy.
apply fun_ext; intros x.
rewrite fct_zero_eq; unfold mult, fct_zero, zero ; simpl.
rewrite Rmult_0_l; easy.
intros x; unfold Derive_alp, Derive_multii.
rewrite fct_zero_eq Rmult_0_l.
rewriteDerive_n_ext with (g:=fun _ ⇒ 0); try easy.
case (alpha ord_max); try easy.
intros m; apply Derive_n_const.
Qed.

Lemma DeriveF_scal : {n} (alpha:'nat^n) l f,
     DeriveF alpha (scal l f) = scal l (DeriveF alpha f).
Proof.
intros n alpha l f; unfold DeriveF.
apply comp_n_f_scal_compat.
intros i y g; unfold Derive_alp; apply fun_ext; intros x.
rewrite Derive_multii_scal; try easy.
Qed.

Lemma DeriveF_plus : {n} (alpha:'nat^n) f1 f2,
   is_Poly f1 is_Poly f2
     DeriveF alpha (f1+f2)%M = (DeriveF alpha f1 + DeriveF alpha f2)%M.
Proof.
intros n alpha f1 f2 H1 H2; unfold DeriveF.
assert (H: f_plus_compat_sub is_Poly (comp_n (Derive_alp alpha))).
2: apply H; easy.
apply comp_n_f_plus_compat_sub.
intros i g (g1,Hg1); unfold Derive_alp.
apply is_Poly_Derive_n_is_Poly; try easy.
intros i g1 g2 Hg1 Hg2.
unfold Derive_alp, Derive_multii.
apply fun_ext; intros x.
rewrite Derive_n_plus; try easy.
(mkposreal 1 Rlt_0_1); intros y Hy k Hk.
generalize (is_Poly_ex_derive_n g1 Hg1 i k (replaceF x y i)); unfold ex_derive_multii.
rewrite replaceF_correct_l; try easy.
intros T; apply: (ex_derive_n_ext _ (fun x0 : Rg1 (replaceF x x0 i))).
2: apply T.
intros t; simpl; unfold replaceF; f_equal; apply extF; intros i0.
case (ord_eq_dec i0 i); try easy.
(mkposreal 1 Rlt_0_1); intros y Hy k Hk.
generalize (is_Poly_ex_derive_n g2 Hg2 i k (replaceF x y i)); unfold ex_derive_multii.
rewrite replaceF_correct_l; try easy.
intros T; apply: (ex_derive_n_ext _ (fun x0 : Rg2 (replaceF x x0 i))).
2: apply T.
intros t; simpl; unfold replaceF; f_equal; apply extF; intros i0.
case (ord_eq_dec i0 i); try easy.
Qed.

Lemma DeriveF_lc_Poly : {n m} (alpha:'nat^n) f (L:'R^m),
   ( i, is_Poly (f i))
    DeriveF alpha (lin_comb L f) = lin_comb L (fun iDeriveF alpha (f i)).
Proof.
intros n m; induction m.
intros alpha f L H.
rewrite 2!lc_nil.
apply DeriveF_zero.
intros alpha f L H.
rewrite lc_ind_l.
rewrite DeriveF_plus.
rewrite DeriveF_scal.
rewrite IHm.
now rewrite lc_ind_l.
intros i; apply H; easy.
now apply is_Poly_scal.
apply is_Poly_lc.
intros i; unfold liftF_S; apply H.
Qed.

Lemma Monom_dk_lin_indep_aux1 : d k alpha i,
     alpha = Adk d k i
    DeriveF alpha (Monom_dk d k i) zero zero.
Proof.
intros d k alpha i H; rewrite H; unfold Monom_dk.
destruct (DeriveF_powF_P (Adk d k i) (Adk d k i)) as (C,(HC1,HC2)).
rewrite HC1.
rewrite powF_P_zero_compat_r.
rewrite Rmult_1_r; unfold zero; simpl.
intros T; apply HC2 in T; destruct T as (j,Hj).
contradict Hj; auto with arith.
apply extF; intros j; rewrite constF_correct; auto with arith.
Qed.

Lemma Monom_dk_lin_indep_aux2 : d k alpha i,
    alpha Adk d k i
    DeriveF alpha (Monom_dk d k i) zero = zero.
Proof.
intros d k alpha i H; unfold Monom_dk.
destruct (DeriveF_powF_P alpha (Adk d k i)) as (C,(HC1,HC2)).
rewrite HC1; unfold zero at 2; simpl.
apply nextF_rev in H; destruct H as (j,Hj); unfold neq in Hj.
apply not_eq in Hj; destruct Hj.
rewrite powF_P_zero_compat; try ring.
j; unfold powF, map2F.
unfold zero; simpl.
apply eq_sym, pow_i; auto with zarith.
rewrite (proj2 HC2); try ring.
now j.
Qed.

End Derive_Gen.

Section Pdk_Facts2.

Context {d : nat}.
Variable k : nat.

[RR9557v1] Lem 1523, p. 75.
Lemma Monom_dk_lin_indep : lin_indep (Monom_dk d k).
Proof.
intros L HL1; apply extF; intros ipl; rewrite zeroF.
assert (HL2 : DeriveF (Adk d k ipl) (lin_comb L (Monom_dk d k)) zero =
                DeriveF (Adk d k ipl) zero zero) by now f_equal.
rewrite DeriveF_zero fct_zero_eq DeriveF_lc_Poly in HL2;
    [| apply is_Poly_Monom_dk].
rewrite fct_lc_r_eq (lc_one_r ipl) in HL2.
destruct (is_integral_contra_R _ _ HL2) as [H | H]; [easy |].
contradict H; apply Monom_dk_lin_indep_aux1; easy.
apply extF; intros ipk; rewrite zeroF; unfold skipF.
apply Monom_dk_lin_indep_aux2.
move⇒ /Adk_inj; apply not_eq_sym, skip_ord_correct_m.
Qed.

Lemma Monom_dk_lin_gen : lin_gen (Pdk d k) (Monom_dk d k).
Proof. easy. Qed.

[RR9557v1] Lem 1524, pp. 75-76.
[RR9557v1] Lem 1525, p. 76.
Lemma Pdk_has_dim : has_dim (Pdk d k) ((pbinom d k).+1).
Proof. apply has_dim_lin_span, Monom_dk_lin_indep. Qed.

End Pdk_Facts2.