Library Algebra.Ring.Ring_kron
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.
Support for the Kronecker function on rings.
Let K : Ring.
This module may be used through the import of Algebra.Ring.Ring,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- kron K : nat → nat → K is the Kronecker delta function taking value 1 when both arguments are equal, and 0 otherwise;
- kronR : nat → nat → R is the specialization for real numbers.
Usage
From Requisite Require Import stdlib_wR ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group Ring_compl.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section Kron_Def.
Definition kron (K : Ring) (i j : nat) : K :=
match (Nat.eq_dec i j) with
| left _ ⇒ one
| right _ ⇒ zero
end.
Definition kronR := kron R_Ring.
End Kron_Def.
Section Kron_Facts.
Variable K : Ring.
Lemma kron_or : ∀ i j, kron K i j = 0 ∨ kron K i j = 1.
Proof.
intros i j; unfold kron; destruct (Nat.eq_dec i j); [right | left]; easy.
Qed.
Lemma kron_is_1 : ∀ i j, i = j → kron K i j = 1.
Proof.
intros i j; unfold kron; case (Nat.eq_dec i j); easy.
Qed.
Lemma kron_1 : ∀ i j, nonzero_struct K → kron K i j = 1 → i = j.
Proof.
intros i j HK; unfold kron; case (Nat.eq_dec i j); try easy.
intros _ H; contradict H; apply not_eq_sym, one_not_zero; easy.
Qed.
Lemma kron_in_equiv : ∀ i j, nonzero_struct K → kron K i j = 1 ↔ i = j.
Proof. intros; split; [apply kron_1; easy | apply kron_is_1]. Qed.
Lemma kron_is_0 : ∀ i j, i ≠ j → kron K i j = 0.
Proof.
intros i j; unfold kron; case (Nat.eq_dec i j); easy.
Qed.
Lemma kron_0 : ∀ i j, nonzero_struct K → kron K i j = 0 → i ≠ j.
Proof.
intros i j HK; unfold kron; case (Nat.eq_dec i j); try easy.
intros _ H; contradict H; apply one_not_zero; easy.
Qed.
Lemma kron_out_equiv :
∀ i j, nonzero_struct K → kron K i j = 0 ↔ i ≠ j.
Proof. intros; split; [apply kron_0; easy | apply kron_is_0]. Qed.
Lemma kron_sym : ∀ i j, kron K i j = kron K j i.
Proof.
intros i j; unfold kron at 2; destruct (Nat.eq_dec j i).
apply kron_is_1; easy.
apply kron_is_0; auto.
Qed.
Lemma kron_pred_eq :
∀ i j, (i ≠ 0)%nat → (j ≠ 0)%nat →
kron K (i - 1) (j - 1) = kron K i j.
Proof.
intros i j Hi Hj; destruct (Nat.eq_dec i j) as [H | H].
rewrite kron_is_1; try now rewrite kron_is_1.
rewrite H; easy.
rewrite kron_is_0; try now rewrite kron_is_0.
contradict H.
apply Nat.pred_inj; try easy.
rewrite -2!Nat.sub_1_r; easy.
Qed.
End Kron_Facts.
Section Kron_FF_Facts.
Properties with the second identity element of rings (one).
Context {K : Ring}.
Lemma itemF_kron_eq :
∀ {d} (x : K) i, itemF d x i = (fun j ⇒ x × kron K i j).
Proof.
intros d x i; apply extF; intros j.
destruct (ord_eq_dec j i) as [-> | Hj].
rewrite itemF_correct_l// kron_is_1// mult_one_r; easy.
rewrite itemF_correct_r// kron_is_0. rewrite mult_zero_r; easy.
apply ord_neq_compat, not_eq_sym; easy.
Qed.
Lemma kron_skipF_diag_l :
∀ {n} (i : 'I_n.+1), skipF (fun j : 'I_n.+1 ⇒ kron K i j) i = 0.
Proof.
intros n i; apply skipF_zero_compat; intros j Hj.
apply kron_is_0; contradict Hj; apply ord_inj; easy.
Qed.
Lemma kron_skipF_diag_r :
∀ {n} (j : 'I_n.+1), skipF (fun i : 'I_n.+1 ⇒ kron K i j) j = 0.
Proof.
intros n j; apply skipF_zero_compat; intros i Hi.
apply kron_is_0; contradict Hi; apply ord_inj; easy.
Qed.
Lemma sum_kron_l :
∀ {n p} (j : 'I_p),
(p ≤ n)%coq_nat → sum (fun i : 'I_n ⇒ kron K i j) = 1.
Proof.
intros [| n] p j.
move⇒ /Nat.le_0_r H; subst; destruct j; easy.
move⇒ /leP H; rewrite (sum_one _ (widen_ord H j));
[apply kron_is_1; easy | apply kron_skipF_diag_r].
Qed.
Lemma sum_kron_r :
∀ {n p} (i : 'I_p),
(p ≤ n)%coq_nat → sum (fun j : 'I_n ⇒ kron K i j) = 1.
Proof.
intros [| n] p i.
move⇒ /Nat.le_0_r H; subst; destruct i; easy.
move⇒ /leP H; rewrite (sum_one _ (widen_ord H i));
[apply kron_is_1 | rewrite (kron_skipF_diag_l (widen_ord _ _))]; easy.
Qed.
End Kron_FF_Facts.
Local Open Scope R_scope.
Section Kron_R_Def.
Definition multi_kronR {n : nat} (alpha beta : 'nat^n) : R :=
prod_R (map2F kronR alpha beta).
End Kron_R_Def.
Section Kron_R_Facts.
Lemma kronR_or : ∀ i j, kronR i j = 0 ∨ kronR i j = 1.
Proof. apply kron_or. Qed.
Lemma kronR_bound : ∀ i j, 0 ≤ kronR i j ≤ 1.
Proof.
intros i j; destruct (kronR_or i j) as [H | H]; rewrite H; Lra.lra.
Qed.
Lemma kronR_is_1 : ∀ i j, i = j → kronR i j = 1.
Proof. apply kron_is_1. Qed.
Lemma kronR_1 : ∀ i j, kronR i j = 1 → i = j.
Proof. move=>>; apply kron_1, nonzero_struct_R. Qed.
Lemma kronR_in_equiv : ∀ i j, kronR i j = 1 ↔ i = j.
Proof. move=>>; apply kron_in_equiv, nonzero_struct_R. Qed.
Lemma kronR_is_0 : ∀ i j, i ≠ j → kronR i j = 0.
Proof. apply kron_is_0. Qed.
Lemma kronR_0 : ∀ i j, kronR i j = 0 → i ≠ j.
Proof. move=>>; apply kron_0, nonzero_struct_R. Qed.
Lemma kronR_out_equiv : ∀ i j, kronR i j = 0 ↔ i ≠ j.
Proof. move=>>; apply kron_out_equiv, nonzero_struct_R. Qed.
Lemma kronR_sym : ∀ i j, kronR i j = kronR j i.
Proof. apply kron_sym. Qed.
Lemma kronR_pred_eq :
∀ i j, (i ≠ 0)%nat → (j ≠ 0)%nat →
kronR (i - 1) (j - 1) = kronR i j.
Proof. apply kron_pred_eq. Qed.
Lemma itemF_kronR_eq :
∀ {d} (x : R) i, itemF d x i = (fun j ⇒ x × kronR i j).
Proof. intros; apply: itemF_kron_eq. Qed.
Lemma kronR_skipF_diag_l :
∀ {n} (i : 'I_n.+1), skipF (kronR i) i = 0%M.
Proof. intros; apply kron_skipF_diag_l. Qed.
Lemma kronR_skipF_diag_r :
∀ {n} (j : 'I_n.+1), skipF (fun i : 'I_n.+1 ⇒ kronR i j) j = 0%M.
Proof. intros; apply kron_skipF_diag_r. Qed.
Lemma sum_kronR_l :
∀ {n p} (j : 'I_p),
(p ≤ n)%coq_nat → sum (fun i : 'I_n ⇒ kronR i j) = 1.
Proof. move=>>; apply: sum_kron_l. Qed.
Lemma sum_kronR_r :
∀ {n p} (i : 'I_p),
(p ≤ n)%coq_nat → sum (fun j : 'I_n ⇒ kronR i j) = 1.
Proof. move=>>; apply: sum_kron_r. Qed.
End Kron_R_Facts.