GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisgaussiangauss

The standard Gaussian measure on row vectors

GaussianAnalysis.gaussian.gausslibrary/gaussian/gauss.v519 lines28 lemmas and theorems, 2 definitionssource
Imports 2 library modules and 27 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.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.sequences, mathcomp.analysis.exp, mathcomp.analysis.numfun, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability

Imported by 46
Required by 28 files of the paper proofs

gauss n is the law of a row vector of n independent standard normal coordinates: the n-fold product of normal_prob 0 1 on 'rV[R]_n, with the sigma-algebra of measurable_matrix.v. It is defined by recursion on n, the first coordinate being drawn first (gaussS). The measure of a box is the product of the measures of its sides (gauss_box), and this property characterizes gauss n among all measures (gauss_unique). Measurable functions of polynomial growth are integrable (integrable_gauss_poly).

The vectors are rows because the linear algebra of MathComp writes them so, with linear maps acting on the right: if x has law gauss n and A is an n x m matrix, then x *m A is a centered Gaussian vector with covariance A^T *m A.

rV_cons pthe row vector of size n.+1 with first coordinate p.1, and then the coordinates of p.2 : 'rV_n
gauss nthe standard Gaussian measure on 'rV[R]_n

Main results

ResultsStatementUsed by theories/
gauss
gauss n, the standard Gaussian measure on 'rV[R]_n: the law of n independent standard normal coordinates, a probability.Gaussian/Law/LibraryBridge, Gaussian/Orthogonal/EqualCovariance, Gaussian/Lipschitz/Concentration, Gaussian/Lipschitz/Variance, Projected/BulkLaw
gauss_boxgauss_unique
gauss n gives the box with sides A i the measure \prod_i normal_prob 0 1 (A i), and it is the only measure on 'rV[R]_n that does.Gaussian/Law/LibraryBridge
ge0_integral_gauss_consintegrable_gauss_consintegral_gauss_cons
Fubini for the first coordinate: the integral against gauss n.+1 is the iterated integral against normal_prob 0 1 and gauss n, and integrability against gauss n.+1 is integrability against the product of the two.Gaussian/Law/LibraryBridge, for Gaussian/Iterated/PolynomialGrowth
gauss_row_mx
Independent blocks: the image of gauss n \x gauss m under (x, y) |-> row_mx x y is gauss (n + m).
gauss_col_permintegral_gauss_col_perm
gauss n, and the integral of every integrable function against it, are invariant under permutations of the coordinates.Gaussian/Law/LibraryBridge, for Gaussian/Iterated/BlockRotation
gauss_lsubmxgauss_rsubmxintegral_gauss_lsubmxintegral_gauss_rsubmx
Marginals of the blocks: if x has law gauss (n + m), then lsubmx x has law gauss n and rsubmx x has law gauss m.
integral_image
If nu is the image of the measure mu under a measurable g, then \int[mu] f (g x) = \int[nu] f y for every nu-integrable f.
gauss_coordintegral_gauss_coord
Each coordinate of a vector of law gauss n has law normal_prob 0 1.
ge0_integral_gauss_prod
Independent coordinates: the integral of \prod_i f i (x 0 i) against gauss n is \prod_i of the integrals of f i against normal_prob 0 1, for nonnegative measurable f i.
integrable_gauss_polypoly_bound_ge0entry_mul_bound
Every measurable function bounded by C (1 + |x|^k) is integrable against gauss n. The constant of such a bound is nonnegative, and multiplying the function by a coordinate raises k by one and doubles C.Gaussian/Law/LibraryBridge

Declarations31 exported, 3 local

lemma, theoremdefinitioninstancelocal
sectionintegral_image
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variables (mu : {measure set T1 -> \bar R}) (nu : {measure set T2 -> \bar R}).
Variable g : T1 -> T2.
Hypothesis mg : measurable_fun [set: T1] g.
Hypothesis gnu : forall A, measurable A -> mu (g @^-1` A) = nu A.
lemma integrable_image source, line 53 
forall [d1 d2 : measure_display] [T1 : measurableType d1] [T2 : measurableType d2]
  [R : realType] [mu : measure T1 R] [nu : measure T2 R] [g : T1 -> T2],
measurable_fun [set: T1] g ->
(forall A : set T2, d2.-measurable A -> mu (g @^-1` A) = nu A) ->
forall [f : T2 -> \bar R], nu.-integrable [set: T2] f -> mu.-integrable [set: T1] (f \o g)

If nu is the image of mu under g, integrating f against nu is integrating f \o g against mu.

Statement as written in the source
Lemma integrable_image (f : T2 -> \bar R) :
  nu.-integrable [set: T2] f -> mu.-integrable [set: T1] (f \o g).
Used by 2 declarations in 2 files
lemma integral_image main result source, line 65 
forall [d1 d2 : measure_display] [T1 : measurableType d1] [T2 : measurableType d2]
  [R : realType] [mu : measure T1 R] [nu : measure T2 R] [g : T1 -> T2],
measurable_fun [set: T1] g ->
(forall A : set T2, d2.-measurable A -> mu (g @^-1` A) = nu A) ->
forall [f : T2 -> \bar R],
nu.-integrable [set: T2] f -> (\int[mu]_x f (g x))%E = (\int[nu]_y f y)%E
Main result, as the README states it

If nu is the image of the measure mu under a measurable g, then \int[mu] f (g x) = \int[nu] f y for every nu-integrable f.

Statement as written in the source
Lemma integral_image (f : T2 -> \bar R) :
  nu.-integrable [set: T2] f -> (\int[mu]_x f (g x) = \int[nu]_y f y)%E.
Used by 10 declarations in 6 files
sectionrV_cons
Context {R : realType} (n : nat).
definition rV_cons source, line 79
Type
forall {R : realType} [n : nat], measurableTypeR R * 'rV_n -> 'rV_n.+1
Definition
Definition rV_cons (p : measurableTypeR R * 'rV[R]_n) : 'rV[R]_n.+1 :=
  row_mx (const_mx (p.1 : R) : 'rV_1) p.2.
Used by 41 declarations in 7 files
lemma rV_cons0 source, line 82 
forall {R : realType} [n : nat] (p : measurableTypeR R * 'rV_n), rV_cons p 0 ord0 = p.1
Statement as written in the source
Lemma rV_cons0 p : rV_cons p 0 ord0 = p.1.
Used by 15 declarations in 6 files
lemma rV_consS source, line 88 
forall {R : realType} [n : nat] (p : measurableTypeR R * 'rV_n) (j : 'I_n),
rV_cons p 0 (lift ord0 j) = p.2 0 j
Statement as written in the source
Lemma rV_consS p (j : 'I_n) : rV_cons p 0 (lift ord0 j) = p.2 0 j.
Used by 13 declarations in 6 files
lemma measurable_rV_cons source, line 94 
forall {R : realType} [n : nat],
measurable_fun [set: measurableTypeR R * 'rV_n] (rV_cons (n:=n))
Statement as written in the source
Lemma measurable_rV_cons :
  measurable_fun [set: measurableTypeR R * 'rV[R]_n] rV_cons.
Used by 7 declarations in 5 files
instance instance at line 101 source, line 101 
HB.instance Definition _ :=
  isMeasurableFun.Build _ _ _ _ rV_cons measurable_rV_cons.
sectiongauss
Context {R : realType}.
Local Open Scope ereal_scope.
fixpoint gauss main result source, line 110
Type
forall {R : realType} (n : nat), probability 'rV_n R
Definition
Fixpoint gauss n : probability 'rV[R]_n R :=
  if n is n'.+1 then
    distribution (normal_prob 0 1 \x gauss n') (@rV_cons R n')
  else \d_(0%R : 'rV[R]_0).
Main result, as the README states it

gauss n, the standard Gaussian measure on 'rV[R]_n: the law of n independent standard normal coordinates, a probability.

Used in theories/ by: Gaussian/Law/LibraryBridge, Gaussian/Orthogonal/EqualCovariance, Gaussian/Lipschitz/Concentration, Gaussian/Lipschitz/Variance, Projected/BulkLaw
Used by 300 declarations in 42 files
sectiongauss_box
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
lemma gaussS source, line 121 
forall {R : realType} [n : nat] (X : set 'rV_n.+1),
gauss n.+1 X = (normal_prob 0 1 \x gauss n)%E (rV_cons (n:=n) @^-1` X)
Statement as written in the source
Lemma gaussS n X : gauss n.+1 X = (N \x gauss n)%E (@rV_cons R n @^-1` X).
Used by 2 declarations in 2 files
lemma gauss_box main result source, line 124 
forall {R : realType} [n : nat] [A : 'I_n -> set R],
(forall i : 'I_n, 'measurable (A i)) ->
gauss n [set x | (forall i : 'I_n, A i (x 0 i))] = (\prod_(i < n) normal_prob 0 1 (A i))%E
Main result, as the README states it

gauss n gives the box with sides A i the measure \prod_i normal_prob 0 1 (A i), and it is the only measure on 'rV[R]_n that does.

Used in theories/ by: Gaussian/Law/LibraryBridge
Statement as written in the source
Lemma gauss_box n (A : 'I_n -> set R) : (forall i, measurable (A i)) ->
  gauss n [set x : 'rV[R]_n | forall i, A i (x 0 i)] =
    (\prod_(i < n) N (A i))%E.
Used by 7 declarations in 3 files
lemma gauss_unique main result source, line 149 
forall {R : realType} [n : nat] [P : measure 'rV_n R],
(forall A : 'I_n -> set R,
 (forall i : 'I_n, 'measurable (A i)) ->
 P [set x | (forall i : 'I_n, A i (x 0 i))] = (\prod_(i < n) normal_prob 0 1 (A i))%E) ->
forall [X : set 'rV_n],
(measure_matrix_display default_measure_display).-measurable X -> P X = gauss n X

A measure that gives every box the product of the normal measures of its sides is gauss n. The hypothesis at A = fun=> setT makes it a probability.

Main result

Stated in the README together with gauss_box.

Statement as written in the source
Lemma gauss_unique n (P : {measure set 'rV[R]_n -> \bar R}) :
  (forall A : 'I_n -> set R, (forall i, measurable (A i)) ->
     P [set x : 'rV[R]_n | forall i, A i (x 0 i)] =
       (\prod_(i < n) N (A i))%E) ->
  forall X, measurable X -> P X = gauss n X.
Used by 4 declarations in 2 files
sectiongauss_integral
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Local Open Scope ereal_scope.
lemma ge0_integral_gauss_cons main result source, line 171 
forall {R : realType} [n : nat] [f : 'rV_n.+1 -> \bar R],
measurable_fun [set: 'rV_n.+1] f ->
(forall x : 'rV_n.+1, (0%R <= f x)%E) ->
(\int[gauss n.+1]_x f x)%E = (\int[normal_prob 0 1]_t \int[gauss n]_v f (rV_cons (t, v)))%E
Main result, as the README states it

Fubini for the first coordinate: the integral against gauss n.+1 is the iterated integral against normal_prob 0 1 and gauss n, and integrability against gauss n.+1 is integrability against the product of the two.

Used in theories/ by: Gaussian/Law/LibraryBridge, for Gaussian/Iterated/PolynomialGrowth
Statement as written in the source
Lemma ge0_integral_gauss_cons n (f : 'rV[R]_n.+1 -> \bar R) :
  measurable_fun [set: 'rV[R]_n.+1] f -> (forall x, 0 <= f x) ->
  \int[gauss n.+1]_x f x = \int[N]_t \int[gauss n]_v f (rV_cons (t, v)).
Used by 4 declarations in 4 files
lemma integrable_gauss_cons main result source, line 182 
forall {R : realType} [n : nat] [f : 'rV_n.+1 -> \bar R],
measurable_fun [set: 'rV_n.+1] f ->
(gauss n.+1).-integrable [set: 'rV_n.+1] f <->
(normal_prob 0 1 \x gauss n)%E.-integrable [set: measurableTypeR R * 'rV_n]
  (f \o rV_cons (n:=n))
Main result

Stated in the README together with ge0_integral_gauss_cons.

Statement as written in the source
Lemma integrable_gauss_cons n (f : 'rV[R]_n.+1 -> \bar R) :
  measurable_fun [set: 'rV[R]_n.+1] f ->
  (gauss n.+1).-integrable [set: 'rV[R]_n.+1] f <->
  (N \x gauss n).-integrable [set: measurableTypeR R * 'rV[R]_n]
    (f \o @rV_cons R n).
Used by 2 declarations in 2 files
lemma integral_gauss_cons main result source, line 201 
forall {R : realType} [n : nat] [f : 'rV_n.+1 -> \bar R],
(gauss n.+1).-integrable [set: 'rV_n.+1] f ->
(\int[gauss n.+1]_x f x)%E = (\int[normal_prob 0 1]_t \int[gauss n]_v f (rV_cons (t, v)))%E
Main result

Stated in the README together with ge0_integral_gauss_cons.

Statement as written in the source
Lemma integral_gauss_cons n (f : 'rV[R]_n.+1 -> \bar R) :
  (gauss n.+1).-integrable [set: 'rV[R]_n.+1] f ->
  \int[gauss n.+1]_x f x = \int[N]_t \int[gauss n]_v f (rV_cons (t, v)).
sectiongauss_invariance
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
lemma gauss_col_perm main result source, line 217 
forall {R : realType} [n : nat] (s : {perm 'I_n}) [X : set 'rV_n],
(measure_matrix_display default_measure_display).-measurable X ->
gauss n (col_perm s @^-1` X) = gauss n X
Main result, as the README states it

gauss n, and the integral of every integrable function against it, are invariant under permutations of the coordinates.

Used in theories/ by: Gaussian/Law/LibraryBridge, for Gaussian/Iterated/BlockRotation
Statement as written in the source
Lemma gauss_col_perm n (s : 'S_n) (X : set 'rV[R]_n) : measurable X ->
  gauss n (col_perm s @^-1` X) = gauss n X.
Used by 1 declaration in 1 file
lemma integral_gauss_col_perm main result source, line 235 
forall {R : realType} [n : nat] (s : {perm 'I_n}) [f : 'rV_n -> \bar R],
(gauss n).-integrable [set: 'rV_n] f ->
(\int[gauss n]_x f (col_perm s x))%E = (\int[gauss n]_x f x)%E
Main result

Stated in the README together with gauss_col_perm.

Statement as written in the source
Lemma integral_gauss_col_perm n (s : 'S_n) (f : 'rV[R]_n -> \bar R) :
  (gauss n).-integrable [set: 'rV[R]_n] f ->
  (\int[gauss n]_x f (col_perm s x) = \int[gauss n]_x f x)%E.
Used by 1 declaration in 1 file
lemma gauss_row_mx main result source, line 242 
forall {R : realType} [n m : nat] [X : set 'rV_(n + m)],
(measure_matrix_display default_measure_display).-measurable X ->
gauss (n + m) X =
(gauss n \x gauss m)%E ((fun p : 'rV_n * 'rV_m => row_mx p.1 p.2) @^-1` X)
Main result, as the README states it

Independent blocks: the image of gauss n \x gauss m under (x, y) |-> row_mx x y is gauss (n + m).

Statement as written in the source
Lemma gauss_row_mx n m (X : set 'rV[R]_(n + m)) : measurable X ->
  gauss (n + m) X =
  (gauss n \x gauss m)%E
    ((fun p : 'rV[R]_n * 'rV[R]_m => row_mx p.1 p.2) @^-1` X).
Used by 2 declarations in 1 file
lemma gauss_lsubmx main result source, line 279 
forall {R : realType} [n : nat] (m : nat) [X : set 'rV_n],
(measure_matrix_display default_measure_display).-measurable X ->
gauss (n + m) (lsubmx @^-1` X) = gauss n X
Main result, as the README states it

Marginals of the blocks: if x has law gauss (n + m), then lsubmx x has law gauss n and rsubmx x has law gauss m.

Statement as written in the source
Lemma gauss_lsubmx n m (X : set 'rV[R]_n) : measurable X ->
  gauss (n + m) (@lsubmx R 1 n m @^-1` X) = gauss n X.
Used by 1 declaration in 1 file
lemma gauss_rsubmx main result source, line 293 
forall {R : realType} (n : nat) [m : nat] [Y : set 'rV_m],
(measure_matrix_display default_measure_display).-measurable Y ->
gauss (n + m) (rsubmx @^-1` Y) = gauss m Y
Main result

Stated in the README together with gauss_lsubmx.

Statement as written in the source
Lemma gauss_rsubmx n m (Y : set 'rV[R]_m) : measurable Y ->
  gauss (n + m) (@rsubmx R 1 n m @^-1` Y) = gauss m Y.
Used by 1 declaration in 1 file
lemma integral_gauss_lsubmx main result source, line 307 
forall {R : realType} [n : nat] (m : nat) [f : 'rV_n -> \bar R],
(gauss n).-integrable [set: 'rV_n] f ->
(\int[gauss (n + m)]_x f (lsubmx x))%E = (\int[gauss n]_x f x)%E
Main result

Stated in the README together with gauss_lsubmx.

Statement as written in the source
Lemma integral_gauss_lsubmx n m (f : 'rV[R]_n -> \bar R) :
  (gauss n).-integrable [set: 'rV[R]_n] f ->
  (\int[gauss (n + m)]_x f (lsubmx x) = \int[gauss n]_x f x)%E.
Used by 5 declarations in 3 files
lemma integral_gauss_rsubmx main result source, line 314 
forall {R : realType} (n : nat) [m : nat] [f : 'rV_m -> \bar R],
(gauss m).-integrable [set: 'rV_m] f ->
(\int[gauss (n + m)]_x f (rsubmx x))%E = (\int[gauss m]_x f x)%E
Main result

Stated in the README together with gauss_lsubmx.

Statement as written in the source
Lemma integral_gauss_rsubmx n m (f : 'rV[R]_m -> \bar R) :
  (gauss m).-integrable [set: 'rV[R]_m] f ->
  (\int[gauss (n + m)]_x f (rsubmx x) = \int[gauss m]_x f x)%E.
Used by 5 declarations in 3 files
lemma gauss_coord main result source, line 321 
forall {R : realType} [n : nat] (i : 'I_n) [A : set R],
'measurable A -> gauss n [set x | A (x 0 i)] = normal_prob 0 1 A
Main result, as the README states it

Each coordinate of a vector of law gauss n has law normal_prob 0 1.

Statement as written in the source
Lemma gauss_coord n (i : 'I_n) (A : set R) : measurable A ->
  gauss n [set x : 'rV[R]_n | A (x 0 i)] = N A.
Used by 1 declaration in 1 file
lemma ge0_integral_gauss_prod main result source, line 335 
forall {R : realType} [n : nat] [f : 'I_n -> R -> R],
(forall i : 'I_n, measurable_fun [set: R] (f i)) ->
(forall (i : 'I_n) (t : R), 0 <= f i t) ->
(\int[gauss n]_x (\prod_(i < n) f i (x 0 i))%:E)%E =
(\prod_(i < n) \int[normal_prob 0 1]_t (f i t)%:E)%E
Main result, as the README states it

Independent coordinates: the integral of \prod_i f i (x 0 i) against gauss n is \prod_i of the integrals of f i against normal_prob 0 1, for nonnegative measurable f i.

Statement as written in the source
Lemma ge0_integral_gauss_prod n (f : 'I_n -> R -> R) :
  (forall i, measurable_fun [set: R] (f i)) -> (forall i t, 0 <= f i t) ->
  (\int[gauss n]_x (\prod_(i < n) f i (x 0 i))%:E =
   \prod_(i < n) \int[N]_t (f i t)%:E)%E.
Used by 3 declarations in 3 files
sectiongauss_coord_integral
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
let measurable_coord section-local source, line 378 
Let measurable_coord n (i : 'I_n) :
  measurable_fun [set: 'rV[R]_n]
    (fun x : 'rV[R]_n => (x 0 i : measurableTypeR R)).
Used by 1 declaration in 1 file
let coord section-local source, line 383 
Let coord n (i : 'I_n) : {mfun 'rV[R]_n >-> measurableTypeR R} :=
  HB.pack (fun x : 'rV[R]_n => (x 0 i : measurableTypeR R))
    (isMeasurableFun.Build _ _ _ _ _ (measurable_coord i)).
Used by 3 declarations in 1 file
Local Open Scope ereal_scope.
let distribution_coord section-local source, line 389 
Let distribution_coord n i A : measurable A ->
  distribution (gauss n) (coord i) A = N A.
Used by 2 declarations in 1 file
lemma ge0_integral_gauss_coord source, line 393 
forall {R : realType} [n : nat] (i : 'I_n) [f : R -> \bar R],
measurable_fun [set: R] f ->
(forall t : R, (0%R <= f t)%E) ->
(\int[gauss n]_x f (x 0%R i))%E = (\int[normal_prob 0 1]_t f t)%E
Statement as written in the source
Lemma ge0_integral_gauss_coord n (i : 'I_n) (f : R -> \bar R) :
  measurable_fun [set: R] f -> (forall t, 0 <= f t) ->
  \int[gauss n]_x f (x 0%R i) = \int[N]_t f t.
Used by 3 declarations in 3 files
lemma integrable_gauss_coord source, line 402 
forall {R : realType} [n : nat] (i : 'I_n) [f : R -> \bar R],
measurable_fun [set: R] f ->
(gauss n).-integrable [set: 'rV_n] (fun x : 'rV_n => f (x 0 i)) <->
(normal_prob 0 1).-integrable [set: R] f
Statement as written in the source
Lemma integrable_gauss_coord n (i : 'I_n) (f : R -> \bar R) :
  measurable_fun [set: R] f ->
  (gauss n).-integrable [set: 'rV[R]_n] (fun x => f (x 0%R i)) <->
  N.-integrable [set: R] f.
Used by 3 declarations in 2 files
lemma integral_gauss_coord main result source, line 416 
forall {R : realType} [n : nat] (i : 'I_n) [f : R -> \bar R],
(normal_prob 0 1).-integrable [set: R] f ->
(\int[gauss n]_x f (x 0%R i))%E = (\int[normal_prob 0 1]_t f t)%E
Main result

Stated in the README together with gauss_coord.

Statement as written in the source
Lemma integral_gauss_coord n (i : 'I_n) (f : R -> \bar R) :
  N.-integrable [set: R] f ->
  \int[gauss n]_x f (x 0%R i) = \int[N]_t f t.
Used by 1 declaration in 1 file
  • GaussianAnalysis.gaussian.gauss_moments: gauss_mean

Polynomial bounds C * (1 + `|x| ^+ k), with `|x| the largest absolute value of a coordinate.

sectionpoly_bound
Context {R : realType}.
lemma exprn1D_le source, line 433 
forall {R : realType} [a : R] (k : nat), 0 <= a -> (1 + a) ^+ k <= 2 ^+ k * (1 + a ^+ k)
Statement as written in the source
Lemma exprn1D_le (a : R) k :
  0 <= a -> (1 + a) ^+ k <= 2 ^+ k * (1 + a ^+ k).
lemma exprn1S_le source, line 446 
forall {R : realType} [a : R] (k : nat), 0 <= a -> 1 + a ^+ k <= 2 * (1 + a ^+ k.+1)
Statement as written in the source
Lemma exprn1S_le (a : R) k : 0 <= a -> 1 + a ^+ k <= 2 * (1 + a ^+ k.+1).
Used by 1 declaration in 1 file
lemma poly_bound_ge0 main result source, line 458 
forall {R : realType} [V : normedZmodType R] [G : V -> R] [C : R] [k : nat],
(forall x : V, `|G x| <= C * (1 + `|x| ^+ k)) -> 0 <= C

The constant of a polynomial bound is nonnegative.

Main result

Stated in the README together with integrable_gauss_poly.

Statement as written in the source
Lemma poly_bound_ge0 (V : normedZmodType R) (G : V -> R) (C : R) (k : nat) :
  (forall x, `|G x| <= C * (1 + `|x| ^+ k)) -> 0 <= C.
Used by 9 declarations in 4 files
lemma entry_mul_bound main result source, line 467 
forall {R : realType} [m : nat] (i : 'I_m) [G : 'rV_m -> R] [C : R] [k : nat],
(forall x : 'rV_m, `|G x| <= C * (1 + `|x| ^+ k)) ->
forall x : 'rV_m, `|x 0 i * G x| <= 2 * C * (1 + `|x| ^+ k.+1)

Multiplying by a coordinate raises the degree of a polynomial bound by one.

Main result

Stated in the README together with integrable_gauss_poly.

Statement as written in the source
Lemma entry_mul_bound m (i : 'I_m) (G : 'rV[R]_m -> R) (C : R) (k : nat) :
  (forall x, `|G x| <= C * (1 + `|x| ^+ k)) ->
  forall x : 'rV[R]_m, `|x 0 i * G x| <= (2 * C) * (1 + `|x| ^+ k.+1).
Used by 4 declarations in 2 files
sectiongauss_integrable_poly
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
lemma integrable_gauss_poly main result source, line 490 
forall {R : realType} [n : nat] [f : 'rV_n -> R] [C : R] [k : nat],
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, `|f x| <= C * (1 + `|x| ^+ k)) ->
(gauss n).-integrable [set: 'rV_n] (EFin \o f)
Main result, as the README states it

Every measurable function bounded by C (1 + |x|^k) is integrable against gauss n. The constant of such a bound is nonnegative, and multiplying the function by a coordinate raises k by one and doubles C.

Used in theories/ by: Gaussian/Law/LibraryBridge
Statement as written in the source
Lemma integrable_gauss_poly n (f : 'rV[R]_n -> R) (C : R) k :
  measurable_fun [set: 'rV[R]_n] f ->
  (forall x, `|f x| <= C * (1 + `|x| ^+ k)) ->
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o f).
Used by 30 declarations in 12 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.