GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisprobabilityfinite_gap

Spectral gaps on a finite space

GaussianAnalysis.probability.finite_gaplibrary/probability/finite_gap.v256 lines16 lemmas and theorems, 5 definitionssource
Imports 3 library modules and 11 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, mathcomp.classical.boolp, mathcomp.reals.reals, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 1

For a finite type X and weights w x > 0, wdot w f g = sum_x w x f x g x is the inner product of L^2(w). The map f |-> (sqrt (w x) f x)_x (wvec, with inverse wfun) is an isometry of L^2(w) onto 'cV[R]_#|X| (mxdot_wvec), and an operator L on the functions on X has the matrix wop_mx w L in the basis wbasis that wvec maps to the canonical basis (wop_mx_mul, wop_mx_form).

Let L be linear, self-adjoint in L^2(w) and nonnegative: <f, L g>_w = <L f, g>_w and <f, L f>_w >= 0. If k <f, L f>_w <= <L f, L f>_w for every f, then

k <f, f>_w <= <f, L f>_w

for every f orthogonal to the kernel of L (wgap_from_square): the matrix of L is symmetric and positive semidefinite, and psd_square_gap of matrix/spectral_gap.v applies to it. If moreover the weights sum to one and the kernel of L is the constants, this is the Poincare inequality

k Var_w(f) <= <f, L f>_w

(wpoincare_from_square): a bound of the Dirichlet form by the norm of the generator gives a spectral gap.

Part of target T4 of phase 12: a Rocq formalization of the credited argument of the end of the proof of the proposition 'Gap and covariance under scaled interactions and fields' (rcut:prop:uniform-gap) of 'Cutoff throughout the high-temperature Sherrington-Kirkpatrick phase' (family 227 of the OpenAI math collection, revision 1581d4cbd, file appendices/entropy.tex). The manuscript reads ||A f||^2 >= kappa <f, A f> as a spectral gap of the self-adjoint nonnegative operator A, whose kernel is the constants, by applying it to the eigenfunctions; here the spectral theorem enters through the matrix of the operator. It follows the TeX, not a Lean module of the collection.

wdot w f gsum_x w x * f x * g x, the inner product of L^2(w)
wvec fthe column (sqrt (w x) * f x)_x, indexed by enum_val
wfun ux |-> u_(enum_rank x) / sqrt (w x), the inverse of wvec
wbasis kwfun of the k-th canonical column
wop_mx w Lthe matrix of L in the basis wbasis

Main results

ResultsStatement
wgap_from_squarewpoincare_from_square
Spectral gaps on a finite space. For a finite type X, weights w x > 0 and an operator L on the functions on X that is linear, self-adjoint in L^2(w) (<f, L g>_w = <L f, g>_w, with <f, g>_w = sum_x w x f x g x) and nonnegative (<f, L f>_w >= 0): if k <f, L f>_w <= <L f, L f>_w for every f, then k <f, f>_w <= <f, L f>_w for every f orthogonal to the kernel of L. If moreover the weights sum to one and the kernel of L is the constants, then k Var_w(f) <= <f, L f>_w for every f (a Poincare inequality). A Rocq formalization of the credited argument of a proposition of family 227 of the OpenAI math collection (see the header).
wdotwvecwfunmxdot_wvecwop_mxwop_mx_mulwop_mx_formwop_mx_sym
The isometry f |-> (sqrt (w x) f x)_x of L^2(w) onto 'cV[R]_#|X| and its inverse, and the matrix wop_mx w L of an operator in the corresponding basis: wop_mx w L *m wvec f = wvec (L f) and u^T (wop_mx w L) u = <wfun u, L (wfun u)>_w for a linear L, symmetric when L is self-adjoint.

Declarations21 exported

lemma, theoremdefinitioninstancelocal
sectionfinite_gap
Context {R : realType} {X : finType}.
Variable w : X -> R.
Local Notation N := #|X|.
definition wdot main result source, line 63
Type
forall {R : realType} {X : finType}, (X -> R) -> (X -> R) -> (X -> R) -> R
Definition
Definition wdot (f g : X -> R) : R := \sum_x w x * f x * g x.

The inner product of L^2(w): <f, g>_w = sum_x w x f x g x.

Main result, as the README states it

The isometry f |-> (sqrt (w x) f x)_x of L^2(w) onto 'cV[R]_#|X| and its inverse, and the matrix wop_mx w L of an operator in the corresponding basis: wop_mx w L *m wvec f = wvec (L f) and u^T (wop_mx w L) u = <wfun u, L (wfun u)>_w for a linear L, symmetric when L is self-adjoint.

Used by 14 declarations in 2 files
lemma wdotC source, line 65 
forall {R : realType} {X : finType} (w f g : X -> R), wdot w f g = wdot w g f
Statement as written in the source
Lemma wdotC f g : wdot f g = wdot g f.
Used by 2 declarations in 2 files
definition wvec main result source, line 70
Type
forall {R : realType} {X : finType}, (X -> R) -> (X -> R) -> 'cV_#|X|
Definition
Definition wvec (f : X -> R) : 'cV[R]_N :=
  \col_k (Num.sqrt (w (enum_val k)) * f (enum_val k)).

The map f |-> (sqrt (w x) f x)_x of L^2(w) onto 'cV[R]_N, and its inverse.

Main result

Stated in the README together with wdot.

Used by 6 declarations in 1 file
definition wfun main result source, line 73
Type
forall {R : realType} {X : finType}, (X -> R) -> 'cV_#|X| -> X -> R
Definition
Definition wfun (u : 'cV[R]_N) (x : X) : R :=
  u (enum_rank x) 0 / Num.sqrt (w x).
Main result

Stated in the README together with wdot.

Used by 8 declarations in 1 file
Hypothesis w0 : forall x, 0 < w x.
lemma sqrt_w_gt0 source, line 78 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) -> forall x : X, 0 < Num.ExtraDef.sqrtr (w x)
Statement as written in the source
Lemma sqrt_w_gt0 x : 0 < Num.sqrt (w x).
Used by 4 declarations in 1 file
lemma wvecK source, line 81 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) -> forall u : 'cV_#|X|, wvec w (wfun w u) = u
Statement as written in the source
Lemma wvecK u : wvec (wfun u) = u.
Used by 2 declarations in 1 file
lemma wfunK source, line 88 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) -> forall f : X -> R, wfun w (wvec w f) = f
Statement as written in the source
Lemma wfunK f : wfun (wvec f) = f.
Used by 1 declaration in 1 file
lemma sum_enum_val source, line 95 
forall {R : realType} {X : finType} (F : X -> R),
\sum_(k < #|X|) F (enum_val k) = \sum_x F x
Statement as written in the source
Lemma sum_enum_val (F : X -> R) : \sum_(k < N) F (enum_val k) = \sum_x F x.
Used by 1 declaration in 1 file
lemma mxdot_wvec main result source, line 101 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) -> forall f g : X -> R, mxdot (wvec w f) (wvec w g) = wdot w f g
Main result

Stated in the README together with wdot.

Statement as written in the source
Lemma mxdot_wvec f g : mxdot (wvec f) (wvec g) = wdot f g.
Used by 2 declarations in 1 file
lemma wvec_eq0 source, line 108 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) -> forall [f : X -> R], wvec w f = 0 -> forall x : X, f x = 0
Statement as written in the source
Lemma wvec_eq0 f : wvec f = 0 -> forall x, f x = 0.
Used by 1 declaration in 1 file
definition wbasis source, line 117
Type
forall {R : realType} {X : finType}, (X -> R) -> 'I_#|X| -> X -> R
Definition
Definition wbasis (k : 'I_N) : X -> R := wfun (delta_mx k 0).

The basis of L^2(w) that wvec maps to the canonical basis, and the inner products with it.

Used by 3 declarations in 1 file
lemma wfun_sum source, line 119 
forall {R : realType} {X : finType} (w : X -> R) (u : 'cV_#|X|),
wfun w u = (fun x : X => \sum_k u k 0 * wbasis w k x)
Statement as written in the source
Lemma wfun_sum u : wfun u = fun x => \sum_k u k 0 * wbasis k x.
Used by 1 declaration in 1 file
lemma wdot_basis source, line 127 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) ->
forall (k : 'I_#|X|) (g : X -> R),
wdot w (wbasis w k) g = Num.ExtraDef.sqrtr (w (enum_val k)) * g (enum_val k)
Statement as written in the source
Lemma wdot_basis k g :
  wdot (wbasis k) g = Num.sqrt (w (enum_val k)) * g (enum_val k).
Used by 1 declaration in 1 file

A linear operator L on functions, self-adjoint and nonnegative in L^2(w).

Variable L : (X -> R) -> X -> R.
Hypothesis L_lin : forall (a : R) (f g : X -> R) x,
  L (fun y => a * f y + g y) x = a * L f x + L g x.
Hypothesis L_sym : forall f g, wdot f (L g) = wdot (L f) g.
Hypothesis L_ge0 : forall f, 0 <= wdot f (L f).
lemma L_cst0 source, line 150 
forall {R : realType} {X : finType} [L : (X -> R) -> X -> R],
(forall (a : R) (f g : X -> R) (x : X),
 L (fun y : X => a * f y + g y) x = a * L f x + L g x) ->
forall x : X, L (fun=> 0) x = 0
Statement as written in the source
Lemma L_cst0 x : L (fun _ => 0) x = 0.
Used by 1 declaration in 1 file
lemma L_sum source, line 159 
forall {R : realType} {X : finType} [L : (X -> R) -> X -> R],
(forall (a : R) (f g : X -> R) (x : X),
 L (fun y : X => a * f y + g y) x = a * L f x + L g x) ->
forall [I : finType] (c : I -> R) (h : I -> X -> R) (x : X),
L (fun y : X => \sum_i c i * h i y) x = \sum_i c i * L (h i) x
Statement as written in the source
Lemma L_sum (I : finType) (c : I -> R) (h : I -> X -> R) x :
  L (fun y => \sum_i c i * h i y) x = \sum_i c i * L (h i) x.
Used by 1 declaration in 1 file
definition wop_mx main result source, line 176
Type
forall {R : realType} {X : finType}, (X -> R) -> ((X -> R) -> X -> R) -> 'M_#|X|
Definition
Definition wop_mx : 'M[R]_N := \matrix_(k, l) wdot (wbasis k) (L (wbasis l)).

The matrix of L in the basis wbasis.

Main result

Stated in the README together with wdot.

Used by 4 declarations in 1 file
lemma wop_mx_mul main result source, line 178 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) ->
forall [L : (X -> R) -> X -> R],
(forall (a : R) (f g : X -> R) (x : X),
 L (fun y : X => a * f y + g y) x = a * L f x + L g x) ->
forall u : 'cV_#|X|, wop_mx w L *m u = wvec w (L (wfun w u))
Main result

Stated in the README together with wdot.

Statement as written in the source
Lemma wop_mx_mul u : wop_mx *m u = wvec (L (wfun u)).
Used by 2 declarations in 1 file
lemma wop_mx_sym main result source, line 185 
forall {R : realType} {X : finType} [w : X -> R] [L : (X -> R) -> X -> R],
(forall f g : X -> R, wdot w f (L g) = wdot w (L f) g) -> wop_mx w L \is symmetricmx
Main result

Stated in the README together with wdot.

Statement as written in the source
Lemma wop_mx_sym : wop_mx \is symmetricmx.
Used by 1 declaration in 1 file
lemma wop_mx_form main result source, line 191 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) ->
forall [L : (X -> R) -> X -> R],
(forall (a : R) (f g : X -> R) (x : X),
 L (fun y : X => a * f y + g y) x = a * L f x + L g x) ->
forall u : 'cV_#|X|, mxdot u (wop_mx w L *m u) = wdot w (wfun w u) (L (wfun w u))
Main result

Stated in the README together with wdot.

Statement as written in the source
Lemma wop_mx_form u : mxdot u (wop_mx *m u) = wdot (wfun u) (L (wfun u)).
Used by 1 declaration in 1 file
theorem wgap_from_square main result source, line 198 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) ->
forall [L : (X -> R) -> X -> R],
(forall (a : R) (f g : X -> R) (x : X),
 L (fun y : X => a * f y + g y) x = a * L f x + L g x) ->
(forall f g : X -> R, wdot w f (L g) = wdot w (L f) g) ->
(forall f : X -> R, 0 <= wdot w f (L f)) ->
forall [k : R],
(forall f : X -> R, k * wdot w f (L f) <= wdot w (L f) (L f)) ->
forall [f : X -> R],
(forall g : X -> R, (forall x : X, L g x = 0) -> wdot w g f = 0) ->
k * wdot w f f <= wdot w f (L f)

The gap from a bound of the form by the squared norm, for the functions orthogonal to the kernel.

Main result, as the README states it

Spectral gaps on a finite space. For a finite type X, weights w x > 0 and an operator L on the functions on X that is linear, self-adjoint in L^2(w) (<f, L g>_w = <L f, g>_w, with <f, g>_w = sum_x w x f x g x) and nonnegative (<f, L f>_w >= 0): if k <f, L f>_w <= <L f, L f>_w for every f, then k <f, f>_w <= <f, L f>_w for every f orthogonal to the kernel of L. If moreover the weights sum to one and the kernel of L is the constants, then k Var_w(f) <= <f, L f>_w for every f (a Poincare inequality). A Rocq formalization of the credited argument of a proposition of family 227 of the OpenAI math collection (see the header).

Statement as written in the source
Theorem wgap_from_square (k : R) :
  (forall f, k * wdot f (L f) <= wdot (L f) (L f)) ->
  forall f, (forall g, (forall x, L g x = 0) -> wdot g f = 0) ->
  k * wdot f f <= wdot f (L f).
Used by 1 declaration in 1 file
theorem wpoincare_from_square main result source, line 219 
forall {R : realType} {X : finType} [w : X -> R],
(forall x : X, 0 < w x) ->
forall [L : (X -> R) -> X -> R],
(forall (a : R) (f g : X -> R) (x : X),
 L (fun y : X => a * f y + g y) x = a * L f x + L g x) ->
(forall f g : X -> R, wdot w f (L g) = wdot w (L f) g) ->
(forall f : X -> R, 0 <= wdot w f (L f)) ->
forall [k : R],
\sum_x w x = 1 ->
(forall g : X -> R, (forall x : X, L g x = 0) <-> (forall x y : X, g x = g y)) ->
(forall f : X -> R, k * wdot w f (L f) <= wdot w (L f) (L f)) ->
forall f : X -> R, k * \sum_x w x * (f x - \sum_y w y * f y) ^+ 2 <= wdot w f (L f)

The Poincare inequality, when the weights sum to one and the kernel of L is the constants.

Main result

Stated in the README together with wgap_from_square.

Statement as written in the source
Theorem wpoincare_from_square (k : R) : \sum_x w x = 1 ->
  (forall g, (forall x, L g x = 0) <-> (forall x y, g x = g y)) ->
  (forall f, k * wdot f (L f) <= wdot (L f) (L f)) ->
  forall f, k * \sum_x w x * (f x - \sum_y w y * f y) ^+ 2 <= wdot f (L f).
Used by 1 declaration in 1 file
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.