Module mathcomp.analysis.normedtype_theory.matrix_normedtype

From HB Require Import structures.
From mathcomp Require Import boot order finmap ssralg ssrnum matrix.
From mathcomp Require Import interval interval_inference.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp contra classical_sets reals topology.
From mathcomp Require Import prodnormedzmodule tvs pseudometric_normed_Zmodule.
From mathcomp Require Import normed_module.

# Normed topological Abelian group of matrices This file defines a `normedModType` of space of matrices. It also proves the Heine-Borel theorem, more precisely that a closed and bounded set of vectors in $\bar{R}^n$ is compact and various lemmas about compact sets. ``` mx_norm M == norm of the matrix M := \big[maxr/0]_i `|x i.1 i.2| ```

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Lemma { : numFieldType} :
continuous (fun : 'M[K]_(m, n) => M i j).

Proof.

move=> /= M s /= /(nbhs_ballP (M i j)) [e e0 es].
by apply/nbhs_ballP; exists e => //= N [_ MN]; exact/es/MN.
Qed.

#[local] Lemma ( : ptopologicalType)
    ( : 'I_n.+1 -> set T) :
  (forall , compact (A i)) ->
  compact [ set : 'rV[T]_n.+1 | forall , A i (v ord0 i)].

Proof.

move=> Aico.
have : @compact (prod_topology _) [set | forall , A i (f i)].
  by apply: tychonoff.
move=> Aco F FF FA.
set G := [set [set : 'I_n.+1 -> T | B (\row_ f j)] | in F].
have row_simpl ( : 'rV[T]_n.+1) : \row_ (v ord0 j) = v.
  by apply/rowP => ?; rewrite mxE.
have row_simpl' ( : 'I_n.+1 -> T) : (\row_ f j) ord0 = f.
  by rewrite funeqE=> ?; rewrite mxE.
have [f [Af clGf]] : [set | forall , A i (f i)] `&`
  @cluster (prod_topology _) G !=set0.
  suff GF : ProperFilter G.
    apply: Aco; exists [set : 'rV[T]_n.+1 | forall , A i (v ord0 i)] => //.
    by rewrite predeqE => f; split => Af i; [have := Af i|]; rewrite row_simpl'.
  apply Build_ProperFilter_ex.
    move=> _ [C FC <-]; have /filter_ex [v Cv] := FC.
    by exists (v ord0); rewrite /= row_simpl.
  split.
  - by exists setT => //; apply: filterT.
  - by move=> _ _ [C FC <-] [D FD <-]; exists (C `&` D) => //; apply: filterI.
  move=> C D sCD [E FE EeqC]; exists [set : 'rV[T]_n.+1 | D (v ord0)].
    by apply: filterS FE => v Ev; apply/sCD; rewrite -EeqC/= row_simpl.
  by rewrite predeqE => ? /=; rewrite row_simpl'.
exists (\row_ f j); split; first by move=> i; rewrite mxE; apply: Af.
move=> C D FC f_D; have {}f_D :
  nbhs (f : prod_topology _) [set | D (\row_ g j)].
  have [E f_E sED] := f_D; rewrite nbhsE.
  set Pj := fun => open_nbhs (f j) Bj /\ Bj `<=` E ord0 j.
  have exPj : forall , exists , open_nbhs (f j) Bj /\ Bj `<=` E ord0 j.
    move=> j; have := f_E ord0 j; rewrite nbhsE => - [Bj].
    by rewrite row_simpl'; exists Bj.
  exists [set | forall , (get (Pj j)) (g j)]; last first.
    move=> g Pg; apply: sED => i j; rewrite ord1 row_simpl'.
    by have /getPex [_ /(_ _ (Pg j))] := exPj j.
  split; last by move=> j; have /getPex [[]] := exPj j.
  exists [set [set | forall , get (Pj j) (g j)] | in [set | 'I_n.+1 x]];
    last first.
    rewrite predeqE => g; split; first by move=> [_ [_ _ <-]].
    move=> Pg; exists [set | forall , get (Pj j) (g j)] => //.
    by exists ord0.
  move=> _ [_ _ <-]; set s := [seq (@^~ j) @^-1` (get (Pj j)) | .+1].
  exists [fset in s]%fset.
    move=> B'; rewrite in_fset => /mapP [j _ ->]; rewrite inE.
    exists j => //; exists (get (Pj j)) => //.
    by have /getPex [[]] := exPj j.
  rewrite predeqE => g; split=> [Ig j|Ig B'].
    apply: (Ig ((@^~ j) @^-1` (get (Pj j)))).
    by rewrite /= in_fset; apply/mapP; exists j => //; rewrite mem_enum.
  by rewrite /= in_fset => /mapP [j _ ->]; apply: Ig.
have GC : G [set | C (\row_ g j)] by exists C.
by have [g []] := clGf _ _ GC f_D; exists (\row_ (g j : T)).
Qed.

Lemma ( : ptopologicalType) ( : 'I_n -> set T) :
(forall , compact (A i)) ->
compact [ set : 'rV[T]_n | forall , A i (v ord0 i)].

Proof.

case: n A => [A _ | ]; last exact: rV_compact_nondegenerate.
have P0 : #|{: 'I_1 * 'I_0}| = 0 by rewrite card_prod/= !card_ord muln0.
pose v0 := Matrix (ffun0 P0 : {ffun 'I_1 * 'I_0 -> T}).
rewrite (_ : mkset _ = [set v0]); last exact: compact_set1.
by rewrite predeqE => x /=; split => [ _ | _ []//]; apply/rowP => -[].
Qed.

Section mx_norm.
Variables ( : numDomainType) ( : nat).
Implicit Types x y : 'M[K]_(m, n).

Definition : K := (\big[maxr/0%:nng]_ `|x i.1 i.2|%:nng)%:num.

Lemma : mx_norm x = (\big[maxr/0%:nng]_ `|x i.1 i.2|%:nng)%:num.

Proof.

by []. Qed.

Lemma : mx_norm (x + y) <= mx_norm x + mx_norm y.

Proof.

rewrite !mx_normE [_ <= _%:num]num_le; apply/bigmax_leP.
split=> [|ij _]; first exact: addr_ge0.
rewrite mxE; apply: le_trans (ler_normD _ _) _.
by rewrite lerD// -[leLHS]nngE num_le; exact: le_bigmax.
Qed.

Lemma : mx_norm x = 0 -> x = 0.

Proof.

move/eqP; rewrite eq_le -[0]nngE mx_normE num_le => /andP[/bigmax_leP[_ x0] _].
apply/matrixP => i j; rewrite mxE; apply/eqP.
by rewrite -num_abs_eq0 eq_le (x0 (i, j))//= -num_le/=.
Qed.

Lemma : mx_norm 0 = 0.

Proof.

rewrite /mx_norm (eq_bigr (fun=> 0%R%:nng)) /=.
by move=> i _; apply val_inj => /=; rewrite mxE normr0.
by elim/big_ind : _ => // a b; rewrite num_max => -> ->; rewrite maxxx.
Qed.

Lemma : mx_norm x != 0 -> exists , mx_norm x = `|x i.1 i.2|.

Proof.

rewrite /mx_norm.
elim/big_ind : _ => [|a b Ha Hb H|/= i _ _]; [by rewrite eqxx| |by exists i].
case: (leP a b) => ab.
+ suff /Hb[i xi] : b%:num != 0 by exists i.
by apply: contra H => b0; rewrite max_r.
+ suff /Ha[i xi] : a%:num != 0 by exists i.
by apply: contra H => a0; rewrite max_l // ltW.
Qed.

Lemma : mx_norm (x *+ k) = (mx_norm x) *+ k.

Proof.

rewrite [in RHS]/mx_norm; elim: k => [|k ih]; first by rewrite !mulr0n mx_norm0.
rewrite !mulrS; apply/eqP; rewrite eq_le; apply/andP; split.
by rewrite -ih; exact/ler_mx_norm_add.
have [/mx_norm_eq0->|x0] := eqVneq (mx_norm x) 0.
by rewrite -/(mx_norm 0) -/(mx_norm 0) !(mul0rn,addr0,mx_norm0).
rewrite -/(mx_norm x) -num_abs_le; first by rewrite mx_normE.
apply/bigmax_geP; right => /=.
have [i Hi] := mx_norm_neq0 x0.
exists i => //; rewrite Hi -!mulrS -normrMn mulmxnE.
by rewrite le_eqVlt; apply/orP; left; apply/eqP/val_inj => /=; rewrite normr_id.
Qed.

Lemma : mx_norm (- x) = mx_norm x.

Proof.

congr (_%:nngnum).
by apply eq_bigr => /= ? _; apply/eqP; rewrite mxE -num_eq //= normrN.
Qed.

End mx_norm.

Lemma ( : realDomainType) ( : nat) ( : 'M[K]_(m, n)) :
mx_norm x = \big[maxr/0]_ `|x ij.1 ij.2|.

Proof.

rewrite /mx_norm; apply/esym.
elim/big_ind2 : _ => //= a a' b b' ->{a'} ->{b'}.
by have [ab|ab] := leP a b; [rewrite max_r | rewrite max_l // ltW].
Qed.

. () (m n : nat) :=
  Num.Zmodule_isNormed.Build K 'M[K]_(m, n)
    (@ler_mx_norm_add _ _ _) (@mx_norm_eq0 _ _ _)
    (@mx_norm_natmul _ _ _) (@mx_normN _ _ _).

Section example_of_sharing.
Variables ( : numDomainType).

Example ( : 'M[K]_(m, n)) :
  `|M + N| <= `|M| + `|N|.

Proof.

exact: ler_normD. Qed.

Example ( : K * K) : `|x + y| <= `|x| + `|y|.

Proof.

exact: ler_normD. Qed.

End example_of_sharing.

Section matrix_pseudoMetricNormedZmod.
Variables ( : numFieldType) ( : nat).

Local Lemma ( : 'M[K]_(m, n)) : ball x e y -> 0 < e.

Proof.

by case. Qed.

Lemma : @ball _ 'M[K]_(m, n) = ball_ (fun => `| x |).

Proof.

rewrite /normr /ball_ predeq3E => x e y/= /[!mx_normE]; split=> [[]|xey].
- move=> /[dup] => /ltW/nonnegP[{}e] e_gt0 xey.
  rewrite num_lt; apply/bigmax_ltP => /=.
  by rewrite -num_lt /=; split => // -[? ?] _; rewrite !mxE; exact: xey.
- have e_gt0 : 0 < e by rewrite (le_lt_trans _ xey).
  move: e_gt0 (e_gt0) xey => /ltW/nonnegP[{}e] e_gt0.
  move=> /(bigmax_ltP _ _ _ (fun=> _%:itv)) /= [e0 xey].
  split=> // i j.
  by move: (xey (i, j)); rewrite !mxE; exact.
Qed.

.
  NormedZmod_PseudoMetric_eq.Build K 'M[K]_(m, n) mx_norm_ball.

..Build _ 'M[K]_(m, n).

End matrix_pseudoMetricNormedZmod.

Section within_continuous_coord.
Context { : topologicalType} { : realFieldType} { : nat}.
Import numFieldNormedType.Exports.

Lemma ( : T -> 'rV[R]_n) :
  {within A, continuous f} <->
  forall , {within A, continuous (fun => f x ord0 i)}.

Proof.

split=> [Af i|Af].
- apply: (within_continuous_comp _ f (fun => M ord0 i)) => //= x _.
  exact: coord_continuous.
- apply/subspace_continuousP => /= x Ax; apply/cvgrPdist_le => /= e e0.
  rewrite near_withinE; near=> t => At.
  rewrite /Num.norm/= mx_normrE (bigmax_le _ (ltW e0))//= => -[i j] _ /=.
  rewrite {i}(ord1 i) !mxE.
  move: j At; near: t; apply: filter_forall => /= j.
  have /subspace_continuousP/(_ x Ax)/cvgr_dist_le/(_ _ e0) := Af j.
  by rewrite near_withinE.
Unshelve. all: by end_near. Qed.

End within_continuous_coord.

Lemma ( : realType) ( : set 'rV[R]_n) :
bounded_set A -> closed A -> compact A.

Proof.

move=> [M [Mreal normAltM]] Acl.
have Mnco : compact
    [set : 'rV[R]_n | forall , v ord0 i \in `[(- (M + 1)), (M + 1)]].
  apply: (@rV_compact _ _ (fun=> `[(- (M + 1)), (M + 1)]%classic)).
  by move=> _; apply: segment_compact.
apply: subclosed_compact Acl Mnco _ => v /normAltM normvleM i.
suff : `|v ord0 i : R| <= M + 1 by rewrite ler_norml.
apply: le_trans (normvleM _ _); last by rewrite ltrDl.
have /mapP[j Hj ->] : `|v ord0 i| \in [seq `|v x.1 x.2| | * 'I_n].
  by apply/mapP; exists (ord0, i) => //=; rewrite mem_enum.
by rewrite [leRHS]/normr /= mx_normrE; apply/bigmax_geP; right => /=; exists j.
Qed.

Section matrix_NormedModule.

Lemma ( : numDomainType) ( : K) ( : 'M[K]_(m, n)) :
`| l *: x | = `| l | * `| x |.

Proof.

rewrite {1 3}/normr /= !mx_normE
(eq_bigr (fun => (`|l| * `|x i.1 i.2|)%:nng)).
by move=> i _; rewrite mxE //=; apply/eqP; rewrite -num_eq /= normrM.
elim/big_ind2 : _ => // [|a b c d bE dE]; first by rewrite mulr0.
by rewrite !num_max bE dE maxr_pMr.
Qed.

. () m n :=
  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n)
    (@mx_normZ K m n).

End matrix_NormedModule.

Lemma { : topologicalType} { : realFieldType} { : nat}
    ( : V -> 'M[R]_(m, n)) :
  (forall , continuous (fun => f x i j)) <->
  continuous (fun : V => \matrix_( < m, < n) f x i j).

Proof.

split => [cf x|cf i j v].
- apply/cvgrPdist_le => /= e e0; near=> t.
  rewrite /Num.norm/= mx_normrE/= (bigmax_le _ (ltW e0))// => -[i j] _.
  rewrite !mxE/=.
  move: i j; near: t.
  apply: filter_forall => /= i; apply: filter_forall => /= j.
  have /(@cvgrPdist_le _ R^o)/(_ _ e0) := cf i j x.
  exact: filterS.
- apply/(@cvgrPdist_le _ R^o) => /= e e0.
  have /cvgrPdist_le/(_ _ e0) := cf v.
  apply: filterS => w.
  apply: le_trans.
  rewrite [in leRHS]/Num.norm/= mx_normrE/=.
  apply: le_trans (le_bigmax _ _ (i, j)).
  by rewrite !mxE.
Unshelve. all: by end_near. Qed.

Section norm_row_mx.
Context { : realDomainType} { : nat}.
Implicit Types (M : 'M[K]_(m, n1)) (N : 'M[K]_(m, n2)).

Lemma : `|row_mx M N| = Num.max `|M| `|N|.

Proof.

rewrite /Num.norm/= !mx_normrE.
rewrite -!(pair_bigA_idem _ (fun => `|_ i j|))/= ?maxxx//.
rewrite -big_split_idem/= ?maxxx//; apply: eq_bigr => i _.
rewrite big_split_ord_idem/= ?maxxx//.
by move=> a; rewrite maxC.
by congr maxr; apply: eq_bigr => j _; [rewrite row_mxEl|rewrite row_mxEr].
Qed.

Lemma : `|row_mx M (0 : 'M_(m, n2))| = `|M|.

Proof.

by rewrite norm_row_mx normr0; exact/max_idPl. Qed.

Lemma : `|row_mx (0 : 'M_(m, n1)) N| = `|N|.

Proof.

by rewrite norm_row_mx normr0; exact/max_idPr. Qed.

End norm_row_mx.

Lemma { : realFieldType} { : set_system T} { : nat}
    ( : 'rV[T]_n1) ( : 'rV[T]_n2) : Filter F ->
  forall ( : T -> 'rV[T]_n1) ( : T -> 'rV[T]_n2),
  f x @[ --> F] --> G -> g x @[ --> F] --> H ->
  row_mx (f x) (g x) @[ --> F] --> row_mx G H.

Proof.

move=> FF M N cvgM cvgN; apply/cvgrPdist_le => /= e e0; near=> t.
rewrite sub_row_mx norm_row_mx ge_max; apply/andP; split.
- by near: t; move/cvgrPdist_le : cvgM => /(_ _ e0).
- by near: t; move/cvgrPdist_le : cvgN => /(_ _ e0).
Unshelve. all: by end_near. Qed.

Files

Module mathcomp.analysis.normedtype_theory.matrix_normedtype