On this page

Glossary

The definitions and notations that the file headers introduce, each with its one-line reading, in the MathComp style of documentation headers. Names link to their definitions; the file column links to the header.

gaussian/10 entries

measure_matrix_display d	display 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	measurable_matrix
mxbox A	the 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)	measurable_matrix
mxboxes T	the boxes mxbox A with measurable sides A i j	measurable_matrix
rV_cons p	the row vector of size n.+1 with first coordinate p.1, and then the coordinates of p.2 : 'rV_n	gauss
gauss n	the standard Gaussian measure on 'rV[R]_n	gauss
rV_prefix k h	the row vector h with its coordinates of index k or more set to 0	partial_derivative
lebesgue_rV_cons m	the image of lebesgue_measure \x m under rV_cons, for a sigma-finite measure m on 'rV[R]_n	lebesgue_rV
lebesgue_rV_rec n	Lebesgue measure on 'rV[R]_n as a sigma-finite measure, by recursion on n	lebesgue_rV
lebesgue_rV n	the function of lebesgue_rV_rec n, with the same structure; the lemmas are stated for it	lebesgue_rV
gauss_pdf x	(2 pi)^(-n/2) exp (- mxdot x x / 2), the density of gauss n with respect to lebesgue_rV n	lebesgue_rV

comparison/43 entries

centered_chi2 a x	\sum_i a_i (x_i^2 - 1), for a x : 'rV[R]_n	chi_square
row_tail a	the row of the coordinates 1, ..., n of a : 'rV[R]_n.+1	gauss_linear
gauss_smooth eps G x	E[G (x + eps y)], y of law gauss n	gauss_smoothing
gauss_smooth_partial eps G j x	E[G (x + eps y) y_j] / eps	gauss_smoothing
clip k x	the point of [-k, k] closest to x	gauss_concentration
rmax z	the largest coordinate of the row vector z	slepian
lse b z	b^-1 * ln (\sum_j expR (b * z 0 j))	slepian
softmax b z j	expR (b * z 0 j) / \sum_i expR (b * z 0 i)	slepian
incr_var A j l	(A^T *m A) j j + (A^T *m A) l l - 2 * (A^T *m A) j l, the variance of (x *m A) 0 j - (x *m A) 0 l	slepian
minmax Z	min_u max_t Z u t, for Z : 'M[R]_(p.+1, q.+1)	gordon
gsum b z u	\sum_t expR (b * z 0 (mxvec_index u t))	gordon
gtot b z	\sum_u (gsum b z u)^-1	gordon
smm b z	- b^-1 * ln (gtot b z), the soft min-max of vec_mx z	gordon
gq b z u	(gsum b z u)^-1 / gtot b z, weights of the soft min	gordon
gp b z u t	expR (b * z 0 (mxvec_index u t)) / gsum b z u, weights of the soft max of the row u	gordon
smm_D b z u t	gq b z u * gp b z u t, the partial derivative of smm b along mxvec_index u t	gordon
smm_D2 b z u t v s	the partial derivative of z |-> smm_D b z u t along mxvec_index v s	gordon
unvec k	the pair (i, j) such that mxvec_index i j = k	escape
fam_mx xs	the matrix whose columns are the vectors xs u	escape
bil_mx xs ys	the matrix B such that vec_mx (a *m B) u t is ys t ^T *m vec_mx a *m xs u	escape
aux_mx xs ys	the matrix C such that vec_mx (z *m C) u t is <lsubmx z, ys t> + <rsubmx z, xs u>	escape
gwidth_fun T h	sup_(x in T) <h, x>, for h : 'rV[R]_M	escape
escape_inf T G	inf_(x in T) |G *m x|	escape
minmax_sph T Y G	inf_(x in T) sup_(y in Y) <y, G *m x>	escape
range_sphere P	the unit vectors y of 'cV[R]_N with P *m y = y	escape
cgmt_aux K g h	inf_(x in K) (|g| |x| - <h, x>)_+	cgmt
tr_set K	the set of the transposes x^T of the x in K	cgmt
infsup S T F	inf_(s in S) sup_(t in T) F s t	cgmt
auxg_mx rs cs	the matrix C such that vec_mx (z *m C) u t is |rs u| <lsubmx z, cs t> + |cs t| <rsubmx z, rs u>	cgmt
auxgT_mx rs cs	the same with the two blocks of z exchanged	cgmt
bilg_mx rs cs B	the matrix C such that vec_mx (w *m C) u t is vec_mx (lsubmx w *m B) u t + rsubmx w 0 0 |rs u| |cs t|	cgmt
cone_sup K h	sup_(x in K, |x| <= 1) <h, x>, for h : 'rV[R]_M	cone_escape
separated dist K eps s	s is a list of distinct points of K, pairwise more than eps apart for dist	sudakov
lipschitz_pos	the sets [set x | 0 < Phi x], for Phi : 'rV[R]_k -> R nonnegative and Lipschitz for the Euclidean norm	gauss_law
tuple_mx t	the n x m matrix whose rows are the vectors of t	gauss_matrix_law
mehler_kernel r x y	the density at y, against normal_prob 0 1, of the law of r x + sqrt (1 - r^2) Z, |r| < 1	ornstein_uhlenbeck
mehler r f x	E[f (r x + b Z)], with b = sqrt (1 - r^2)	ornstein_uhlenbeck
mehler_d1 r f x	r / b * E[f (r x + b Z) Z], the derivative of mehler r f at x	ornstein_uhlenbeck
mehler_d2 r f x	r^2 / b^2 * E[f (r x + b Z) (Z^2 - 1)]	ornstein_uhlenbeck
mehler_d3 r f x	r^3 / b^3 * E[f (r x + b Z) (Z^3 - 3 Z)]	ornstein_uhlenbeck
mehler_dr r f x	E[f (r x + b Z) (x Z / b - r (Z^2 - 1) / b^2)], the derivative of r |-> mehler r f x	ornstein_uhlenbeck
ou t f x	mehler (expR (- t)) f x	ornstein_uhlenbeck
mehler_bound r1 X	a constant C such that the kernel times a polynomial factor of degree 3 is at most C expR (c |y|) for |r| <= r1 < 1, |x| <= X	ornstein_uhlenbeck

matrix/47 entries

mxdot A B	the Frobenius inner product of A, B : 'M[R]_(m, n), \sum_i \sum_j A i j * B i j	euclidean
frobenius A	the Frobenius norm Num.sqrt (mxdot A A) of A; the Euclidean norm when A is a row or a column vector	euclidean
M \is orthogonalmx	the square matrix M is orthogonal: M *m M^T = 1	euclidean
householder w	the Householder reflection 1 - (2 / mxdot w w) *: (w *m w^T) of w : 'cV[R]_n, equal to 1 when w = 0	real_spectral
sym_spectralmx A	an orthogonal matrix P such that A = P^T *m diag_mx (sym_spectral_diag A) *m P when A is symmetric	real_spectral
sym_spectral_diag A	the eigenvalues of A, in the order of the rows of sym_spectralmx A	real_spectral
whitening_mx S	diag_mx (\row_i (Num.sqrt (d 0 i))^-1) *m P for the chosen spectral decomposition S = P^T diag_mx d P (sym_spectralmx, sym_spectral_diag)	whitening
opnorm A	the operator norm of A, the supremum of frobenius (A *m x) over the columns x with frobenius x <= 1	opnorm
lambda_max A	the supremum of mxdot x (A *m x) over the columns x with mxdot x x = 1; the largest eigenvalue of a symmetric A	lambda_max
orthoprojmx P	P is an orthogonal projection: symmetric and P P = P	psd_splitting
nonneg_part x	1 if x >= 0 and 0 otherwise	psd_splitting
is_net S N eps	every x in S has a point y of N with frobenius (x - y) <= eps	nets
unit_ball n	the closed unit ball [set x | frobenius x <= 1] of 'cV[R]_n	nets
unit_sphere n	the unit sphere [set x | frobenius x = 1] of 'cV[R]_n	nets
budget n k	the lists of n natural numbers with sum at most k	nets
sign_lists n	the lists of n booleans	nets
grid_point h (a, s)	the column with coordinates (-1)^(s_i) h a_i	nets
grid_code h x	the code (a, s) of the column x: a_i is the integer part of |x_i| / h, and s_i says whether x_i < 0	nets
grid_codes n k	the codes (a, s) with a in budget n k	nets
sym_part A	(A + A^T) / 2, the symmetric part of a square matrix	random_opnorm
colmax A	max_j |A e_j|, the largest Euclidean norm of a column of A, the norm of A from l^1 to l^2	covering
colsum_mx g w y	the m x q matrix whose column j is sum_i y_(g i j) w_i	covering
spec_seq A	the sorted list of the eigenvalues of A	von_neumann
spec A	the eigenvalues of the symmetric matrix A, in decreasing order	von_neumann
psdmx A	A is symmetric with x^T A x >= 0 for every x	psd_part
pos_row d	the row of the (d_i)_+	psd_part
psd_part A	the positive part of A	psd_part
nuclear A	sup of <A, B> over the B with opnorm B <= 1	nuclear
coef_map W D	the row (<W_i, D>)_i	nuclear
coef_adj W l	sum_i l_i W_i, the adjoint of coef_map W	nuclear
itv_dist a b x	the distance from x to the interval [a, b]	condition_cone
clamp a b x	the nearest point of [a, b] to x	condition_cone
cond_cone C	the symmetric Q with t I <= Q <= C t I, some t >= 0	condition_cone
cond_cone_vec C	the same cone in the coordinates of mxvec	condition_cone
cond_energy C t H	sum_i itv_dist t (C t) (spec H 0 i) ^ 2	condition_cone
cond_dist C H	the infimum of cond_energy C t H over t >= 0	condition_cone
cond_clip C t H	H with its eigenvalues clipped to [t, C t]	condition_cone
cond_support C A	sup of <A, Q> over the Q of the cone with |Q|_F <= 1	condition_cone
cond_slice C	the Q of the cone with trace n	condition_cone
cond_slice_vec C	the same slice in the coordinates of mxvec	condition_cone
trace_scale a S	S + a (tr S / n) I	trace_projection
trace_quad c H S	2 <H, S> - |S|_F^2 - (c / n) (tr S)^2	trace_projection
trace_argmax K c H	the maximizer of trace_quad c H on K	trace_projection
select_rows P S	the rows of P indexed by the set S, a matrix with #|S| rows	tensor_packing
rowproj V	V^T V, the orthogonal projection on the span of the rows of V when V V^T = 1	tensor_packing
rowperp V	1 - V^T V	tensor_packing
mxcoef A Z	the row of the inner products <Z, A_k>, k < r	tensor_packing

probability/64 entries

tuple_cons p	the tuple p.1 :: p.2 of size n.+1, for p : T * n.-tuple T	lindeberg
tuple_prod mu n	the product of the probability measures mu 0, ..., mu n.-1 on n.-tuple T: the law of n independent random elements with laws mu 0, ..., mu n.-1	lindeberg
tuple_set x i t	the tuple x with its coordinate i replaced by t	lindeberg
subgaussian P X K	0 < K, X is measurable and E exp (X^2 / K^2) <= 2	subgaussian
subexponential P X L	0 < L, X is measurable and E exp (|X| / L) <= 2	subgaussian
psi2_norm P X	the infimum of the K with subgaussian P X K	subgaussian
mixture_weights w	w i >= 0 for every i and \sum_i w i = 1	mixture
mixture P hw	for hw : mixture_weights w, the probability A |-> \sum_i w i P i (A)	mixture
cmixture_weights p	p s >= 0 for every s and \sum_(s <oo) p s = 1	countable_mixture
cmixture P hp	for hp : cmixture_weights p, the probability A |-> \sum_(s <oo) p s P s (A)	countable_mixture
cmixture_tail p m	r_m = \sum_(s > m) p s, the weight of the labels above m	countable_mixture
cmixture_tail_w p m s	p s / r_m for s > m and 0 otherwise, the weights of the normalized tail	countable_mixture
labels_le n m	the n-tuples of labels in nat that are all <= m	countable_mixture
tv_dist P Q	sup {|P A - Q A| : A measurable}, a real number	total_variation
atoms P	the set of the points x with P [set x] != 0	atoms
unif_mean f	#|T|^-1 * \sum_(x : T) f x, the mean of f : T -> R under the uniform law of the finite type T	finite_mean
unif_var f	unif_mean (fun x => (f x - unif_mean f) ^+ 2)	finite_mean
row_index i j	the index i * d + j of 'I_(n * d), for i : 'I_n and j : 'I_d	tuple_rows
tuple_rows n d x	the n rows of length d of the (n * d)-tuple x	tuple_rows
tuple_map g x	[tuple g i (tnth x i) | i < n], for x : n.-tuple T and g : nat -> T -> T'	tuple_rows
semicircle_pdf r x	2 / (pi r^2) sqrt (r^2 - x^2), zero outside [-r, r] since Num.sqrt is zero on negative numbers; the indicator of [0, 1] if r = 0	semicircle_law
semicircle_prob r	the measure with density semicircle_pdf r with respect to Lebesgue measure	semicircle_law
upper_moment mu k w	\int[mu]_x ((x - w)_+)^k, the upper partial moment of order k at w: m(w) for k = 1, s(w) for k = 2	variational
upper_energy mu c w	s(w) + c m(w)^2	variational
upper_cutoff mu c z	sup {w | w + z <= c m(w)}, the solution of w + z = c m(w) when c > -1	variational
upper_value mu c z	upper_energy mu c (upper_cutoff mu c z), the value of the variational problem	variational
upper_admissible mu	the measurable f >= 0 with f^2 integrable and E f > 0	variational
upper_ratio mu c z f	(E (X + z) f(X))_+^2 / (E f(X)^2 + c (E f(X))^2)	variational
empirical s	the average of the Dirac masses at the elements of s	variational
empirical_fun g	empirical [seq g i | i <- enum 'I_d]	variational
clip_energy mu C t	s(-t) + s(C t)	variational
clip_value mu C	the infimum of clip_energy mu C t over t >= 0	variational
clip_profile C a t x	min (max (x - a) t) (C t)	clip_profile
clip_admissible C q	q measurable, t <= q <= C t, some t >= 0	clip_profile
clip_admissible_ae mu C q	q measurable, t <= q <= C t mu-a.e., some t >= 0	clip_profile
clip_objective mu c q	2 E[X q] - E[q^2] - c (E q)^2	clip_profile
clip_energy_shift mu C a t	s(-t - a) + s(C t + a)	clip_profile
clip_dual mu c C b	E X^2 + c (1 + c) b^2 - inf_(t >= 0) clip_energy_shift mu C (c b) t	clip_profile
rademacher b	the sign 1 if b, -1 otherwise	symmetrization
rademacher_mean F	2^-n sum_{s : n.-tuple bool} F s, the expectation of F over n independent signs	symmetrization
sign_flip i s	s with its sign i changed	symmetrization
sign_neg s	s with every sign changed	symmetrization
max_norm v	max_j |v j| for v : 'I_m -> R (0 if m = 0)	symmetrization
doubled_law mu n	the laws of n + n coordinates whose two blocks are independent copies of tuple_prod mu n	symmetrization
tuple_left z, tuple_right z	the two blocks of z : (n + n).-tuple T	symmetrization
ramp u x	min 1 (max 0 (|x| / u - 1))	small_ball_method
small_ball_event n f c	the x : n.-tuple T for which some f_j has sum_k f_j(x_k)^2 < c	small_ball_method
tuple_box A	the n-tuples x with x_i in A i for every i	conditioning
tuple_merge S x y	the n-tuple with the coordinates of x in S and those of y outside S	conditioning
tuple_pick f x	the k-tuple (x_(f 0), ..., x_(f (k - 1)))	conditioning
prob_density mu f	f is measurable, nonnegative everywhere, and of integral one against mu	density_law
density_prob mu f	the probability with density f against mu, if prob_density mu f, and mu otherwise	density_law
density_law mu f hf	the probability with density f against mu, for a proof hf of prob_density mu f	density_law
first_min g q k	the first minimizer of g among q 0, ..., q k, with its value	measurable_minimizer
ls_reduced Z P s lambda beta gamma B theta	the objective with a barrier at (theta, ls_bopt theta), the best b for theta	measurable_minimizer
ls_min DV scB B0 D0 Z P s lambda beta gamma	the minimizer over D of ls_reduced	measurable_minimizer
gibbs_mean w H q	the mean of q under the probability on X with weights proportional to w x exp (H x)	log_partition
sign_row s	the row of the signs (if s i then 1 else -1) of s : {ffun 'I_n -> bool}	rademacher_lindeberg
ffun_cons b s	the function on 'I_n.+1 with value b at 0 and s on the other indices	rademacher_lindeberg
wdot w f g	sum_x w x * f x * g x, the inner product of L^2(w)	finite_gap
wvec f	the column (sqrt (w x) * f x)_x, indexed by enum_val	finite_gap
wfun u	x |-> u_(enum_rank x) / sqrt (w x), the inverse of wvec	finite_gap
wbasis k	wfun of the k-th canonical column	finite_gap
wop_mx w L	the matrix of L in the basis wbasis	finite_gap

fourier/21 entries

cmul z w	the complex product of the pairs z and w	charfun
cmod z	the modulus sqrt (z.1 ^ 2 + z.2 ^ 2) of the pair z	charfun
cf_re mu t	\int[mu]_x cos (t * x), the real part of the characteristic function of the law mu at t	charfun
cf_im mu t	\int[mu]_x sin (t * x), its imaginary part	charfun
cf mu t	the pair (cf_re mu t, cf_im mu t)	charfun
cf_norm mu t	the modulus of the characteristic function of mu at t	charfun
conc_fun mu L	sup_a mu [a, a + L], the Levy concentration function	esseen
fejer T z	\int_0^T (1 - t / T) cos (t z) dt, half the Fejer kernel	esseen
sym_diff p	p.1 - p.2, as a measurable function on pairs	gauss_factor
sym_law mu	the law of X - X' for independent X and X' of law mu	gauss_factor
tuple_sum x	the sum of the coordinates of the tuple x	gauss_factor
sum_law mu n	the law of X_0 + ... + X_(n-1) for independent X_k of laws mu k	gauss_factor
gauss_factor_const v lambda eps	the constant C of gauss_factor_le	gauss_factor
cf_rV_re nu theta	\int[nu]_x cos (mxdot x theta)	charfun_rV
cf_rV_im nu theta	\int[nu]_x sin (mxdot x theta)	charfun_rV
cf_rV nu theta	the pair (cf_rV_re nu theta, cf_rV_im nu theta)	charfun_rV
cf_rV_norm nu theta	its modulus cmod (cf_rV nu theta)	charfun_rV
cf_rV_kernel nu w theta	cos <theta, w> cf_rV_re nu theta + sin <theta, w> cf_rV_im nu theta	inversion
cf_rV_density nu w	(2 pi)^-m \int cf_rV_kernel nu w theta dtheta	inversion
cf_rV_density_reg nu s w	the same, with the factor exp (- s^2 |theta|^2 / 2)	inversion
cf_rV_inv_prob h	for h : \int |cf nu| < +oo, the probability with density cf_rV_density nu	inversion

convex/33 entries

rel_open_convex V D	D is convex, y - z is in V for y, z in D, and around each z of D, D contains the points z + h with h in V and `|h| < e for some e > 0: D is relatively open in its affine hull z + V	self_concordant
sc_function V D B	B is a self-concordant function on D with directions V: three times differentiable along V, with a gradient vector and a Hessian matrix, convex, (SC), and B (z + t h) tends to +oo when t tends to 1 from the left, if z + t h is in D for 0 <= t < 1 and z + h is not	self_concordant
sc_barrier V D theta B	B is a theta-self-concordant barrier: a self-concordant function with (BP)	self_concordant
sc_norm B z h	the local norm sqrt (D^2 B(z)[h, h])	self_concordant
bregman_div B y z	the Bregman divergence B y - B z - D B(z)[y - z]	self_concordant
sc_omega r	r - ln (1 + r)	self_concordant
sc_omega_star r	- r - ln (1 - r)	self_concordant
ls_objective Z lambda beta theta b	F_Z(theta, b; beta), the average (2 n)^-1 sum_i (b - <Z_i, theta>)^2 plus the ridge term beta (lambda |theta|^2 + b^2)	least_squares
ls_loss Z P theta b	sum_(i in P) (b - <Z_i, theta>)^2	least_squares
ls_ridge Z P s lambda beta theta b	s ls_loss Z P theta b + beta (lambda |theta|^2 + b^2)	least_squares
ls_barrier_objective Z P s lambda beta gamma B theta b	ls_ridge Z P s lambda beta theta b + gamma B theta; with P the indices other than i and s = (2 n)^-1, the leave-one-out objective F^(i) of the paper	least_squares
ls_barrier_value Z lambda beta D gamma B	Phi_Z(D, B; beta, gamma), the infimum of F_Z(theta, b; beta) + gamma B theta over theta in D and b real	least_squares
ls_value Z lambda beta D	Phi_Z(D; beta), the infimum of F_Z(theta, b; beta) over theta in D and b real; Phi_Z(D) is ls_value Z lambda 0 D, for any lambda	least_squares
regular_feature K tau Sigma mu	the law mu on 'rV[R]_N is a (K, tau)-regular feature with covariance Sigma: lambda = opnorm Sigma > 0, (F1) E <Z, theta>^4 <= K^4 lambda^2 |theta|^4, mean 0, E <Z, theta> <Z, theta'> = theta Sigma theta'^T and (F2) Var (Z T Z^T) <= tau^2 |T|_F^2 for T symmetric	least_squares
posdefmx A	A is symmetric positive definite: 0 < x A x^T for every row vector x != 0	logdet_barrier
pd_slice n s	the matrices A (as mxvec A) that are positive definite with trace s	logdet_barrier
logdet_barrier n x	- ln (det (vec_mx x)), for x : 'rV[R]_(n * n)	logdet_barrier
pd_slice2 n m M	the matrices A (as mxvec A) of trace n with A - m I and M I - A positive definite	logdet_barrier
logdet_barrier2 n m M x	- ln det (A - m I) - ln det (M I - A) + n ln ((1 - m) (M - 1)), with A = vec_mx x	logdet_barrier
sym_traceless n	the subspace of the mxvec of the symmetric matrices of trace 0	logdet_barrier
logsum l c t	c - sum_i ln (1 + t l_i), for l : 'rV[R]_k	logdet_barrier
ls_grad Z P s lambda beta theta b h c	the first variation of the ridge objective at (theta, b) in the direction (h, c)	minimizers
ls_bopt Z P s beta theta	the b that minimizes the ridge objective for a fixed theta	minimizers
ins_alpha E z	the row (1, - z E^T): <ins_alpha E z, w> is c - <z, y E>, the change of the residual of z	ls_insertion
ins_hform ... w w'	the Hessian of F^(i) at the minimizer, as a bilinear form of the coordinates	ls_insertion
ins_hessian ...	its matrix H^(i)	ls_insertion
ins_ell ... z	l_i(z) = <alpha(z), H^-1 alpha(z)>	ls_insertion
ins_r ... z	r_i(z) = b_m - <z, theta_m>, the residual	ls_insertion
ins_cost ... z	Delta_i(z), the insertion cost	ls_insertion
ins_c0, ins_v, ins_T	the coefficients of l_i as a quadratic polynomial	ls_insertion
hybrid mu nu k	the laws of the coordinates of the Lindeberg argument: mu before the coordinate k, nu from k on	barrier_lindeberg
proj K z	the nearest point of K to z, if it exists (xget)	moreau
polar C	the polar cone [set u | <u, y> <= 0 for every y in C]	moreau

random_matrix/25 entries

goe_mx a	the GOE matrix (A + A^T) / sqrt (2 d) of a row vector a of size d * d, A = vec_mx a	goe
polyfun F	F is continuous with |F x| <= C (1 + |x|^k)	goe
mx_polyfun A	every entry of the matrix function A is a polyfun	goe
mxpow_deriv W E k	\sum_(r < k) W ^+ r *m E *m W ^+ (k.-1 - r)	goe
goe_form_mx xs	the matrix of the process x_j^T W x_j, W = goe_mx a: (a *m goe_form_mx xs) 0 j = x_j^T W x_j	goe_edge
goe_lin_mx xs	(2 / sqrt d) times the matrix whose columns are the x_j, the matrix of the process (2 / sqrt d) <g, x_j>	goe_edge
conj_equivariant F	F (Q W Q^T) = Q F(W) Q^T for every orthogonal Q and every symmetric W	goe_rotation
diag_var A	(1 / n) \sum_j (A_jj - tr A / n)^2, the empirical variance of the diagonal of A : 'M_n	goe_rotation
goe_stat f a	(1 / d) \sum_i f (spec (goe_mx a) 0 i), the empirical mean of f over the spectrum of the GOE matrix goe_mx a	wigner
tuple_mx x	the N x n matrix with rows x_1, ..., x_N	restricted_isometry
supp u	the support of u : 'rV[R]_N	restricted_isometry
restr E u	u restricted to the coordinates in E	restricted_isometry
gram_off x u v	<u X, v X> - sum_i u_i v_i |x_i|^2, the off-diagonal part of the Gram form, sum_(i <> j) u_i v_j <x_i, x_j>	restricted_isometry
maxnorm x	max_i |x_i|	restricted_isometry
sparse_ball m	the m-sparse vectors of norm at most 1	restricted_isometry
rip_const m x	B_m^2 = sup over sparse_ball m of |gram_off x u u|	restricted_isometry
rip_T beta K	2100 K psi sqrt m (ln (e N / m) + ln (1 / beta))	restricted_isometry
sqnorm_dev x	max_i | |x_i|^2 - 1 |	restricted_isometry
sparse_emb w	the vector supported in F with coordinates w, for w : 'cV_#|F| (in the order of enum_val)	restricted_isometry
sparse_proj F z	the coordinates of z in F	restricted_isometry
tuple_submx F x	the n x |F| matrix with columns x_i, i in F	restricted_isometry
sphere_net k	a 1/4-net of the unit sphere of 'cV_k of size at most (18 e)^k	restricted_isometry
sparse_norm_bound m s	8 K sqrt (m (1 + ln (N / m)) + 6 (m + n) + s)	restricted_isometry
sym_dilation B	the symmetric matrix [[0, B], [B^T, 0]] of size m + p of B : 'M[R]_(m, p)	matrix_series
goe_coef i j	the row vector c of 'rV[R]_(d * d) such that goe_mx a i j = <a, c> for every a	goe_entries

applications/1 entries

pressure_energy G x

sum_mu f ((G x)_mu / sqrt N), the energy of the spins x for the patterns G

Pressure