GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisgaussianmeasurable_matrix

Measurable structure on matrices

GaussianAnalysis.gaussian.measurable_matrixlibrary/gaussian/measurable_matrix.v500 lines36 lemmas and theorems, 3 definitionssource
Imports 0 library modules and 23 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.finite_group.fingroup, mathcomp.finite_group.perm, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.rat, mathcomp.algebra.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.classical.cardinality, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.algebra.interval, mathcomp.algebra.interval_inference, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation

Imported by 56
Required by 48 files of the paper proofs

A matrix with entries in a measurable space is measurable for the sigma-algebra generated by its entries, as tuples are in MathComp-Analysis (measurable_structure.v). Row vectors 'rV[T]_n and column vectors 'cV[T]_n are matrices, so they get this structure too. The boxes generate it and are closed under intersection, so two finite measures that agree on the boxes agree (measure_mxbox_unique). For real matrices it contains the open sets, so continuous functions are measurable (continuous_measurable_mx).

The last sections concern the norm `|A| of a real matrix, which in MathComp is the largest absolute value of an entry: bounds for entries, permuted columns, blocks and products (mx_norm_entry_le, ...), and the continuity of maps into matrices (continuous_mxP) and of matrix products (continuous_mulmxr, continuous_mulmxl).

measure_matrix_display ddisplay of the sigma-algebra of the matrices with entries in a space of display d 'M[T]_(m, n) is equipped with a measurableType structure generated by the entries
mxbox Athe box of the matrices M such that M i j is in A i j for all i and j; for a row vector x, the box [set x | forall j, A j (x 0 j)] is used directly (rowboxE)
mxboxes Tthe boxes mxbox A with measurable sides A i j

Main results

ResultsStatementUsed by theories/
measurable_fun_mxP
A map into 'M[T]_(m, n) is measurable if and only if each of its entries is. Matrices carry the sigma-algebra generated by their entries.Gaussian/Law/LibraryBridge
measure_mxbox_uniquemeasure_rowbox_unique
Two measures on matrices (or row vectors) that agree on the boxes with measurable sides, the first of them finite, agree on every measurable set.through gauss_unique
continuous_measurable_mx
A continuous real function of a real matrix is measurable: the open sets of 'M[R]_(m, n) are measurable.Gaussian/Orthogonal/EqualCovariance
mx_norm_entry_lemx_norm_mulmx_lemx_norm_col_mx_lemx_norm_col_perm_le
For the norm of a real matrix: every entry is bounded by the norm, |A B| <= n |A| |B| when A has n columns, |col_mx P Q| <= |P| + |Q|, and permuting the columns does not increase the norm.Gaussian/Law/LibraryBridge
continuous_mxPcontinuous_mulmxrcontinuous_mulmxl
A map into real matrices is continuous if each of its entries is, and the matrix product is continuous in each factor.

Declarations40 exported, 6 local

lemma, theoremdefinitioninstancelocal
definition measure_matrix_display source, line 50
Type
measure_display -> measure_display
Definition
Definition measure_matrix_display : measure_display -> measure_display.
Used by 1 declaration in 1 file
sectionmeasurable_matrix
Context {d} {T : sigmaRingType d} (m n : nat).
let entry section-local source, line 56 
Let entry (k : 'I_(m * n)) (A : 'M[T]_(m, n)) : T := mxvec A 0 k.
Used by 4 declarations in 1 file
let matrix_set0 section-local source, line 58 
Let matrix_set0 : g_sigma_preimage entry set0.
Used by 1 declaration in 1 file
let matrix_setC section-local source, line 61 
Let matrix_setC A : g_sigma_preimage entry A -> g_sigma_preimage entry (~` A).
Used by 1 declaration in 1 file
let matrix_bigcup section-local source, line 64 
Let matrix_bigcup (F : nat -> set 'M[T]_(m, n)) :
  (forall i, g_sigma_preimage entry (F i)) ->
  g_sigma_preimage entry (\bigcup_i (F i)).
Used by 1 declaration in 1 file

HB declares canonical projections that the structure of T already provides, as for tuples; the warning says so. The setting lasts until the end of this file and is not exported.

Set Warnings "-redundant-canonical-projection".
instance instance at line 73 source, line 73 
HB.instance Definition _ := @isMeasurable.Build (measure_matrix_display d)
  'M[T]_(m, n) (g_sigma_preimage entry) matrix_set0 matrix_setC matrix_bigcup.
sectionmeasurable_entries
Context {d d'} {T : measurableType d} {U : measurableType d'} {m n : nat}.
Implicit Types f : U -> 'M[T]_(m, n).
lemma measurable_mxentry source, line 82 
forall {d : measure_display} {T : measurableType d} {m n : nat} (i : 'I_m) (j : 'I_n),
measurable_fun [set: 'M_(m, n)]
  (fun A : 'M_(m, n) => A i j)
Statement as written in the source
Lemma measurable_mxentry (i : 'I_m) (j : 'I_n) :
  measurable_fun [set: 'M[T]_(m, n)] (fun A => A i j).
Used by 62 declarations in 22 files
lemma measurable_fun_mxP main result source, line 91 
forall {d d' : measure_display} {T : measurableType d} {U : measurableType d'} 
  {m n : nat} (f : U -> 'M_(m, n)),
measurable_fun [set: U] f <->
(forall (i : 'I_m) (j : 'I_n), measurable_fun [set: U] (fun x : U => f x i j))
Main result, as the README states it

A map into 'M[T]_(m, n) is measurable if and only if each of its entries is. Matrices carry the sigma-algebra generated by their entries.

Used in theories/ by: Gaussian/Law/LibraryBridge
Statement as written in the source
Lemma measurable_fun_mxP f : measurable_fun [set: U] f <->
  forall i j, measurable_fun [set: U] (fun x => f x i j).
Used by 37 declarations in 13 files
lemma measurable_matrix source, line 106 
forall {d d' : measure_display} {T : measurableType d} {U : measurableType d'} 
  {m n : nat} [h : 'I_m -> 'I_n -> U -> T],
(forall (i : 'I_m) (j : 'I_n), measurable_fun [set: U] (h i j)) ->
measurable_fun [set: U] (fun x : U => \matrix_(i, j) h i j x)
Statement as written in the source
Lemma measurable_matrix (h : 'I_m -> 'I_n -> U -> T) :
  (forall i j, measurable_fun [set: U] (h i j)) ->
  measurable_fun [set: U] (fun x => \matrix_(i, j) h i j x).
sectionmeasurable_matrix_operations
Context {d d'} {T : measurableType d} {U : measurableType d'}.
lemma measurable_row_mx source, line 119 
forall {d d' : measure_display} {T : measurableType d} {U : measurableType d'}
  [m n1 n2 : nat] [f : U -> 'M_(m, n1)] [g : U -> 'M_(m, n2)],
measurable_fun [set: U] f ->
measurable_fun [set: U] g -> measurable_fun [set: U] (fun x : U => row_mx (f x) (g x))
Statement as written in the source
Lemma measurable_row_mx m n1 n2 (f : U -> 'M[T]_(m, n1))
    (g : U -> 'M[T]_(m, n2)) :
  measurable_fun [set: U] f -> measurable_fun [set: U] g ->
  measurable_fun [set: U] (fun x => row_mx (f x) (g x)).
Used by 5 declarations in 2 files
lemma measurable_col_mx source, line 130 
forall {d d' : measure_display} {T : measurableType d} {U : measurableType d'}
  [m1 m2 n : nat] [f : U -> 'M_(m1, n)] [g : U -> 'M_(m2, n)],
measurable_fun [set: U] f ->
measurable_fun [set: U] g -> measurable_fun [set: U] (fun x : U => col_mx (f x) (g x))
Statement as written in the source
Lemma measurable_col_mx m1 m2 n (f : U -> 'M[T]_(m1, n))
    (g : U -> 'M[T]_(m2, n)) :
  measurable_fun [set: U] f -> measurable_fun [set: U] g ->
  measurable_fun [set: U] (fun x => col_mx (f x) (g x)).
lemma measurable_lsubmx source, line 141 
forall {d : measure_display} {T : measurableType d} [m n1 n2 : nat],
measurable_fun [set: 'M_(m, n1 + n2)] lsubmx
Statement as written in the source
Lemma measurable_lsubmx m n1 n2 :
  measurable_fun [set: 'M[T]_(m, n1 + n2)] (@lsubmx T m n1 n2).
Used by 2 declarations in 1 file
lemma measurable_rsubmx source, line 148 
forall {d : measure_display} {T : measurableType d} [m n1 n2 : nat],
measurable_fun [set: 'M_(m, n1 + n2)] rsubmx
Statement as written in the source
Lemma measurable_rsubmx m n1 n2 :
  measurable_fun [set: 'M[T]_(m, n1 + n2)] (@rsubmx T m n1 n2).
Used by 3 declarations in 2 files
lemma measurable_usubmx source, line 155 
forall {d : measure_display} {T : measurableType d} [m1 m2 n : nat],
measurable_fun [set: 'M_(m1 + m2, n)] usubmx
Statement as written in the source
Lemma measurable_usubmx m1 m2 n :
  measurable_fun [set: 'M[T]_(m1 + m2, n)] (@usubmx T m1 m2 n).
lemma measurable_dsubmx source, line 162 
forall {d : measure_display} {T : measurableType d} [m1 m2 n : nat],
measurable_fun [set: 'M_(m1 + m2, n)] dsubmx
Statement as written in the source
Lemma measurable_dsubmx m1 m2 n :
  measurable_fun [set: 'M[T]_(m1 + m2, n)] (@dsubmx T m1 m2 n).
lemma measurable_col_perm source, line 169 
forall {d : measure_display} {T : measurableType d} [m n : nat] (s : {perm 'I_n}),
measurable_fun [set: 'M_(m, n)] (col_perm s)
Statement as written in the source
Lemma measurable_col_perm m n (s : 'S_n) :
  measurable_fun [set: 'M[T]_(m, n)] (col_perm s).
Used by 6 declarations in 3 files
lemma measurable_row_perm source, line 176 
forall {d : measure_display} {T : measurableType d} [m n : nat] (s : {perm 'I_m}),
measurable_fun [set: 'M_(m, n)] (row_perm s)
Statement as written in the source
Lemma measurable_row_perm m n (s : 'S_m) :
  measurable_fun [set: 'M[T]_(m, n)] (row_perm s).
lemma measurable_trmx source, line 183 
forall {d : measure_display} {T : measurableType d} [m n : nat],
measurable_fun [set: 'M_(m, n)] trmx
Statement as written in the source
Lemma measurable_trmx m n : measurable_fun [set: 'M[T]_(m, n)] trmx.
lemma measurable_const_mx source, line 189 
forall {d : measure_display} {T : measurableType d} [m n : nat],
measurable_fun [set: T] const_mx
Statement as written in the source
Lemma measurable_const_mx m n :
  measurable_fun [set: T] (@const_mx T m n).
Used by 1 declaration in 1 file
sectionmeasurable_mxbox
Context {d} {T : measurableType d} {m n : nat}.
definition mxbox source, line 201
Type
forall {d : measure_display} {T : measurableType d} {m n : nat},
('I_m -> 'I_n -> set T) -> set 'M_(m, n)
Definition
Definition mxbox (A : 'I_m -> 'I_n -> set T) : set 'M[T]_(m, n) :=
  [set M | forall i j, A i j (M i j)].
Used by 9 declarations in 2 files
definition mxboxes source, line 204
Type
forall {d : measure_display} {T : measurableType d} {m n : nat}, set (set 'M_(m, n))
Definition
Definition mxboxes : set (set 'M[T]_(m, n)) :=
  [set mxbox A | A in [set A | forall i j, measurable (A i j)]].
Used by 4 declarations in 2 files
lemma mxboxT source, line 207 
forall {d : measure_display} {T : measurableType d} {m n : nat},
mxbox (fun=> (fun=> [set: T])) = [set: 'M_(m, n)]
Statement as written in the source
Lemma mxboxT : mxbox (fun _ _ => [set: T]) = [set: 'M[T]_(m, n)].
Used by 1 declaration in 1 file
lemma mxboxI source, line 210 
forall {d : measure_display} {T : measurableType d} {m n : nat}
  (A B : 'I_m -> 'I_n -> set T),
mxbox A `&` mxbox B = mxbox (fun (i : 'I_m) (j : 'I_n) => A i j `&` B i j)
Statement as written in the source
Lemma mxboxI A B : mxbox A `&` mxbox B = mxbox (fun i j => A i j `&` B i j).
Used by 1 declaration in 1 file
lemma measurable_mxbox source, line 217 
forall {d : measure_display} {T : measurableType d} {m n : nat} [A : 'I_m -> 'I_n -> set T],
(forall (i : 'I_m) (j : 'I_n), d.-measurable (A i j)) ->
(measure_matrix_display d).-measurable (mxbox A)
Statement as written in the source
Lemma measurable_mxbox A : (forall i j, measurable (A i j)) ->
  measurable (mxbox A).
Used by 3 declarations in 1 file
lemma measurable_mxboxes source, line 230 
forall {d : measure_display} {T : measurableType d} {m n : nat},
(measure_matrix_display d).-measurable = <<s mxboxes >>
Statement as written in the source
Lemma measurable_mxboxes : @measurable _ 'M[T]_(m, n) = <<s mxboxes >>.
Used by 2 declarations in 2 files
lemma setI_closed_mxboxes source, line 246 
forall {d : measure_display} {T : measurableType d} {m n : nat}, setI_closed mxboxes
Statement as written in the source
Lemma setI_closed_mxboxes : setI_closed mxboxes.
Used by 2 declarations in 2 files
lemma measure_mxbox_unique main result source, line 252 
forall {d : measure_display} {T : measurableType d} {m n : nat} 
  [R : realType] [mu1 mu2 : measure 'M_(m, n) R],
(mu1 [set: 'M_(m, n)] < +oo)%E ->
(forall A : 'I_m -> 'I_n -> set T,
 (forall (i : 'I_m) (j : 'I_n), d.-measurable (A i j)) -> mu1 (mxbox A) = mu2 (mxbox A)) ->
forall [X : set 'M_(m, n)], (measure_matrix_display d).-measurable X -> mu1 X = mu2 X
Main result, as the README states it

Two measures on matrices (or row vectors) that agree on the boxes with measurable sides, the first of them finite, agree on every measurable set.

Used in theories/ by: through gauss_unique
Statement as written in the source
Lemma measure_mxbox_unique (R : realType)
    (mu1 mu2 : {measure set 'M[T]_(m, n) -> \bar R}) :
  (mu1 [set: 'M[T]_(m, n)] < +oo)%E ->
  (forall A, (forall i j, measurable (A i j)) ->
    mu1 (mxbox A) = mu2 (mxbox A)) ->
  forall X, measurable X -> mu1 X = mu2 X.
Used by 1 declaration in 1 file
sectionmeasurable_rowbox
Context {d} {T : measurableType d} {n : nat}.
lemma rowboxE source, line 274 
forall {d : measure_display} {T : measurableType d} {n : nat} (A : 'I_n -> set T),
[set x | (forall j : 'I_n, A j (x 0 j))] = mxbox (fun=> [eta A])
Statement as written in the source
Lemma rowboxE (A : 'I_n -> set T) :
  [set x : 'rV[T]_n | forall j, A j (x 0 j)] = mxbox (fun _ j => A j).
Used by 3 declarations in 2 files
lemma measurable_rowbox source, line 280 
forall {d : measure_display} {T : measurableType d} {n : nat} [A : 'I_n -> set T],
(forall j : 'I_n, d.-measurable (A j)) ->
(measure_matrix_display d).-measurable [set x | (forall j : 'I_n, A j (x 0 j))]
Statement as written in the source
Lemma measurable_rowbox (A : 'I_n -> set T) : (forall j, measurable (A j)) ->
  measurable [set x : 'rV[T]_n | forall j, A j (x 0 j)].
Used by 5 declarations in 3 files
lemma measure_rowbox_unique main result source, line 284 
forall {d : measure_display} {T : measurableType d} {n : nat} [R : realType]
  [mu1 mu2 : measure 'rV_n R],
(mu1 [set: 'rV_n] < +oo)%E ->
(forall A : 'I_n -> set T,
 (forall j : 'I_n, d.-measurable (A j)) ->
 mu1 (fun x : 'rV_n => [set x0 | (forall j : 'I_n, A j (x0 0 j))] x) =
 mu2 (fun x : 'rV_n => [set x0 | (forall j : 'I_n, A j (x0 0 j))] x)) ->
forall [X : set 'rV_n], (measure_matrix_display d).-measurable X -> mu1 X = mu2 X
Main result

Stated in the README together with measure_mxbox_unique.

Statement as written in the source
Lemma measure_rowbox_unique (R : realType)
    (mu1 mu2 : {measure set 'rV[T]_n -> \bar R}) :
  (mu1 [set: 'rV[T]_n] < +oo)%E ->
  (forall A : 'I_n -> set T, (forall j, measurable (A j)) ->
    mu1 [set x | forall j, A j (x 0 j)] =
    mu2 [set x | forall j, A j (x 0 j)]) ->
  forall X, measurable X -> mu1 X = mu2 X.
Used by 1 declaration in 1 file
sectionmeasurable_real_matrix
Context {R : realType} {d} {U : measurableType d}.
lemma measurable_addmx source, line 304 
forall {R : realType} {d : measure_display} {U : measurableType d} 
  [m n : nat] [f g : U -> 'M_(m, n)],
measurable_fun [set: U] f ->
measurable_fun [set: U] g -> measurable_fun [set: U] (fun x : U => f x + g x)
Statement as written in the source
Lemma measurable_addmx m n (f g : U -> 'M[R]_(m, n)) :
  measurable_fun [set: U] f -> measurable_fun [set: U] g ->
  measurable_fun [set: U] (fun x => f x + g x).
Used by 25 declarations in 11 files
lemma measurable_oppmx source, line 313 
forall {R : realType} {d : measure_display} {U : measurableType d} 
  [m n : nat] [f : U -> 'M_(m, n)],
measurable_fun [set: U] f -> measurable_fun [set: U] (fun x : U => - f x)
Statement as written in the source
Lemma measurable_oppmx m n (f : U -> 'M[R]_(m, n)) :
  measurable_fun [set: U] f -> measurable_fun [set: U] (fun x => - f x).
Used by 6 declarations in 3 files
lemma measurable_scalemx source, line 321 
forall {R : realType} {d : measure_display} {U : measurableType d} 
  [m n : nat] [c : U -> R] [f : U -> 'M_(m, n)],
measurable_fun [set: U] c ->
measurable_fun [set: U] f -> measurable_fun [set: U] (fun x : U => c x *: f x)
Statement as written in the source
Lemma measurable_scalemx m n (c : U -> R) (f : U -> 'M[R]_(m, n)) :
  measurable_fun [set: U] c -> measurable_fun [set: U] f ->
  measurable_fun [set: U] (fun x => c x *: f x).
Used by 14 declarations in 8 files
lemma measurable_mulmx source, line 330 
forall {R : realType} {d : measure_display} {U : measurableType d} 
  [m n p : nat] [f : U -> 'M_(m, n)] [g : U -> 'M_(n, p)],
measurable_fun [set: U] f ->
measurable_fun [set: U] g -> measurable_fun [set: U] (fun x : U => f x *m g x)
Statement as written in the source
Lemma measurable_mulmx m n p (f : U -> 'M[R]_(m, n)) (g : U -> 'M[R]_(n, p)) :
  measurable_fun [set: U] f -> measurable_fun [set: U] g ->
  measurable_fun [set: U] (fun x => f x *m g x).
Used by 9 declarations in 6 files

The norm of a real matrix is the largest absolute value of an entry.

sectionmx_norm
Context {R : realType}.
lemma mx_norm_entry_le main result source, line 345 
forall {R : realType} [m n : nat] (x : 'M_(m, n)) (i : 'I_m) (j : 'I_n), `|x i j| <= `|x|
Main result, as the README states it

For the norm of a real matrix: every entry is bounded by the norm, |A B| <= n |A| |B| when A has n columns, |col_mx P Q| <= |P| + |Q|, and permuting the columns does not increase the norm.

Used in theories/ by: Gaussian/Law/LibraryBridge
Statement as written in the source
Lemma mx_norm_entry_le m n (x : 'M[R]_(m, n)) i j : `|x i j| <= `|x|.
Used by 30 declarations in 16 files
lemma mx_norm_col_perm_le main result source, line 351 
forall {R : realType} [m n : nat] (s : {perm 'I_n}) (x : 'M_(m, n)),
`|col_perm s x| <= `|x|
Main result

Stated in the README together with mx_norm_entry_le.

Statement as written in the source
Lemma mx_norm_col_perm_le m n (s : 'S_n) (x : 'M[R]_(m, n)) :
  `|col_perm s x| <= `|x|.
Used by 1 declaration in 1 file
lemma mx_norm_col_mx_le main result source, line 360 
forall {R : realType} [m1 m2 n : nat] (P : 'M_(m1, n)) (Q : 'M_(m2, n)),
`|col_mx P Q| <= `|P| + `|Q|
Main result

Stated in the README together with mx_norm_entry_le.

Statement as written in the source
Lemma mx_norm_col_mx_le m1 m2 n (P : 'M[R]_(m1, n)) (Q : 'M[R]_(m2, n)) :
  `|col_mx P Q| <= `|P| + `|Q|.
Used by 1 declaration in 1 file
lemma mx_norm_mulmx_le main result source, line 371 
forall {R : realType} [m n p : nat] (A : 'M_(m, n)) (B : 'M_(n, p)),
`|A *m B| <= n%:R * `|A| * `|B|
Main result

Stated in the README together with mx_norm_entry_le.

Statement as written in the source
Lemma mx_norm_mulmx_le m n p (A : 'M[R]_(m, n)) (B : 'M[R]_(n, p)) :
  `|A *m B| <= n%:R * `|A| * `|B|.
Used by 8 declarations in 4 files
lemma mx_norm_exprn_le source, line 383 
forall {R : realType} [m n : nat] (x : 'M_(m, n)) (k : nat),
`|x| ^+ k <= 1 + \sum_ij `|x ij.1 ij.2| ^+ k
Statement as written in the source
Lemma mx_norm_exprn_le m n (x : 'M[R]_(m, n)) k :
  `|x| ^+ k <= 1 + \sum_(ij : 'I_m * 'I_n) `|x ij.1 ij.2| ^+ k.
Used by 1 declaration in 1 file
lemma continuous_mxP main result source, line 401 
forall {R : realType} {T : topologicalType} [m n : nat] [f : T -> 'M_(m, n)],
(forall (i : 'I_m) (j : 'I_n), continuous (fun x0 : T => f x0 i j)) -> continuous f
Main result, as the README states it

A map into real matrices is continuous if each of its entries is, and the matrix product is continuous in each factor.

Statement as written in the source
Lemma continuous_mxP {T : topologicalType} m n (f : T -> 'M[R]_(m, n)) :
  (forall i j, continuous (fun x => f x i j)) -> continuous f.
Used by 1 declaration in 1 file
lemma continuous_mulmxr main result source, line 415 
forall {R : realType} [m n p : nat] [B : 'M_(n, p)], continuous (mulmx^~ B)
Main result

Stated in the README together with continuous_mxP.

Statement as written in the source
Lemma continuous_mulmxr m n p (B : 'M[R]_(n, p)) :
  continuous (fun A : 'M[R]_(m, n) => A *m B).
Used by 14 declarations in 8 files
lemma continuous_mulmxl main result source, line 429 
forall {R : realType} [m n p : nat] [A : 'M_(m, n)], continuous [eta mulmx A]
Main result

Stated in the README together with continuous_mxP.

Statement as written in the source
Lemma continuous_mulmxl m n p (A : 'M[R]_(m, n)) :
  continuous (fun B : 'M[R]_(n, p) => A *m B).
Used by 1 declaration in 1 file
sectioncontinuous_measurable_mx
Context {R : realType} {m n : nat}.
let rbox section-local source, line 448 
Let rbox (q : 'M[rat]_(m, n)) (r : rat) : set 'M[R]_(m, n) :=
  mxbox (fun i j => [set x : R | `|ratr (q i j) - x| < ratr r]).
Used by 2 declarations in 1 file
let measurable_rbox section-local source, line 451 
Let measurable_rbox q r : measurable (rbox q r).
Used by 1 declaration in 1 file
lemma open_measurable_mx source, line 460 
forall {R : realType} {m n : nat} [V : set 'M_(m, n)],
open V -> (measure_matrix_display default_measure_display).-measurable V
Statement as written in the source
Lemma open_measurable_mx (V : set 'M[R]_(m, n)) : open V -> measurable V.
Used by 1 declaration in 1 file
lemma continuous_measurable_mx main result source, line 492 
forall {R : realType} {m n : nat} [f : 'M_(m, n) -> R],
continuous f -> measurable_fun [set: 'M_(m, n)] f
Main result, as the README states it

A continuous real function of a real matrix is measurable: the open sets of 'M[R]_(m, n) are measurable.

Used in theories/ by: Gaussian/Orthogonal/EqualCovariance
Statement as written in the source
Lemma continuous_measurable_mx (f : 'M[R]_(m, n) -> R) :
  continuous f -> measurable_fun [set: 'M[R]_(m, n)] f.
Used by 61 declarations in 25 files
Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.