Files

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 tvs pseudometric_normed_Zmodule 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 coord_continuousUsed by
  • mathcomp.analysis.derive
Source code {KSource code : numFieldType} mSource code nSource code iSource code jSource code :
  continuous (fun MSource code : '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 rV_compact_nondegenerateSource code (TSource code : ptopologicalType) nSource code
    (ASource code : 'I_n.+1 -> set T) :
  (forall iSource code, compact (A i)) ->
  compact [ set vSource code : 'rV[T]_n.+1 | forall iSource code, A i (v ord0 i)].
Proof.
move=> Aico.
have : @compact (prod_topology _) [set fSource code | forall iSource code, A i (f i)].
  by apply: tychonoff.
move=> Aco F FF FA.
set G := [set [set fSource code : 'I_n.+1 -> T | B (\row_jSource code f j)] | BSource code in F].
have row_simpl (vSource code : 'rV[T]_n.+1) : \row_jSource code (v ord0 j) = v.
  by apply/rowP => ?; rewrite mxE.
have row_simpl' (fSource code : 'I_n.+1 -> T) : (\row_jSource code f j) ord0 = f.
  by rewrite funeqE=> ?; rewrite mxE.
have [f [Af clGf]] : [set fSource code | forall iSource code, A i (f i)] `&`
  @cluster (prod_topology _) G !=set0.
  suff GF : ProperFilter G.
    apply: Aco; exists [set vSource code : 'rV[T]_n.+1 | forall iSource code, 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 vSource code : '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_jSource code 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 gSource code | D (\row_jSource code g j)].
  have [E f_E sED] := f_D; rewrite nbhsE.
  set Pj := fun jSource code BjSource code => open_nbhs (f j) Bj /\ Bj `<=` E ord0 j.
  have exPj : forall jSource code, exists BjSource code, 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 gSource code | forall jSource code, (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 gSource code | forall jSource code, get (Pj j) (g j)] | kSource code in [set xSource code | 'I_n.+1 x]];
    last first.
    rewrite predeqE => g; split; first by move=> [_ [_ _ <-]].
    move=> Pg; exists [set gSource code | forall jSource code, get (Pj j) (g j)] => //.
    by exists ord0.
  move=> _ [_ _ <-]; set s := [seq (@^~ j) @^-1` (get (Pj j)) | jSource code :Source code 'I_nSource code.+1].
  exists [fset xSource code 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 gSource code | C (\row_jSource code g j)] by exists C.
by have [g []] := clGf _ _ GC f_D; exists (\row_jSource code (g j : T)).
Qed.

Lemma rV_compactSource code (TSource code : ptopologicalType) nSource code (ASource code : 'I_n -> set T) :
  (forall iSource code, compact (A i)) ->
  compact [ set vSource code : 'rV[T]_n | forall iSource code, 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.
Context [KSource code : numDomainType] {mSource code nSource code : nat}.
Implicit Types x y : 'M[K]_(m, n).

Definition mx_norm

mx_norm : forall [K : numDomainType] {m n : nat}, 'M_(m, n) -> K mx_norm is not universe polymorphic Arguments mx_norm [K] {m n}%_nat_scope x%_ring_scope mx_norm is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.matrix_normedtype.mx_norm Declared in library mathcomp.analysis.normedtype_theory.matrix_normedtype, line 114, characters 11-18

Source code xSource code : K := (\big[maxr/0%:nng]_iSource code `|x i.1 i.2|%:nng)%:num.

Lemma mx_normESource code xSource code : mx_norm x = (\big[maxr/0%:nng]_iSource code `|x i.1 i.2|%:nng)%:num.
Proof.
by []. Qed.

Lemma ler_mx_norm_addSource code xSource code ySource code : 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_eq0Source code xSource code : 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_norm0Source code : 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_neq0Source code xSource code : mx_norm x != 0 -> exists iSource code, 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_natmulSource code xSource code kSource code : 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_normNSource code xSource code : mx_norm (- x) = mx_norm x.
Proof.
congr (_%:nngnum).
by apply eq_bigr => /= ? _; apply/eqP; rewrite mxE -num_eq //= normrN.
Qed.

End mx_norm.

HBSource code.instanceSource code DefinitionSource code _Source code {KSource code :Source code numDomainType}Source code m n :=
  Num.Zmodule_isNormed.Build K 'M[K]_(m, n)
    (@ler_mx_norm_add _ _ _) (@mx_norm_eq0 _ _ _)
    (@mx_norm_natmul _ _ _) (@mx_normN _ _ _).

Section norm_trmx.
Import MaxNngComLaw.

Lemma norm_trmxUsed by
  • mathcomp.analysis.derive
Source code {RSource code : realFieldType} mSource code nSource code (MSource code : 'M[R]_(m, n)) :
  mx_norm M^T = mx_norm M.
Proof.
rewrite [LHS]mx_normE/=.
under eq_bigr do rewrite mxE/=.
rewrite -(pair_big xpredT xpredT (fun iSource code jSource code => `|M j i|%:nng))/=.
by rewrite exchange_big//= pair_big.
Qed.

End norm_trmx.

Lemma mx_normrEUsed by
  • mathcomp.analysis.derive
Source code (KSource code : realDomainType) (mSource code nSource code : nat) (xSource code : 'M[K]_(m, n)) :
  mx_norm x = \big[maxr/0]_ijSource code `|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.

Section example_of_sharing.
Context {KSource code : numDomainType}.

Example matrix_triangle

matrix_triangle : forall {K : numDomainType} [m n : nat] (M N : 'M_(m, n)), (`|M + N| <= `|M| + `|N|)%R matrix_triangle is not universe polymorphic Arguments matrix_triangle {K} [m n]%_nat_scope (M N)%_ring_scope matrix_triangle is opaque Expands to: Constant mathcomp.analysis.normedtype_theory.matrix_normedtype.matrix_triangle Declared in library mathcomp.analysis.normedtype_theory.matrix_normedtype, line 204, characters 8-23

Source code mSource code nSource code (MSource code NSource code : 'M[K]_(m, n)) :
  `|M + N| <= `|M| + `|N|.
Proof.
exact: ler_normD. Qed.

Example pair_triangle

pair_triangle : forall {K : numDomainType} (x y : K * K), (`|x + y| <= `|x| + `|y|)%R pair_triangle is not universe polymorphic Arguments pair_triangle {K} x y pair_triangle is opaque Expands to: Constant mathcomp.analysis.normedtype_theory.matrix_normedtype.pair_triangle Declared in library mathcomp.analysis.normedtype_theory.matrix_normedtype, line 208, characters 8-21

Source code (xSource code ySource code : K * K) : `|x + y| <= `|x| + `|y|.
Proof.
exact: ler_normD. Qed.

End example_of_sharing.

Section matrix_pseudoMetricNormedZmod.
Context {KSource code : numFieldType} {mSource code nSource code : nat}.

Local Lemma ball_gt0Source code (xSource code ySource code : 'M[K]_(m, n)) eSource code : ball x e y -> 0 < e.
Proof.
by case. Qed.

Lemma mx_norm_ballSource code : @ball _ 'M[K]_(m, n) = ball_ (fun xSource code => `| 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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code
  NormedZmod_PseudoMetric_eq.Build K 'M[K]_(m, n) mx_norm_ball.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isPseudoMetricNormedZmoduleSource code.Build _ 'M[K]_(m, n).

End matrix_pseudoMetricNormedZmod.

Section within_continuous_coord.
Context {TSource code : topologicalType} {RSource code : realFieldType} {nSource code : nat}.
Import numFieldNormedType.Exports.

Lemma within_continuous_coordSource code ASource code (fSource code : T -> 'rV[R]_n) :
  {within A, continuous f} <->
  forall iSource code, {within A, continuous (fun xSource code => f x ord0 i)}.
Proof.
split=> [Af i|Af].
- apply: (within_continuous_comp _ f (fun MSource code => 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 bounded_closed_compactSource code (RSource code : realType) nSource code (ASource code : set 'rV[R]_n) :
  bounded_set A -> closed A -> compact A.
Proof.
move=> [M [Mreal normAltM]] Acl.
have Mnco : compact
    [set vSource code : 'rV[R]_n | forall iSource code, 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| | xSource code :Source code 'I_1Source code * '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 mx_normZSource code (KSource code : numDomainType) mSource code nSource code (lSource code : K) (xSource code : 'M[K]_(m, n)) :
  `| l *: x | = `| l | * `| x |.
Proof.
rewrite {1 3}/normr /= !mx_normE
    (eq_bigr (fun iSource code => (`|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.

HBSource code.instanceSource code DefinitionSource code _Source code (KSource code :Source code numFieldTypeSource code) (m n : nat) :=
  Uniform.on ('M[K]_(m, n)).

Section matrix_UniformNZmodule.
Context {KSource code : numFieldType} {mSource code nSource code : nat}.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code PreUniformNmodule_isUniformNmoduleSource code.Build
  'M[K]_(m, n) (@PseudoMetricNormedZmodule_add_unif_continuous _ _).

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code UniformNmodule_isUniformZmoduleSource code.Build
  'M[K]_(m, n) (@PseudoMetricNormedZmodule_opp_unif_continuous _ _).

End matrix_UniformNZmodule.

HBSource code.instanceSource code DefinitionSource code _Source code (KSource code :Source code numFieldTypeSource code) m n :=
  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n)
    (@mx_normZ K m n).

End matrix_NormedModule.

Lemma continuous_mxUsed by
  • mathcomp.analysis.derive
Source code {VSource code : topologicalType} {RSource code : realFieldType} {mSource code nSource code : nat}
    (fSource code : V -> 'M[R]_(m, n)) :
  (forall iSource code jSource code, continuous (fun xSource code => f x i j)) <->
  continuous (fun xSource code : V => \matrix_(iSource code < m, jSource code < 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 {KSource code : realDomainType} {mSource code n1Source code n2Source code : nat}.
Implicit Types (M : 'M[K]_(m, n1)) (N : 'M[K]_(m, n2)).

Lemma norm_row_mxUsed by
  • mathcomp.analysis.derive
Source code MSource code NSource code : `|row_mx M N| = Num.max `|M| `|N|.
Proof.
rewrite /Num.norm/= !mx_normrE.
rewrite -!(pair_bigA_idem _ (fun iSource code jSource code => `|_ 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 norm_row_mx0rSource code MSource code : `|row_mx M (0 : 'M_(m, n2))| = `|M|.
Proof.
by rewrite norm_row_mx normr0; exact/max_idPl. Qed.

Lemma norm_row_mx0lSource code NSource code : `|row_mx (0 : 'M_(m, n1)) N| = `|N|.
Proof.
by rewrite norm_row_mx normr0; exact/max_idPr. Qed.

End norm_row_mx.

Lemma cvg_row_mxUsed by
  • mathcomp.analysis.derive
Source code {TSource code : realFieldType} {FSource code : set_system T} {n1Source code n2Source code : nat}
    (GSource code : 'rV[T]_n1) (HSource code : 'rV[T]_n2) : Filter F ->
  forall (fSource code : T -> 'rV[T]_n1) (gSource code : T -> 'rV[T]_n2),
  f x @[xSource code --> F] --> G -> g x @[xSource code --> F] --> H ->
  row_mx (f x) (g x) @[xSource code --> 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.
Generated by rocqnavi
Source
Uses
Used By