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.
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}:
For simplices (P1 in dim d), with x = (x_i)_{i=1..d}:
[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.
Description
- 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.
- Pd1 = lin_span (1, x_1, ..., x_d) = lin_span LagPd1_ref,
- p = lin_comb L x \in Pd1.
Bibliography
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.
[RR9557v1]
Def 1505, p. 72.
[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 k ⇒ sub_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 x ⇒ x (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 ipk ⇒ powF_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 x ⇒ p0 (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 x ⇒ p0 (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 x ⇒ p0 (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 x ⇒ p0 (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 x ⇒ x i × p x).
Proof.
intros d k p i H; inversion H as [L HL].
apply Pdk_ext with
(lin_comb L (fun j x ⇒ x 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 x ⇒ p (widenF_S x)).
Proof.
intros d k p H; inversion H.
apply Pdk_ext with
(lin_comb L (fun i x ⇒ Monom_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 x ⇒ x ord_max × (p1 (widenF_S x) × q2 x + p2 x × q1 (widenF_S x)))
+ (fun x ⇒ x 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 x ⇒ prod_R (fun i ⇒ p 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 x ⇒ prod_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 x ⇒ pow (f x l) m).
Proof.
intros d n f l m Hf.
apply Pdk_ext with (fun x ⇒ prod_R (fun i:'I_m ⇒ f 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.
Proof. intros; apply lin_span_cms. Qed.
Definition Pdk_ms := fun d k ⇒ sub_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 x ⇒ x (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 ipk ⇒ powF_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 x ⇒ p0 (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 x ⇒ p0 (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 x ⇒ p0 (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 x ⇒ p0 (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 x ⇒ x i × p x).
Proof.
intros d k p i H; inversion H as [L HL].
apply Pdk_ext with
(lin_comb L (fun j x ⇒ x 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 x ⇒ p (widenF_S x)).
Proof.
intros d k p H; inversion H.
apply Pdk_ext with
(lin_comb L (fun i x ⇒ Monom_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 x ⇒ x ord_max × (p1 (widenF_S x) × q2 x + p2 x × q1 (widenF_S x)))
+ (fun x ⇒ x 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 x ⇒ prod_R (fun i ⇒ p 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 x ⇒ prod_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 x ⇒ pow (f x l) m).
Proof.
intros d n f l m Hf.
apply Pdk_ext with (fun x ⇒ prod_R (fun i:'I_m ⇒ f 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 → (R→R)) (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:R→R) ⇒ ∀ 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 → (R→R)) (L:'R^n) (d :'I_n → (R→R)),
(∀ 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 y ⇒ f (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 y ⇒ f (replaceF x y i)) (x i) l.
Definition Derive_onei {n} :=
fun (i:'I_n) (f: 'R^n → R) (x:'R^n) ⇒
Derive (fun y ⇒ f (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 y ⇒ f (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 y ⇒ f (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 y ⇒ f (replaceF x y i)) j (x i).
Lemma ex_derive_onei_lc :
∀ {n m} (j:'I_n) (f :'I_m → ('R^n→R)) (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^n→R)) (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 y ⇒ d 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^n→R) 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^n→R) → ('R^n→R))^n :=
fun i ⇒ Derive_multii i (alpha i).
Definition DeriveF_part {n} (alpha : 'nat^n) (j:'I_n.+1) : ('R^n→R) → ('R^n→R) :=
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^n→R) → ('R^n→R) :=
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 x ⇒ f1 x× f2 x)
= (fun x ⇒ f1 x*(Derive_multii i j f2 x)).
Proof.
intros n i j f1 f2 H1.
apply fun_ext; intros x; unfold Derive_multii.
rewrite →Derive_n_ext with (g:=fun y ⇒ f1 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.+1→R) 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: i≠ord_max) (g1:R→R) (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.+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.
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:R→R) (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 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.
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_n ⇒ powF 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 x ⇒ C× 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'.
rewrite →Derive_ext with
(g:=fun z ⇒ C × 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 x ⇒ C× 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.
rewrite →DeriveF_ind_r_scal_fun with
(g1:= fun t ⇒ C1 × t^(B ord_max - alpha ord_max))
(g2:= fun t ⇒ powF_P (widenF_S B) (widenF_S t)).
apply fun_ext; intros x.
rewrite 2!Rmult_assoc; f_equal.
rewrite →DeriveF_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.
rewrite →DeriveF_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.
rewrite →Derive_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 : R ⇒ g1 (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 : R ⇒ g2 (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 i ⇒ DeriveF 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.
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.
Lemma Monom_dk_basis : basis (Pdk d k) (Monom_dk d k).
Proof. apply basis_lin_span_equiv, Monom_dk_lin_indep. Qed.
Proof. apply basis_lin_span_equiv, Monom_dk_lin_indep. Qed.
[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.
Proof. apply has_dim_lin_span, Monom_dk_lin_indep. Qed.
End Pdk_Facts2.