Add LoadPath "./interval". Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype finfun finset ssralg matrix bigops perm. Require Import Reals. Require Import Fourier. Require Import ClassicalChoice. Require Import Rstruct min_max. (* - specific definitions for real matrices: absolute value, order component wise; - definition for a canonical norm structure - properites of the norm - definition for limit and convergence of matrix series - componentwise - properties for limit, convergence ... - link between norm and determinant *) Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. Open Scope R_scope. Open Local Scope ring_scope. Delimit Scope R_scope with Re. Delimit Scope ring_scope with Ri. Import GRing.Theory. Section matRDef. Variable p q: nat. (*Definitions for absolute value of a matrix and componentwise order *) Definition Mabs (A: 'M_(p, q)) := map_mx Rabs A. (*Definition Mabs (A: 'M_(p, q)) := \matrix_(i, j) Rabs (A i j).*) Definition Mle (A B: 'M_(p, q)) := forall i j, A i j <= B i j. Definition Mlt (A B: 'M_(p, q)) := forall i j, A i j < B i j. Definition one_M: matrix R p q := \matrix_(i, j) 1. End matRDef. Implicit Arguments one_M[p q]. Infix " exists i, exists j, A i j != B i j. Proof. move=> A B; move/eqP=> Hab. have H: ~ forall i j, A i j = B i j. by move=> H1; apply: Hab; apply/matrixP. elim (not_all_ex_not _ _ H) => i H2. exists i. elim (not_all_ex_not _ _ H2) => j H3. exists j. by apply/eqP. Qed. Lemma Mabs_pos: forall (a: 'M_(p, q)), 0 <=m: Mabs a. move=> a=> i j; rewrite !mxE; apply Rabs_pos. Qed. Lemma Mabs_triang: forall (u v: 'M_(p,q)), (Mabs (u + v)) <=m: (Mabs u + Mabs v). Proof. move=> u v i k; rewrite !mxE; apply Rabs_triang. Qed. Lemma Mle_trans: forall (u v w: 'M_(p, q)), u <=m: v -> v <=m: w -> u <=m: w. move=> u v w Huv Hvw i j; apply Rle_trans with (v i j); [apply Huv| apply Hvw]. Qed. Lemma Madd_mle_compat: forall (a b c d: 'M_(p,q)), Mle a b -> Mle c d -> Mle (a + c) (b + d). move=> a b c d Hab Hcd i k; rewrite !mxE. apply Rplus_le_compat; [apply Hab| apply Hcd]. Qed. Lemma Mabs_mul: forall (m: 'M_(n, p)) (v:'M_(p, q) ), Mabs (m *m v) <=m: (Mabs m) *m (Mabs v). Proof. move=> m v i k; rewrite !mxE. have H:= @abs_sum_le_sum_abs p (fun j => m i j * v j k ). apply Rle_trans with (1:= H). by right; apply eq_bigr => j _; rewrite /Mabs !mxE Rabs_mult. Qed. Lemma Mabs_scalemx: forall a (m: 'M_(n, p)), Mabs (a *m: m) = Rabs a *m: Mabs m. by move=> a m ; rewrite -matrixP=> i j; rewrite !mxE Rabs_mult. Qed. Lemma Mmul_mle_compat_l: forall (a: 'M_(n,p)) (u v: 'M_(p, q)), u <=m: v -> Mle 0 a -> a *m u <=m: a *m v. move=> a u v Huv Ha i k; rewrite !mxE. apply: big_rel; [by right|apply Rplus_le_compat |]. move=> j _; apply Rmult_le_compat_l; last by apply Huv. by move : (Ha i j); rewrite mxE. Qed. Lemma Mmul_mle_compat_r: forall (a: 'M_(q,n)) (u v: 'M_(p, q)), u <=m: v -> Mle 0 a -> u *m a <=m: v *m a. move=> a u v Huv Ha i k; rewrite !mxE. apply: big_rel; [by right|apply Rplus_le_compat |]. move=> j _; apply Rmult_le_compat_r; last by apply Huv. by move : (Ha j k); rewrite mxE. Qed. Lemma Mmul_mle_compat: forall (a b: 'M_(q,n)) (u v: 'M_(p, q)), u <=m: v -> a <=m: b -> Mle 0 a -> Mle 0 u -> u *m a <=m: v *m b. move=> a b u v Huv Hab Ha Hu i k; rewrite !mxE. apply: big_rel; [by right|apply Rplus_le_compat |]. move=> j _; apply Rmult_le_compat; [| |apply Huv | apply Hab]. by move : (Hu i j); rewrite mxE. by move : (Ha j k); rewrite mxE. Qed. (* Lemma Mlt_not_mle: forall (a b: 'M_(q,n)), a <=m: b <-> ~ b a b; split => H. *) End matRProp. Section normDef. Structure can_norm : Type := MNorm { anorm : forall p q, matrix R p q -> R; pos_norm : forall p q (A: 'M_(p, q)), R0 <= anorm A; hom_pos_norm : forall p q (A: 'M_(p, q)) (r:R), anorm (r *m: A) = Rabs r * anorm A; trin_ineq_norm : forall p q (A B: 'M_(p, q)), anorm (A + B) <= anorm A + anorm B; prod_ineq_norm: forall p q r (A: 'M_(p, q)) (B: matrix _ q r), anorm (A *m B) <= anorm A * anorm B; canonical_norm: forall p q (A: 'M_(p, q) ) i j, Rabs (A i j) <= anorm A; canonical_norm2: forall p q (A B: 'M_(p, q)), (forall i j, Rabs (A i j) <= Rabs (B i j)) ->anorm A <= anorm B }. (*Coercion anorm : can_norm >-> Funclass.*) End normDef. Implicit Arguments anorm[p q]. Notation "|| A : N |" := (anorm N A) (at level 0, A, N at level 99, format "|| A : N |") : R_scope. Section normProp. Variable p q: nat. Variable mynorm: can_norm. Lemma mynorm0: || (0: 'M_(p, q)) : mynorm | = 0. Proof. have H1: || (0: 'M_(p, q)) : mynorm | = || (2 *m: (0: 'M_(p, q))) : mynorm |. by rewrite scalemx0. rewrite hom_pos_norm in H1. case (Req_dec (||(0: 'M_(p, q)) : mynorm|) 0) => H2;[done|]. have Hr: Rabs 2 = 1. rewrite -> Rmult_comm in H1. rewrite -{1}(Rmult_1_r (||(0: 'M_(p, q)) : mynorm|)) in H1. by apply Rmult_eq_reg_l with (||(0: 'M_(p, q)) : mynorm|) . have Hr2: Rabs 2 <> R1. rewrite Rabs_right; [apply Rgt_not_eq|]; fourier. by case Hr2. Qed. Lemma norm_pos_st: forall (A: 'M_(p, q) ), A != 0 -> 0 < ||A : mynorm |. Proof. move=> A HA. elim (Rmat_neq HA) => i [j Hneq]. apply Rlt_le_trans with (Rabs (A i j)). by apply Rabs_pos_lt; apply/eqP; rewrite mxE in Hneq. apply canonical_norm. Qed. Lemma RabsM_ineq: forall (A: 'M_(p, q)) eps, 0 <= eps -> (forall i j, Rabs (A i j) < eps) -> || A : mynorm | <= eps * || (one_M:'M_(p, q)) : mynorm |. Proof. move=> A e He H. have H1: forall i j, Rabs (A i j) < (e *m: one_M) i j. move=> i j; rewrite !mxE; rewrite -> Rmult_1_r; apply H. have Hepos: forall (i:'I_p) (j:'I_q), Rabs ((e *m: one_M) i j) = (e *m: one_M) i j. move=> i j; rewrite !mxE; rewrite -> Rabs_right; first by done. apply Rle_ge; apply Rle_trans with (Rabs (A i j)) ; [apply Rabs_pos| left; rewrite -> Rmult_1_r; apply H] . apply Rle_trans with (|| (e *m: one_M) : mynorm|). apply canonical_norm2. move=> i j; rewrite Hepos; left; apply H1. rewrite -{2}(Rabs_right e). right; apply hom_pos_norm. by apply Rle_ge. Qed. Import GRing.Theory. Lemma tri_minus_norm: forall (a b: 'M_(p, q)), || a : mynorm | - || b: mynorm | <= || (a - b)%Ri : mynorm |. Proof. move=> a b. apply (Rplus_le_reg_l (||b :mynorm |)). ring_simplify. pattern a at 1; replace a with (b +( a - b))%Ri. apply: trin_ineq_norm. rewrite addrCA addrA. by rewrite addrK. Qed. Lemma eq_norm_min: forall (a b: 'M_(p, q)), || (a - b)%Ri : mynorm | = || (b - a)%Ri : mynorm |. Proof. move=> a b. replace (a - b)%Ri with (-1 *m: (b - a)%Ri). by rewrite hom_pos_norm Rabs_Ropp Rabs_R1; toR; rewrite Rmult_1_l. toR; apply/matrixP=> i j; rewrite !mxE ; toR; ring. Qed. Lemma tri_min2: forall (a b: 'M_(p, q)), Rabs ( ||a : mynorm| - ||b : mynorm|) <= || (a - b)%Ri : mynorm |. Proof. move=> a b. rewrite /Rabs; case (Rcase_abs (|| a : mynorm | - || b : mynorm |) )=> H; [|apply tri_minus_norm] . rewrite Ropp_minus_distr eq_norm_min; apply tri_minus_norm. Qed. Lemma mat_norm_sum: forall (A : nat -> 'M_(p, q)) n, || (\sum_(i < n.+1) A i) : mynorm | <= \sum_(i < n.+1) || A i : mynorm |. Proof. move=> A n. apply: big_morph_rel. by move=> x; right. by move=> *; apply Rplus_le_compat. by move=>b *; apply Rle_trans with b. apply mynorm0. by move=> a v; apply: trin_ineq_norm. Qed. End normProp. Section limitMatDef. Variable p q: nat. Definition limit_m (An: nat -> 'M_(p, q)) (La: 'M_(p, q)):= forall i j, Un_cv (fun n => An n i j) (La i j). Definition cv_mat_ser (Ak:nat->'M_(p, q)) (A:'M_(p, q)) := forall i j, Un_cv (fun N => sum_f_R0 (fun n => Ak n i j) N) (A i j). Definition cv_mat_ser2 (Ak:nat->'M_(p, q)) (A: 'M_(p, q)) := limit_m (fun N => \sum_(iR) (a l:R), (forall n, a<=un n)-> Un_cv un l -> a<=l. Proof. intros. cut (~(l0). toR; fourier. assert (Hcon: exists N, forall n, (n>=N)%coq_nat ->R_dist (un n) l R) (x y:R), (forall n, xn n<= yn n)-> (Un_cv xn x)-> (Un_cv yn y)-> x<=y. intros. assert (0<=y-x). assert (forall n, 0<=yn n- xn n). intros. elim (H n);intros; toR; fourier. assert (Un_cv (fun i:nat => yn i - xn i) (y - x)). toR; apply: CV_minus; assumption. apply lim_conv_low with (fun i:nat => yn i - xn i); assumption. rewrite /GRing.zero //= in H2; fourier. Qed. Lemma el_eq_seq_eq: forall xn yn x , (forall n, xn n = yn n )-> Un_cv xn x-> Un_cv yn x. Proof. by move=> xn yn x Heq Hcv eps He; elim (Hcv eps He) => N HN; exists N=> n Hn; rewrite -Heq; apply HN. Qed. Lemma el_eq_mat_seq_cv: forall xn yn (x: 'M_(p, q)), (forall n, xn n = yn n) -> limit_m xn x -> limit_m yn x. Proof. move=> xn yn x Hxy Hx i j. apply el_eq_seq_eq with (fun n => xn n i j). by move=> n; rewrite Hxy. apply Hx. Qed. Lemma echiv_mat_ser: forall Ak (A: 'M_(p, q)), cv_mat_ser Ak A <-> cv_mat_ser2 Ak A. Proof. move=> Ak A; split=> H i j; have H1:= H i j. have H2: forall N, sum_f_R0 (fun k : nat => Ak k i j) N = (\sum_(i0 < N.+1) Ak i0) i j. move=> N; rewrite echiv_sums. elim: index_enum. by rewrite !big_nil !mxE. by move => k s Ih; rewrite !big_cons Ih !mxE. apply (@el_eq_seq_eq _ _ _ H2 H1). have H2: forall N, (\sum_(i0 < N.+1) Ak i0) i j =sum_f_R0 (fun k : nat => Ak k i j) N . move=> N; rewrite echiv_sums. elim: index_enum. by rewrite !big_nil !mxE. by move => k s Ih; rewrite !big_cons !mxE Ih. apply (@el_eq_seq_eq _ _ _ H2 H1). Qed. Lemma limit_m_mul: forall (A: nat -> 'M_(p, q)) (R: 'M_(r, p)) (S: 'M_(p, q)), limit_m A S -> limit_m (fun n => R *m (A n))%Ri (R *m S)%Ri. Proof. move=> A R S Hl i j eps He. red in Hl; red in Hl. have Hl1: forall eps, eps > R0 -> forall i j, exists N : nat, forall n : nat, (n >= N)%coq_nat -> R_dist (A n i j) (S i j) < eps. by move=>*; apply Hl. have H0 : R0 <= \big[Rmax/R0]_j Rabs (R i j) . elim: index_enum; [by rewrite big_nil; right|]. move=> t s IH; rewrite big_cons. by apply Rmax_ge; [apply Rabs_pos|]. case H0 => H. have Hp: (0 \big[Rmax/0]_(i f Hp; move: f; rewrite Hp; apply big_ord0. have HR := hbig0 (fun j => Rabs (R i j)). case Cp: (p == O). move/eqP: Cp => Cp. have Hcp:= HR Cp. rewrite Hcp in H. elim (Rlt_irrefl _ H). move/eqP: Cp => Cp; omega. have H01: 0 < \big[Rmax/R0]_i \big[Rmax/0]_j Rabs (R i j). apply Rlt_le_trans with (\big[Rmax/0]_j Rabs (R i j)); [done|]. apply (@max_max r (fun i0 =>\big[Rmax/0]_j0 Rabs (R i0 j0))) => i0. elim: index_enum; [by rewrite big_nil; right|]. move=> t s IH; rewrite big_cons. by apply Rmax_ge; [apply Rabs_pos|]. have H1: (eps / (\big[Rmax/0]_i \big[Rmax/R0]_i0 Rabs (R i i0))) /INR p > 0. rewrite /Rdiv; apply Rmult_gt_0_compat. apply Rmult_gt_0_compat; [done|by apply: Rinv_0_lt_compat] . apply: Rinv_0_lt_compat; apply: lt_INR_0. done. have Hl2:= (Hl1 ((eps/(\big[Rmax/R0]_i \big[Rmax/R0]_i0 (Rabs (R i i0))))/INR p)%R H1). have Hc1: forall i , exists c1: 'I_q -> nat, forall j n, (n >= (c1 j))%coq_nat -> R_dist (A n i j) (S i j) < eps / \big[Rmax/0]_i0 \big[Rmax/0]_i1 Rabs (R i0 i1) / INR p. move=> i0; apply (choice _ (Hl2 i0)). case (choice _ Hc1) => ch Hch. exists ( \max_(i n Hn. rewrite !mxE /R_dist. apply Rle_lt_trans with (Rabs (\sum_j0 (R i j0 * A n j0 j)%Ri - \sum_j0 (R i j0 * S j0 j)%Ri)%Ri). right; f_equal. rewrite -GRing.sumr_sub. apply Rle_lt_trans with (Rabs (\sum_i0 (R i i0 * (A n i0 j - S i0 j)%Ri))). right; f_equal; apply eq_bigr => i0 _; toR; ring. apply Rle_lt_trans with (\sum_i0 Rabs (R i i0 * (A n i0 j - S i0 j)%Ri)). rewrite //=; apply abs_sum_le_sum_abs with (f:= (fun i0 => R i i0 * (A n i0 j - S i0 j))) . apply Rle_lt_trans with (\sum_i0 (\big[Rmax/0]_i0 Rabs (R i i0) * Rabs (A n i0 j - S i0 j)%Ri)). apply (sum_le_f_le) => i0. rewrite Rabs_mult. apply Rmult_le_compat. apply Rabs_pos . apply Rabs_pos. apply (@max_max p (fun j=> Rabs (R i j)))=> i1; apply Rabs_pos. by right. rewrite -big_distrr //= GRing.mulrC. replace eps with ( (eps / \big[Rmax/0]_i0 Rabs (R i i0)) * \big[Rmax/0]_(i0 < p) Rabs (R i i0) )%R. apply Rmult_lt_compat_r . done. apply: (ineq_sum_el ). by move/leP: Hp. left; apply: Rmult_gt_0_compat; [done|by apply: Rinv_0_lt_compat] . move=> x. apply Rlt_le_trans with (eps / \big[Rmax/0]_i0 \big[Rmax/0]_i1 Rabs (R i0 i1) / INR p)%R. rewrite /R_dist in Hch. toR; apply: Hch. apply: (le_trans _ (\max_(i < p) \max_(j < q) ch i j)%nat _);[|apply Hn]. apply le_trans with (\max_(j0 < q) ch x j0 ). apply/leP; apply (@leq_bigmax (ordinal_finType q) (fun j0 => ch x j0) j ). apply/leP; apply (@leq_bigmax _ (fun i0 =>\max_(j0 < q) ch i0 j0) ) . apply: Rmult_le_compat_r. by left; apply: Rinv_0_lt_compat; apply lt_INR_0. apply: Rmult_le_compat_l; [by left|]. apply Rle_Rinv; try done. apply (@max_max r (fun i0 => \big[Rmax/0]_i1 Rabs (R i0 i1))) => i0. have Hp1: (0 Rabs (R i0 j)))=> i1; [apply Rabs_pos| move=> Hx; rewrite Hx; apply Rabs_pos]. toR; rewrite /Rdiv Rmult_assoc Rinv_l; [ring|]. by apply Rgt_not_eq. exists O => n Hn. rewrite !mxE /R_dist. apply Rle_lt_trans with (Rabs (\sum_j0 (R i j0 * A n j0 j)%Ri - \sum_j0 (R i j0 * S j0 j)%Ri)%Ri). right; f_equal. rewrite -GRing.sumr_sub. apply Rle_lt_trans with (Rabs (\sum_i0 (R i i0 * (A n i0 j - S i0 j)%Ri))). right; f_equal; apply eq_bigr => i0 _; toR; ring. apply Rle_lt_trans with (\sum_i0 Rabs (R i i0 * (A n i0 j - S i0 j)%Ri)). rewrite //=; apply abs_sum_le_sum_abs with (f:= (fun i0 => R i i0 * (A n i0 j - S i0 j))) . apply Rle_lt_trans with (\sum_i0 (\big[Rmax/0]_i0 Rabs (R i i0) * Rabs (A n i0 j - S i0 j)%Ri)). apply (sum_le_f_le ) => i0. rewrite Rabs_mult. apply Rmult_le_compat. apply Rabs_pos . apply Rabs_pos. apply (@max_max p (fun j=> Rabs (R i j)))=> i1; apply Rabs_pos. by right. rewrite -big_distrr //= GRing.mulrC. by rewrite -H GRing.mulr0. Qed. Lemma limit_m_add: forall A B (x y: 'M_(p, q)), limit_m A x -> limit_m B y -> limit_m (fun n => A n + B n) (x + y). Proof. move=> a b x y Ha Hb i j. rewrite !mxE. apply el_eq_seq_eq with (fun n => a n i j + b n i j); [by move=> n; rewrite mxE |]. apply CV_plus;[apply Ha|apply Hb]. Qed. Lemma limit_m_opp_0: forall (a: nat -> 'M_(p,q)) , limit_m a 0 -> limit_m (fun n=> (- a n)%Ri) 0. Proof. move=> a Hcv. move=> i j eps He; case (Hcv i j eps He) => N HN; exists N => n Hn. have HN1 := HN n Hn. rewrite !mxE /R_dist !Rminus_0_r in HN1 |- *. by toR; rewrite Rabs_Ropp. Qed. Lemma limit_m_Sn: forall a (x: 'M_(p, q)), limit_m a x -> limit_m (fun n => a (n.+1)) x. Proof. move=> a x Hcv i j eps He ; case (Hcv i j eps He) => N HN; exists (N.+1) => n Hn; apply HN; omega. Qed. Lemma limit_m_uniq: forall a (x y: 'M_(p, q)), limit_m a x -> limit_m a y -> x = y. Proof. move=> a x y Hx Hy; apply/ matrixP => i j. red in Hx. by apply UL_sequence with (fun n => a n i j) . Qed. Lemma th1_246: forall Ak, (exists S:'M_(p,q), cv_mat_ser2 Ak S) -> limit_m Ak 0. Proof. move=> Ak [S Hcv]. move: Hcv; rewrite -echiv_mat_ser => Hcv. move=> i j eps He. have Hc2:= Hcv i j. have Hcau: Cauchy_crit (fun N : nat => sum_f_R0 (fun n : nat => Ak n i j) N). by apply CV_Cauchy; exists (S i j). elim (Hcau eps He) => N HN. exists (N.+1)%nat => n Hn. have H1: (minus n 1 >=N)%coq_nat; [omega|]. have H2: ((minus n 1).+1 >= N)%coq_nat;[omega|]. have HN2:= HN _ _ H1 H2. rewrite /R_dist //= Rabs_minus_sym Rplus_comm /Rminus Rplus_assoc Rplus_opp_r Rplus_0_r in HN2. rewrite /R_dist mxE Rminus_0_r. replace n with ((minus n 1).+1);[done|omega]. Qed. Lemma lem_cv1: forall (Ak: nat -> 'M_(p, q)) (A: 'M_(p, q)), limit_m Ak A <-> Un_cv (fun k => || (A - (Ak k)) : mynorm |) R0. Proof. move=> Ak A; split; move=> H. red in H; red in H. have H1: forall eps, eps>0->forall i j, exists N : nat, forall n : nat, (n >= N)%coq_nat -> R_dist (Ak n i j) (A i j) < eps. by move=>*; apply H. have H2: forall eps, eps>0 -> forall i , exists c2: 'I_q->nat, forall j, forall n : nat, (n >= (c2 j))%coq_nat -> R_dist (Ak n i j) (A i j) < eps. move=> eps He i; apply choice with (A:= 'I_q) (B:= nat) (R:=fun j N => forall n : nat, (n >= N)%coq_nat -> R_dist (Ak n i j) (A i j) < eps). by move=> *; apply H1. have H3: forall eps, eps>0-> exists c1: 'I_p->'I_q->nat, forall i j n, (n >= (c1 i j))%coq_nat -> R_dist (Ak n i j) (A i j) < eps. move=> eps He ; apply (choice _ (H2 eps He)). move=> eps He /=. elim (Req_dec (||@one_M p q :mynorm|) R0) => Hdec. elim (H3 eps He)=> ch Hch. exists (\max_(i n Hn. apply Rle_lt_trans with R0. rewrite /R_dist Rminus_0_r Rabs_right. replace R0 with (eps * ||@one_M p q:mynorm|). apply RabsM_ineq; [left; apply: He|]. move=> i j; rewrite !mxE Rabs_minus_sym. apply:Hch. rewrite /ge; apply le_trans with (\max_(i < p) \max_(j < q) ch i j)%nat. apply le_trans with (\max_(j < q) ch i j)%nat. apply/leP. apply: leq_bigmax. apply/leP. apply (@leq_bigmax _ (fun i => \max_(j0 < q) ch i j0 ) i). omega. rewrite Hdec. by rewrite -> Rmult_0_r. apply Rle_ge; apply: pos_norm. done. have Hen: (1/2* eps / ||@one_M p q:mynorm|)%Ri > 0. apply: Rmult_gt_0_compat. apply Rmult_gt_0_compat; rewrite /GRing.mul /GRing.inv //= /Rinvx . have t2: 2!= 0. apply /eqP; rewrite /GRing.zero //=; apply Rgt_not_eq; fourier. rewrite t2; rewrite /GRing.mul /GRing.inv /GRing.one /GRing.zero //=; fourier. elim (pos_norm mynorm (@one_M p q)) => Hen2. rewrite /GRing.inv /=. case cn: (||@one_M p q : mynorm| == 0); rewrite /Rinvx cn //=. by apply Rinv_0_lt_compat. by elim Hdec. elim (H3 (1/2*eps/(||one_M : mynorm |)) Hen)=> ch Hch. exists (\max_(i n Hn. rewrite /R_dist Rminus_0_r Rabs_right;[|apply Rle_ge; apply:pos_norm]. apply Rle_lt_trans with ((1/2*eps/ || (@one_M p q) : mynorm|) * || (@one_M p q) : mynorm|). have Hrd: forall i j, Rabs (Ak n i j - A i j) < (1 / 2 * eps / || @one_M p q : mynorm |)%Ri. move => i j ; apply:Hch. rewrite /ge; apply le_trans with (\max_(i < p) \max_(j < q) ch i j)%nat. apply le_trans with (\max_(j < q) ch i j)%nat. apply/leP; apply: leq_bigmax. apply/leP; apply: (@leq_bigmax _ (fun i => \max_(j0 < q) ch i j0 ) i). omega. apply RabsM_ineq. by left; apply Rgt_lt. by move=> i j; rewrite !mxE Rabs_minus_sym. toR; rewrite /Rinvx. have t2: 2!= 0. apply /eqP; rewrite /GRing.zero //=; apply Rgt_not_eq; fourier. have tn: || @one_M p q : mynorm | != 0. by apply /eqP. rewrite t2 tn /Rdiv Rmult_assoc Rinv_l; last by done. rewrite Rmult_1_r ; fourier. move=> i j eps He. elim (H eps He) => N HN. exists N => n Hn. rewrite /R_dist in HN |-*. apply Rle_lt_trans with (|| (A - Ak n) : mynorm |). rewrite Rabs_minus_sym. have Heq: (A i j - Ak n i j) = ((A - Ak n) i j); [by rewrite !mxE|]. move: Heq; toR => Heq; rewrite /Rminus. rewrite Heq. apply canonical_norm. have H1:= HN n Hn. rewrite Rminus_0_r in H1. rewrite -(Rabs_right ( || (A - Ak n) : mynorm |));[done|apply Rle_ge; apply:pos_norm]. Qed. Lemma abs_cv_cv: forall xn xs, Un_cv (fun n => sum_f_R0 (fun k => Rabs (xn k)) n) xs -> exists l, Un_cv (fun n=> sum_f_R0 xn n) l. Proof. move=> xn xs Hcva. have H1: Cauchy_crit (fun n : nat => sum_f_R0 (fun k : nat => Rabs (xn k)) n). apply CV_Cauchy; by exists xs. have H2: {l| Un_cv (fun n : nat => sum_f_R0 xn n) l}. apply R_complete => eps He. elim (H1 eps He) => N HN. exists N => n m Hn Hm; have H2:= HN n m Hn Hm. rewrite /R_dist in H2 |-*. rewrite !echiv_sums in H2 |-*. elim (le_lt_dec m n) => Hdec. elim (le_lt_eq_dec _ _ Hdec) => Hd2. move/ltP:Hd2=>Hd2. have H10:= (@sum_dif xn m n Hd2 ). rewrite /GRing.opp /GRing.add /= in H10. rewrite /Rminus H10. have H3:= (@big_addn _ _ _ (O%nat) (n.+1)%nat (m.+1) (fun _ => true) xn). rewrite H3 big_mkord. apply Rle_lt_trans with (\sum_(i < n.+1 - m.+1) Rabs (xn (i + m.+1)%Dn)). apply (abs_sum_le_sum_abs). (* (fun i =>xn (i + m.+1)%Dn) (n.+1 - m.+1)) .*) have H4:= (@big_addn _ _ _ (O%nat) (n.+1)%nat (m.+1) (fun _ => true) (fun i => Rabs (xn i))). have h11:= (@sum_dif ( fun i => Rabs (xn i)) _ _ Hd2) . rewrite /GRing.opp /GRing.add /= in h11; rewrite /Rminus in H2. rewrite h11 H4 big_mkord in H2. apply Rle_lt_trans with (Rabs (\sum_(i < n.+1 - m.+1) Rabs (xn (i + m.+1)%Dn)) ). apply RRle_abs . done. by rewrite Hd2 /Rminus Rplus_opp_r Rabs_R0. rewrite Rabs_minus_sym . move/ltP:Hdec => Hdec. have h12:= (@sum_dif _ _ _ Hdec). rewrite /GRing.opp /GRing.add /= in h12; rewrite /Rminus. rewrite h12. have H3:= (@big_addn _ _ _ (O%nat) (m.+1)%nat (n.+1) (fun _ => true) xn). rewrite H3 big_mkord. apply Rle_lt_trans with (\sum_(i < m.+1 - n.+1) Rabs (xn (i + n.+1)%Dn)). apply (abs_sum_le_sum_abs). have H4:= (@big_addn _ _ _ (O%nat) (m.+1)%nat (n.+1) (fun _ => true) (fun i => Rabs (xn i))). rewrite Rabs_minus_sym in H2. have H5:= (sum_dif ( fun i => Rabs (xn i)) Hdec). rewrite /GRing.add /GRing.opp /= in H5. rewrite /Rminus in H2. rewrite H5 in H2. rewrite H4 big_mkord in H2. apply Rle_lt_trans with (Rabs (\sum_(i < m.+1 - n.+1) Rabs (xn (i + n.+1)%Dn)) ). apply RRle_abs . done. by elim H2 => l Hl; exists l. Qed. Lemma th2_246: forall (Ak: nat -> 'M_(p, q)), (exists S, cv_mat_ser (fun n=> Mabs (Ak n)) S) -> exists S', cv_mat_ser Ak S'. Proof. move=> Ak [S Hcv]. red in Hcv. rewrite /cv_mat_ser . have H1: forall i j, exists l, Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Ak n i j) N) l. move=> i j. apply abs_cv_cv with (S i j). apply el_eq_seq_eq with (fun N : nat => sum_f_R0 (fun n : nat => Mabs (Ak n) i j) N). rewrite /Mabs. induction n => //=; [by rewrite !mxE|by rewrite IHn !mxE]. apply Hcv. have Hc: forall i, exists c1:'I_q->R, forall j, Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Ak n i j) N) (c1 j). by move=> i; apply choice with (R:= fun j l=> Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Ak n i j) N) l) . have Hc2: exists c2:'I_p->'I_q->R, forall i j, Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Ak n i j) N) (c2 i j). apply (choice _ (Hc)). elim Hc2 => ch Hch. by exists (\matrix_(i, j) ch i j) => i j; rewrite !mxE. Qed. Lemma thm2_246: forall (Ak: nat -> 'M_(p, q)) , (exists S, cv_mat_ser2 (fun n=> Mabs (Ak n)) S) -> exists S', cv_mat_ser2 Ak S'. Proof. move=> Ak [S Hs]. have Hs1: exists S : matrix real_field p q, cv_mat_ser (fun n : nat => Mabs (Ak n)) S. by exists S; move: Hs; rewrite -echiv_mat_ser => Hs. elim (th2_246 Hs1) => S' HS'. by exists S'; rewrite -echiv_mat_ser. Qed. Lemma th3_247: forall Ak S, Un_cv (fun N:nat => sum_f_R0 (fun n => || (Ak n: 'M_(p, q)) : mynorm |) N) S -> exists S', cv_mat_ser (fun n=> Mabs (Ak n)) S'. Proof. move=> Ak S Hcv. rewrite /cv_mat_ser. have H: forall i j, {l | Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Mabs (Ak n) i j) N) l}. move=> i j. apply Rseries_CV_comp with (fun n : nat => || Ak n : mynorm |). move=> n; rewrite !mxE; split; [apply Rabs_pos|apply canonical_norm]. by exists S. have H1: forall i j, exists l, Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Mabs (Ak n) i j) N) l. by move=> i j; elim (H i j) => l Hl; exists l. have H2: forall i, exists S1, forall j : 'I_q, Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Mabs (Ak n) i j) N) (S1 j). move=> i; apply (choice _ (H1 i)). have H3: exists S1, forall i j, Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Mabs (Ak n) i j) N) (S1 i j). apply (choice _ H2). by elim H3 => S1 Hs1; exists (\matrix_(i, j) S1 i j)=> i j; rewrite !mxE. Qed. End limitMatProp. Section limitsqrMat. Variable p': nat. Notation p := p'.+1. Lemma Hp: (0 < p)%Dn. by done. Qed. Variable mynorm: can_norm. Hypothesis Hyp_norm1: || (1 : 'M_p) : mynorm | = 1. Lemma matr_prod_ineq: forall (X: 'M_p) k, || (X ^+k): mynorm | <= (|| X : mynorm |)^+k. Proof. move=> X k; elim k. by right ; rewrite /GRing.exp. move=> n IHn; rewrite !GRing.exprS. have H1:= prod_ineq_norm mynorm X (X^+n). rewrite /(@GRing.mul) //=. apply Rle_trans with (|| X : mynorm | * || X^+n : mynorm |). done. apply Rmult_le_compat_l. apply pos_norm. done. Qed. Lemma th4_247: forall (X: 'M_p) , || X : mynorm| < R1 -> exists S, cv_mat_ser (fun n => X^+n) S. Proof. move=> X Hx. apply th2_246. rewrite /cv_mat_ser. have H1: forall i j, {S| Un_cv (fun N : nat => sum_f_R0 (fun n : nat =>Mabs (X ^+n) i j) N) S }. move=> i j. apply Rseries_CV_comp with (fun n => (|| X : mynorm |)^+n). move=> n; rewrite !mxE; split; [apply Rabs_pos|]. apply Rle_trans with ( || X^+n : mynorm |). apply canonical_norm. apply matr_prod_ineq. have H3: Rabs (|| X : mynorm |) < 1. rewrite Rabs_right;[done|apply Rle_ge; apply: pos_norm]. have H2:= GP_infinite (|| X : mynorm |) H3 . exists (/(1 - || X : mynorm |)). move=> eps He; case (H2 eps He)=> N Hn0; exists N => n Hn. have H4:= Hn0 n Hn. rewrite /R_dist in H4 |-*. apply Rle_lt_trans with (Rabs (sum_f_R0 (fun n : nat => 1 * || X : mynorm | ^ n ) n - / (1 - || X : mynorm |)) ). right. congr (Rabs _). congr ( _ - _). elim n => //=. by rewrite !expr0 mulr1. move=> n0 Ihn; rewrite Ihn. congr ( _ + _ ). rewrite exprS mul1r. congr ( _ * _). elim n0 => //=; move=> n1 Ihn1; rewrite exprS /GRing.mul /=. by congr ( _ * _ ). done. have Ha: forall i j : 'I_p, exists S, (Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Mabs (X ^+n) i j) N) S). by move=> i j; case (H1 i j) => S Hs; exists S. have Hz: forall i : 'I_p, exists S, forall j, (Un_cv (fun N : nat => sum_f_R0 (fun n : nat => Mabs (X ^+n) i j) N) (S j)). move=> i; case (choice _ (Ha i)) => ch1 Hch1; by exists ch1. case (choice _ Hz) => ch Hch. by exists (\matrix_(i, j) ch i j) => i j; rewrite !mxE. Qed. Lemma sum_prod_id: forall (X: matrix R p p) k , ((1 - X)*(\sum_(0<=i < k.+1) (X^+i)) = 1 - X^+(k.+1))%Ri. Proof. move=> X k. replace (1 - X)%Ri with (- (-1 + X))%Ri;[|by rewrite oppr_add opprK]. rewrite mulNr mulr_addl mulN1r oppr_add opprK. rewrite big_distrr /=. rewrite -sumr_sub //=. induction k => //=. by rewrite big_mkord big_ord_recl big_ord0 expr0 expr1 addr0 mulr1. rewrite !big_mkord in IHk |-*. rewrite big_ord_recr //= IHk . by rewrite !exprS addrA mulrA addrC -addrA addNr addr0 addrC. Qed. Lemma mat_to_zero: forall (X: 'M_p) , || X : mynorm | < 1 -> limit_m (fun n => X^+n) 0. Proof. move=> X Hx. apply th1_246. have H1: exists S0 : matrix real_field p p, cv_mat_ser (fun n : nat => X ^+n) S0. by apply th4_247. by case H1 => S Hs; exists S; apply/echiv_mat_ser. Qed. Lemma th5_aj1: forall (X: 'M_p) S, || X : mynorm | < 1 -> cv_mat_ser2 (fun n => X^+n) S -> (1 - X) * S = 1. Proof. move=> X S Hmn1 Hcv. red in Hcv. have Hcv2:= (@limit_m_mul _ _ _ _ (1 - X)%Ri _ Hcv). have Hcv3: limit_m (fun n : nat => ((1 - X) * (\sum_(i < n.+1) X ^+i))%Ri) (1)%Ri. apply el_eq_mat_seq_cv with (fun n => ((1 - X^+n.+1))%Ri). by move=> n; rewrite -sum_prod_id big_mkord. replace (1:matrix_ringType real_ringType p' ) with ((1 + 0):matrix real_field p p). apply: limit_m_add. by move=> i j eps He; exists O=> n Hn; rewrite /R_dist !mxE addr0 /Rminus Rplus_opp_r Rabs_R0. apply limit_m_opp_0; apply limit_m_Sn ; rewrite //=. by apply: mat_to_zero. by apply/matrixP => i j; rewrite !mxE addr0. by apply limit_m_uniq with (fun n => ((1 - X) * (\sum_(i < n.+1) X ^+i))%Ri); [|done] . Qed. Lemma th5_248: forall X: 'M_p, || X : mynorm | < R1 -> \det (1 - X) <> 0. Proof. move=> X H. case (@th4_247 X H) => S HS. move: HS; rewrite echiv_mat_ser => HS. have H1:= @th5_aj1 X S H HS. have H0: (\det (1 - X) * \det S)%Ri <> 0. rewrite -(@detM _ p' ((1 - X)) S) H1 det1 . rewrite /1 /0 /=; auto with real. rewrite /GRing.mul //= in H0 . by case (RIneq.Rmult_neq_0_reg (\det (1 - X)) (\det S) H0). Qed. Lemma cor1_th5: forall X: 'M_p, || (1 - X) : mynorm | < R1 -> \det X <> 0. Proof. move => X Hn. have Heq: X = 1 - (1 - X). apply/matrixP => i j; rewrite !mxE; toR. by rewrite Ropp_minus_distr' Rplus_comm Rplus_assoc Rplus_opp_l Rplus_0_r. by rewrite Heq; apply th5_248. Qed. Lemma cor2_th5: forall X : 'M_p, || X : mynorm | < R1 -> cv_mat_ser2 (fun n => X^+n) ((1 - X) ^-1). Proof. move=> X H. rewrite -echiv_mat_ser. case (@th4_247 X H) => S HS. move: HS; rewrite echiv_mat_ser => HS. have Hm:= @th5_aj1 X S H HS. have Heq2: (1 - X) * ((1 - X)^-1) = 1. by apply: mulmxV ; apply /eqP; apply th5_248. have Heq : S = ((1 - X)^-1). have Heq: (1 - X) * S = (1 - X) * (1 - X)^-1. by rewrite Hm Heq2. have H1: \det (1 - X) != 0. by apply/eqP; apply th5_248. apply: (mulrI _ Heq); rewrite /GRing.unit //=. by rewrite -Heq echiv_mat_ser. Qed. Lemma norm_inv_ser0: forall (a: 'M_p), || a : mynorm | < R1 -> || (1: 'M_p) : mynorm | = 1 -> || ( 1 - a)^-1 : mynorm | <= 1 / (1 - || a : mynorm | ). Proof. move=> X H H1. have H2 := @cor2_th5 X H. red in H2; move: H2; rewrite (@lem_cv1 p p mynorm) => H2. have H3: Un_cv (fun k : nat => || \sum_(i < k.+1) X ^+i : mynorm | ) ( || (1 - X)^-1 : mynorm |) . move=> eps He. case (H2 eps He) => N HN; exists N => n Hn. rewrite /R_dist in HN |-*. have HN' := HN n Hn. rewrite Rminus_0_r in HN'. apply Rle_lt_trans with ( || (1 - X)^-1 - \sum_(i < n.+1) X ^+i : mynorm | ). have Heq: || (1 - X)^-1 - \sum_(i < n.+1) X ^+i : mynorm | = || \sum_(i < n.+1) X ^+i - (1 - X)^-1 : mynorm|. have Hb:= eq_norm_min mynorm (\sum_(i < n.+1) X ^+i) ((1 - X)^-1). (*rewrite !dif_mult_sc_1 in Hb |-*.*) rewrite /GRing.opp /GRing.one //= in Hb. rewrite Heq. have H7:= tri_min2 mynorm (\sum_(i < n.+1) X ^+i) ((1 - X)^-1). (*rewrite !dif_mult_sc_1 in H7 |-*.*) rewrite /GRing.opp /GRing.one //= in H7. rewrite -(Rabs_right ( || (1 - X)^-1 - \sum_(i < n.+1) X ^+i : mynorm | ) ); [done| apply Rle_ge ; apply pos_norm]. apply lim_seq_monot with ((fun k : nat => || \sum_(i < k.+1) X ^+i : mynorm |)) ((fun k : nat => (\sum_(i < k.+1) (|| X : mynorm |) ^+i))). move=> n. apply Rle_trans with (\sum_(i < n.+1) || X ^+i : mynorm |). apply: mat_norm_sum. apply: big_rel. by right. by move=>*; apply Rplus_le_compat. by move=> *; apply matr_prod_ineq. (* add this statement as a new lemma: norm_sum_ineq mynorm p q (\sum_(i <= n) X ^+i) <= \sum_(i <= n) mynorm p q X ^+i proof using big_op_rel; give generalisation fu: R1->R2; R1:= matrix R p p; R2:= R unlock reducebig. elim ((index_enum I_(n.+1))) => //=. have Heq: (mynorm p q 0) = (mynorm p q (0 *s \1)). f_equal; apply /matrixP=> i j; rewrite !mxE; simp_R; ring. rewrite Heq hom_pos_norm Rabs_R0 Rmult_0_l; by right. move=> N s IHs. apply Rle_trans with ( mynorm p q (X ^+N) + mynorm p q ( foldr (fun (i : ordinal n.+1) (x : matrix real_ring p p) => X ^+i + x) 0 s)%Ri ). apply: trin_ineq_norm. apply Rplus_le_compat. apply matr_prod_ineq. done. *) done. have H4: Rabs || X : mynorm | < 1. rewrite Rabs_right; [done| apply Rle_ge; apply pos_norm]. have Hpser:= GP_infinite (|| X : mynorm |) H4. red in Hpser; red in Hpser. move=> eps He; case (Hpser eps He)=> N Hn0; exists N => n Hn. have H5:= Hn0 n Hn. rewrite /R_dist in H5 |-*. apply Rle_lt_trans with (Rabs (sum_f_R0 (fun n : nat => 1 * || X : mynorm | ^ n) n - / (1 - || X : mynorm |)) ). right. congr (Rabs _). congr ( _ - _). rewrite -echiv_sums //=. elim n => //=. rewrite expr0; toR; ring. move=> n0 Ihn; rewrite Ihn. rewrite exprS; toR. congr ( _ + _ ); rewrite Rmult_1_l. congr ( _ * _). elim n0 => //=; move=> n1 Ihn1. rewrite exprS; by congr ( _ * _ ). by rewrite /Rdiv Rmult_1_l. done. Qed. End limitsqrMat. Section posdefMat. Variable p: nat. Definition sym_mx (T: eqType) (A:'M[T]_p):= forall i j, A i j = A j i. (* the notion of positive definite matrix is given for a symetric matrix*) Definition pos_def (A: 'M_p) := sym_mx A /\ forall (x: 'cV_p), x != 0 -> 0 0 z; rewrite /mulmx -matrixP=> i j; rewrite (ord1_0 i) (ord1_0 j) !mxE //=. Qed. Lemma sum_sqr_gt: forall x: 'cV[R]_n, x != 0 -> 0 < \sum_k x^T ord0 k * x k ord0. move=> x Hx0. elim (Rmat_neq Hx0)=> i0 [j0 Hij0]. rewrite mxE in Hij0; move/eqP: Hij0 => Hij0. apply Rlt_le_trans with (\sum_k Rsqr (x k ord0)). apply Rlt_le_trans with (Rsqr (x i0 j0)). by apply Rlt_0_sqr. (*rewrite /Rsqr /GRing.exp /=; toR.*) rewrite (ord1_0 j0). rewrite (bigD1 i0) //=. rewrite -{1}(addr0 (Rsqr (x i0 ord0))). apply Rplus_le_compat_l. elim: index_enum; [by rewrite big_nil; right|]. move=> t s IH; rewrite big_cons; case C: (t!=i0). rewrite -{1}(addr0 0); apply Rplus_le_compat. rewrite /GRing.exp //=; toR; rewrite -/(Rsqr (x t ord0)); apply Rle_0_sqr. done. done. by right; apply eq_bigr=> k _; rewrite /trmx mxE /GRing.exp /=. Qed. Lemma vec_prod_pos: forall (z: 'cV[R]_n), reflect (0 x. case Hx0: (x !=0); [apply: ReflectT |apply: ReflectF]. rewrite vec_prod_sum => i j. rewrite (ord1_0 i) (ord1_0 j) !mxE /= mulr1n. by apply sum_sqr_gt. move/eqP:Hx0 => Hx0 Hx. move/matrixP: Hx0 => Hx0. have Hc: 0 = x^T *m x. apply/matrixP=> i j; rewrite !mxE. rewrite big1; first by done. by move=> k _; rewrite /trmx mxE !Hx0 !mxE mulr0. rewrite -Hc in Hx. elim (Rlt_irrefl _ (Hx ord0 ord0)). Qed. Lemma vec_prod_unit: forall (z: 'cV[R]_n), (z != 0) -> (z^T *m z \in unitmx). Proof. move=> x Hx0. apply/eqP. rewrite (mx11_scalar (x^T *m x)) det_scalar1. apply Rgt_not_eq. move/vec_prod_pos: Hx0 => Hx0. have H := Hx0 ord0 ord0. rewrite mxE in H; apply: H. Qed. Lemma vec_prod_abs: forall x: 'cV[R]_n, x^T *m x = (Mabs x) ^T *m Mabs x. move=> x. apply/matrixP=> i j; rewrite !vec_prod_sum !mxE (ord1_0 i) (ord1_0 j) /= !GRing.mulr1n. apply: eq_bigr => k _; rewrite /trmx !mxE; toR. have Heqx: (x k ord0 * x k ord0 = Rsqr (x k ord0))%Re by rewrite //. have Heqxa: (Rabs (x k ord0) * Rabs (x k ord0) = Rsqr (Rabs (x k ord0)))%Re by rewrite //. rewrite Heqx Heqxa; apply Rsqr_abs. Qed. Lemma det_scalar_invmx: forall a:R, (@scalar_mx _ 1 a) \in unitmx -> (@scalar_mx _ 1 a)^-1 = (a^-1)%:M. move=> a Ha. set b:= a^-1. rewrite /GRing.inv /= /invmx . rewrite Ha. rewrite det_scalar1. have Ha1: \adj a%:M = (1%:M: 'M_1). rewrite /adjugate -matrixP => i j; rewrite (ord1_0 i) (ord1_0 j) !mxE /=. rewrite expand_cofactor. transitivity (\sum_(s: 'S_1 | s ord0 == ord0) R1 ). apply eq_bigr => s Hs. have Heq: s = perm_one _. rewrite /perm_one . by rewrite -permP => k; rewrite (ord1_0 k) permE; apply/eqP. rewrite Heq odd_perm1 /= expr0 mul1r. rewrite big_pred0; first by done. by move=> k; rewrite //= (ord1_0 k) /=. rewrite big_const_seq //=. rewrite count_filter. have H1 : (size (filter (fun i1 : 'S_1 => i1 ord0 == ord0) (index_enum (perm_for_finType (ordinal_finType 1))))) = 1%Dn. rewrite (@eq_filter _ _ (predT )); last first. by move=> s; rewrite //= (ord1_0 (s ord0)). rewrite filter_index_enum -cardT. rewrite /=. rewrite -{10}(@cards1 (perm_for_finType (ordinal_finType (S O))) (perm_one (ordinal_finType (S O)))). apply: eq_card. move=> s. have Heq: s = perm_one _. rewrite /perm_one . by rewrite -permP => k; rewrite (ord1_0 k) permE (ord1_0 (s ord0)). by rewrite Heq in_simpl /= set11. by rewrite H1 //= addr0. by rewrite Ha1 scalemx1 /b. Qed. End vectorMat.