Library FEM.monomial
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free 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 a specific multiplicative big operator.
powF u a is the vector of the (u i)^(a i) for a vector u of reals
and a vector a of nat
powF_P L B is a real that is the product of all the (B i)^(L i).
Lemmas about zeros, compatibilities, replaceF are given.
From Requisite Require Import stdlib_wR ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Algebra Require Import Algebra_wDep.
Local Open Scope R_scope.
Section Prod_Def.
Context {d : nat}.
Definition powF (u : 'R^d) (a : 'nat^d) : 'R^d := map2F pow u a.
Lemma powF_correct : ∀ (u : 'R^d) (a : 'nat^d) i, powF u a i = u i ^ a i.
Proof. easy. Qed.
Definition powF_P (L : 'nat^d) (B : 'R^d) := prod_R (powF B L).
End Prod_Def.
Section powF_P_facts.
Lemma powF_zero_l :
∀ {d} (L : 'nat^d),
(∀ i, (0 < L i)%coq_nat) → powF (constF d 0) L = constF d 0.
Proof. intros; apply extF; intro; apply pow_i; easy. Qed.
Lemma powF_inF_zero_l :
∀ {d} (B : 'R^d) (L : 'nat^d),
(∀ i, (0 < L i)%coq_nat) → inF 0 B → inF 0 (powF B L).
Proof.
intros d B L HL HB; destruct HB as [i Hi]; ∃ i.
rewrite powF_correct -Hi pow_i; easy.
Qed.
Lemma powF_zero_compat_l :
∀ {d} (B : 'R^d) (L : 'nat^d),
(∀ i, (0 < L i)%coq_nat) → B = constF d 0 → powF B L = constF d 0.
Proof. intros d B L HL HB; rewrite HB; apply powF_zero_l; easy. Qed.
Lemma powF_zero_r : ∀ {d} (B : 'R^d), powF B (constF d 0%nat) = ones.
Proof. easy. Qed.
Lemma powF_zero_compat_r :
∀ {d} (B : 'R^d) (L : 'nat^d), L = constF d 0%nat → powF B L = ones.
Proof. intros; subst; easy. Qed.
Lemma powF_one_compat_r :
∀ {d} (B : 'R^d) (L : 'nat^d) i, L i = 1%nat → B i ^ L i = B i.
Proof. intros d B L i HL; rewrite HL; apply pow_1. Qed.
Lemma powF_castF :
∀ {d1 d2} (H : d1 = d2) (B : 'R^d1) (L : 'nat^d1),
powF (castF H B) (castF H L) = castF H (powF B L).
Proof. easy. Qed.
Lemma powF_concatF :
∀ {d1 d2} L1 L2 (B1 : 'R^d1) (B2 : 'R^d2),
powF (concatF B1 B2) (concatF L1 L2) = concatF (powF B1 L1) (powF B2 L2).
Proof. intros; apply map2F_concatF. Qed.
Lemma powF_skipF :
∀ {d} (B : 'R^d.+1) (L : 'nat^d.+1) i0,
powF (skipF B i0) (skipF L i0) = skipF (powF B L) i0.
Proof. intros; apply map2F_skipF. Qed.
Lemma powF_replaceF_l :
∀ {d} (B : 'R^d) u (L : 'nat^d) i,
powF (replaceF B u i) L = replaceF (powF B L) (u ^ L i) i.
Proof.
intros d B u L i; apply extF; intros j.
unfold powF; rewrite map2F_correct; destruct (ord_eq_dec j i) as [-> | H].
rewrite !replaceF_correct_l; easy.
rewrite !replaceF_correct_r; easy.
Qed.
Lemma powF_replaceF_r :
∀ {d} (B : 'R^d) (L : 'nat^d) a i,
powF B (replaceF L a i) = replaceF (powF B L) (B i ^ a) i.
Proof.
intros d B L a i; apply extF; intros j.
unfold powF; rewrite map2F_correct; destruct (ord_eq_dec j i) as [-> | H].
rewrite !replaceF_correct_l; easy.
rewrite !replaceF_correct_r; easy.
Qed.
Lemma powF_itemF_l :
∀ {d} (x : R) i0 (L : 'nat^d),
(∀ i, i ≠ i0 → (0 < L i)%coq_nat) →
powF (itemF d x i0) L = itemF d (x ^ L i0) i0.
Proof.
intros d x i0 L HL; apply extF; intros i; destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite Hi powF_correct !itemF_correct_l; easy.
rewrite powF_correct !itemF_correct_r; try apply pow_i, HL; easy.
Qed.
Lemma powF_itemF_r :
∀ {d} (B : 'R^d) (a : nat) i0,
powF B (itemF d a i0) = replaceF ones (B i0 ^ a) i0.
Proof.
intros d B a i0; apply extF; intros i; destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite → Hi, powF_correct, itemF_correct_l, replaceF_correct_l; easy.
rewrite → powF_correct, itemF_correct_r, replaceF_correct_r; easy.
Qed.
Lemma powF_P_eq_r :
∀ {d} (L M : 'nat^d) (B : 'R^d), L = M → powF_P L B = powF_P M B.
Proof. intros; rewrite H; easy. Qed.
Lemma powF_P_eq_l :
∀ {d} (L : 'nat^d) (B C : 'R^d), B = C → powF_P L B = powF_P L C.
Proof. intros; rewrite H; easy. Qed.
Lemma powF_P_ext :
∀ {d} (L M : 'nat^d) (B C : 'R^d),
(∀ i, L i = M i) → (∀ i, B i = C i) →
powF_P L B = powF_P M C.
Proof. intros; f_equal; apply extF; easy. Qed.
Lemma powF_P_compat :
∀ {d} (L M : 'nat^d) (B C : 'R^d),
powF B L = powF C M → powF_P L B = powF_P M C.
Proof. intros; unfold powF_P; rewrite H; easy. Qed.
Lemma powF_P_one_compat :
∀ {d} (L : 'nat^d) (B : 'R^d), powF B L = ones → powF_P L B = 1.
Proof. intros; apply prod_R_one_compat; easy. Qed.
Lemma powF_P_zero_compat :
∀ {d} (L : 'nat^d) (B : 'R^d), inF 0 (powF B L) → powF_P L B = 0.
Proof. intros; apply prod_R_zero; easy. Qed.
Lemma powF_P_zero_compat_r :
∀ {d} (L : 'nat^d) (B : 'R^d), L = constF d 0%nat → powF_P L B = 1.
Proof. intros; apply powF_P_one_compat, powF_zero_compat_r; easy. Qed.
Lemma powF_P_zero_compat_l :
∀ {d} (L : 'nat^d) (B : 'R^d),
inF 0 B → (∀ i : 'I_d, (0 < L i)%coq_nat) → powF_P L B = 0.
Proof. intros; apply powF_P_zero_compat, powF_inF_zero_l; easy. Qed.
Lemma powF_P_zero_ext_r :
∀ {d} (L : 'nat^d) (B : 'R^d),
(∀ i, L i = 0%nat) → powF_P L B = 1.
Proof. intros; apply powF_P_zero_compat_r, extF; easy. Qed.
Lemma powF_P_zero_ext_l :
∀ {d} (L : 'nat^d) (B : 'R^d),
(∃ i, B i = 0) → (∀ i : 'I_d, (0 < L i)%coq_nat) →
powF_P L B = 0.
Proof.
intros d B L [i Hi] HL; apply powF_P_zero_compat_l; [∃ i |]; easy.
Qed.
Lemma powF_P_one :
∀ {d} (L : 'nat^d) (B : 'R^d) (a : nat) (k : 'I_d),
L = itemF d a k →
powF_P L B = pow (B k) a.
Proof.
intros d B L a k HL; destruct d; [destruct k; easy |].
unfold powF_P; rewrite (prod_R_singl _ k).
rewrite HL powF_correct; f_equal; apply itemF_correct_l; easy.
rewrite -powF_skipF HL skipF_itemF_diag.
apply powF_zero_r.
Qed.
Lemma powF_P_castF :
∀ {d d'} (L : 'nat^d) (B : 'R^d) (H : d = d'),
powF_P (castF H L) (castF H B) = powF_P L B.
Proof. intros d d' B L H; unfold powF_P; rewrite -(prod_R_castF H); easy. Qed.
Lemma powF_P_concatF :
∀ {d1 d2} L1 L2 (B1 : 'R^d1) (B2 : 'R^d2),
powF_P (concatF L1 L2) (concatF B1 B2) = powF_P L1 B1 × powF_P L2 B2.
Proof. intros; unfold powF_P; rewrite powF_concatF prod_R_concatF; easy. Qed.
Lemma powF_P_replaceF_l :
∀ {d} (L : 'nat^d) (B : 'R^d) x i,
pow (B i) (L i) × powF_P (replaceF L x i) B = pow (B i) x × powF_P L B.
Proof.
intros d; case d; [intros L B x [i Hi]; easy |].
clear d; intros d L B x i; unfold powF_P, prod_R at 1.
rewrite powF_replaceF_r; replace (B i ^ L i) with (powF B L i) by easy.
replace (B i ^ x × _) with (B i ^ x × prod_R (powF B L))%Mmult by easy.
apply prod_R_replaceF.
Qed.
Lemma powF_P_replaceF_r :
∀ {d} (L : 'nat^d) (B : 'R^d) x i,
pow (B i) (L i) × powF_P L (replaceF B x i) = pow x (L i) × powF_P L B.
Proof.
intros d; case d; [intros L B x [i Hi]; easy |].
clear d; intros d L B x i; unfold powF_P, prod_R at 1.
rewrite powF_replaceF_l; replace (B i ^ L i) with (powF B L i) by easy.
replace (x ^ L i × _) with (x ^ L i × prod_R (powF B L))%Mmult by easy.
apply prod_R_replaceF.
Qed.
End powF_P_facts.