On this page

Product laws by blocks

GaussianAnalysis.probability.tuple_rowslibrary/probability/tuple_rows.v498 lines21 lemmas and theorems, 3 definitionssource

Imports 1 library modules and 18 external

GaussianAnalysis.probability.lindeberg

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.numfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability

Imported by 10

Required by 15 files of the paper proofs

A tuple of n * d coordinates read as n rows of d coordinates, row i being made of the coordinates i * d + j for j < d, as the samples of the ellipsoid fitting papers are read.

`row_index i j`	the index i * d + j of 'I_(n * d), for i : 'I_n and j : 'I_d
`tuple_rows n d x`	the n rows of length d of the (n * d)-tuple x
`tuple_map g x`	[tuple g i (tnth x i) \| i < n], for x : n.-tuple T and g : nat -> T -> T'

Main results:

ge0_integral_tuple_prodS, integral_tuple_prodS: Fubini for the first coordinate, \int[tuple_prod mu n.+1] F = \int[mu 0]_t \int[tuple_prod (fun i => mu i.+1) n]_ts F (t :: ts), for F nonnegative and measurable, or integrable (integrable_tuple_prodS); the lemmas of lindeberg.v state it for bounded F;
ge0_integral_tuple_prod_prod: independent coordinates, the integral of \prod_i f_i (x_i) against tuple_prod mu n is the product of the integrals of the f_i against the mu i, for f_i nonnegative and measurable;
ge0_integral_image: the integral against a law mu that is the image of nu under a measurable g is the integral of f \o g against nu;
coordinatewise maps preserve independence: if mu i is the image of nu i under a measurable g i for every i, then tuple_prod mu n is the image of tuple_prod nu n under tuple_map g (tuple_prod_map), so that the integral of a measurable G against tuple_prod mu n is the integral of x |-> G (tuple_map g x) against tuple_prod nu n (ge0_integral_tuple_map, integral_tuple_map, Rintegral_tuple_map), and integrable_tuple_map;
blocks: Fubini for the first a and the last b coordinates, \int[tuple_prod mu (a + b)] F = \int[tuple_prod mu a]_x \int[tuple_prod (fun i => mu (a + i)) b]_y F [tuple of x ++ y] (ge0_integral_tuple_prod_cat), so disjoint blocks are independent with the product laws of their coordinates;
rows: the image of tuple_prod mu (n * m) under tuple_rows n m is the product over i < n of the laws tuple_prod (fun j => mu (i * m + j)) m of the rows (tuple_prod_rows, ge0_integral_tuple_rows, integral_tuple_rows);
eq_tuple_prod: tuple_prod mu n depends only on mu 0, ..., mu (n - 1).

Main results

Results	Statement
ge0_integral_tuple_prodSintegral_tuple_prodSge0_integral_tuple_prod_prodge0_integral_tuple_prod_cat	Fubini for `tuple_prod mu n`: for the first coordinate (nonnegative or integrable functions), for a first and a last block of coordinates, which are therefore independent with the product laws of their coordinates; the integral of `prod_i f_i (x_i)` is the product of the integrals.
tuple_rowstuple_prod_rowsintegral_tuple_rowstuple_maptuple_prod_mapintegral_tuple_mapge0_integral_imageeq_tuple_prod	A tuple of `n * m` coordinates read as `n` rows of `m`: under `tuple_prod mu (n * m)` the rows are independent, row `i` with law `tuple_prod (fun j => mu (i * m + j)) m`. Coordinatewise maps preserve independence: if `mu i` is the image of `nu i` under `g i`, `tuple_prod mu n` is the image of `tuple_prod nu n` under `tuple_map g`.

Declarations24 exported

sectiontuple_rows

Context (T : Type) (n d : nat).

lemma row_index_subproof source, line 66

forall [n d : nat] (i : 'I_n) (j : 'I_d), (i * d + j < n * d)%N

Statement as written in the source

Lemma row_index_subproof (i : 'I_n) (j : 'I_d) : (i * d + j < n * d)%N.

Used by 1 declaration in 1 file

this file: row_index

definition row_index source, line 72

Type

forall [n d : nat], 'I_n -> 'I_d -> 'I_(n * d)

Definition

Definition row_index (i : 'I_n) (j : 'I_d) : 'I_(n * d) :=
  Ordinal (row_index_subproof i j).

Used by 3 declarations in 1 file

this file: tuple_rows, measurable_tuple_rows, tuple_rows_cat

definition tuple_rows main result source, line 75

Type

forall {T : Type} (n d : nat), (n * d).-tuple T -> n.-tuple (d.-tuple T)

Definition

Definition tuple_rows (x : (n * d).-tuple T) : n.-tuple (d.-tuple T) :=
  [tuple [tuple tnth x (row_index i j) | j < d] | i < n].

Main result, as the README states it

A tuple of n * m coordinates read as n rows of m: under tuple_prod mu (n * m) the rows are independent, row i with law tuple_prod (fun j => mu (i * m + j)) m. Coordinatewise maps preserve independence: if mu i is the image of nu i under g i, tuple_prod mu n is the image of tuple_prod nu n under tuple_map g.

Used by 5 declarations in 1 file

this file: measurable_tuple_rows, tuple_rows_cat, ge0_integral_tuple_rows, integral_tuple_rows, tuple_prod_rows

Arguments tuple_rows {T} n d x.

sectiontuple_prod_integral

Context d (T : measurableType d) (R : realType).
Local Open Scope ereal_scope.

lemma ge0_integral_tuple_prodS main result source, line 86

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] [F : (n.+1).-tuple T -> \bar R],
measurable_fun [set: (n.+1).-tuple T] F ->
(forall x : (n.+1).-tuple T, (0%R <= F x)%E) ->
(\int[tuple_prod mu n.+1]_x F x)%E =
(\int[mu 0%N]_t \int[tuple_prod (fun i : nat => mu i.+1) n]_ts F (tuple_cons (t, ts)))%E

Fubini for the first coordinate, for nonnegative functions.

Main result, as the README states it

Fubini for tuple_prod mu n: for the first coordinate (nonnegative or integrable functions), for a first and a last block of coordinates, which are therefore independent with the product laws of their coordinates; the integral of prod_i f_i (x_i) is the product of the integrals.

Statement as written in the source

Lemma ge0_integral_tuple_prodS (mu : nat -> probability T R) n
    (F : n.+1.-tuple T -> \bar R) :
  measurable_fun [set: n.+1.-tuple T] F -> (forall x, 0 <= F x) ->
  \int[tuple_prod mu n.+1]_x F x =
  \int[mu 0%N]_t
    \int[tuple_prod (fun i => mu i.+1) n]_ts F (tuple_cons (t, ts)).

Used by 6 declarations in 2 files

GaussianAnalysis.probability.efron_stein: ge0_integral_tuple_prod_set, efron_stein_integrable
this file: ge0_integral_tuple_prod_prod, ge0_integral_tuple_map, ge0_integral_tuple_prod_cat, ge0_integral_tuple_rows

lemma integrable_tuple_prodS source, line 100

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] [F : (n.+1).-tuple T -> \bar R],
measurable_fun [set: (n.+1).-tuple T] F ->
(tuple_prod mu n.+1).-integrable [set: (n.+1).-tuple T] F <->
(mu 0%N \x tuple_prod (fun i : nat => mu i.+1) n)%E.-integrable [set: 
  T * n.-tuple T] (F \o tuple_cons (n:=n))

Statement as written in the source

Lemma integrable_tuple_prodS (mu : nat -> probability T R) n
    (F : n.+1.-tuple T -> \bar R) :
  measurable_fun [set: n.+1.-tuple T] F ->
  (tuple_prod mu n.+1).-integrable [set: n.+1.-tuple T] F <->
  (mu 0%N \x tuple_prod (fun i => mu i.+1) n).-integrable
    [set: T * n.-tuple T] (F \o @tuple_cons _ T n).

Used by 2 declarations in 2 files

GaussianAnalysis.probability.efron_stein: efron_stein_integrable
this file: integral_tuple_prodS

lemma integral_tuple_prodS main result source, line 121

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [F : (n.+1).-tuple T -> \bar R],
(tuple_prod mu n.+1).-integrable [set: (n.+1).-tuple T] F ->
(\int[tuple_prod mu n.+1]_x F x)%E =
(\int[mu 0%N]_t \int[tuple_prod (fun i : nat => mu i.+1) n]_ts F (tuple_cons (t, ts)))%E

Fubini for the first coordinate, for integrable functions.

Main result

Stated in the README together with ge0_integral_tuple_prodS.

Statement as written in the source

Lemma integral_tuple_prodS (mu : nat -> probability T R) n
    (F : n.+1.-tuple T -> \bar R) :
  (tuple_prod mu n.+1).-integrable [set: n.+1.-tuple T] F ->
  \int[tuple_prod mu n.+1]_x F x =
  \int[mu 0%N]_t
    \int[tuple_prod (fun i => mu i.+1) n]_ts F (tuple_cons (t, ts)).

lemma ge0_integral_tuple_prod_prod main result source, line 137

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) (n : nat) [f : nat -> T -> R],
(forall i : nat, measurable_fun [set: T] (f i)) ->
(forall (i : nat) (t : T), 0 <= f i t) ->
(\int[tuple_prod mu n]_x (\prod_(i < n) f i (tnth x i))%:E)%E =
(\prod_(i < n) \int[mu i]_t (f i t)%:E)%E

Independent coordinates: the integral of a product of nonnegative functions of the coordinates is the product of the integrals.

Main result

Stated in the README together with ge0_integral_tuple_prodS.

Statement as written in the source

Lemma ge0_integral_tuple_prod_prod (mu : nat -> probability T R) n
    (f : nat -> T -> R) :
  (forall i, measurable_fun [set: T] (f i)) -> (forall i t, (0 <= f i t)%R) ->
  \int[tuple_prod mu n]_x (\prod_(i < n) f i (tnth x i))%:E =
  \prod_(i < n) \int[mu i]_t (f i t)%:E.

Used by 4 declarations in 2 files

GaussianAnalysis.probability.subgaussian: subgaussian_sum_mgf, subexponential_sum_mgf
GaussianAnalysis.probability.density_law: prob_density_tuple_prod, tuple_prod_density

sectionimage_law

Context d1 d2 (V : measurableType d1) (W : measurableType d2) (R : realType).
Local Open Scope ereal_scope.

lemma ge0_integral_image main result source, line 183

forall [d1 d2 : measure_display] [V : measurableType d1] [W : measurableType d2]
  [R : realType] [nu : probability V R] [mu : probability W R] 
  [g : V -> W] [f : W -> \bar R],
measurable_fun [set: V] g ->
(forall A : set W, d2.-measurable A -> mu A = nu (g @^-1` A)) ->
measurable_fun [set: W] f ->
(forall y : W, (0%R <= f y)%E) -> (\int[mu]_y f y)%E = (\int[nu]_x f (g x))%E

The integral against a law mu that is the image of nu under g.

Main result

Stated in the README together with tuple_rows.

Statement as written in the source

Lemma ge0_integral_image (nu : probability V R) (mu : probability W R)
    (g : V -> W) (f : W -> \bar R) :
  measurable_fun setT g -> (forall A, measurable A -> mu A = nu (g @^-1` A)) ->
  measurable_fun setT f -> (forall y, 0 <= f y) ->
  \int[mu]_y f y = \int[nu]_x f (g x).

Used by 3 declarations in 3 files

this file: ge0_integral_tuple_map
GaussianAnalysis.probability.conditioning: ge0_integral_tuple_prod_merge
GaussianAnalysis.convex.gauss_feature: gauss_regular_feature

sectiontuple_map

Context d d' (T : measurableType d) (T' : measurableType d') (R : realType).
Local Open Scope ereal_scope.

definition tuple_map main result source, line 203

Type

forall [d d' : measure_display] [T : measurableType d] [T' : measurableType d'],
(nat -> T -> T') -> forall {n : nat}, n.-tuple T -> n.-tuple T'

Definition

Definition tuple_map (g : nat -> T -> T') {n} (x : n.-tuple T) : n.-tuple T' :=
  [tuple g i (tnth x i) | i < n].

The coordinatewise map x |-> [tuple g i (x_i) | i < n].

Main result

Stated in the README together with tuple_rows.

Used by 8 declarations in 2 files

this file: measurable_tuple_map, tuple_map_cons, ge0_integral_tuple_map, tuple_prod_map, integral_tuple_map, integrable_tuple_map, Rintegral_tuple_map
GaussianAnalysis.convex.barrier_lindeberg: integral_tuple_prod_free

lemma measurable_tuple_map source, line 206

forall [d d' : measure_display] [T : measurableType d] [T' : measurableType d']
  [g : nat -> T -> T'] [n : nat],
(forall i : nat, measurable_fun [set: T] (g i)) ->
measurable_fun [set: n.-tuple _]
  (tuple_map g)

Statement as written in the source

Lemma measurable_tuple_map (g : nat -> T -> T') n :
  (forall i, measurable_fun setT (g i)) -> measurable_fun setT (@tuple_map g n).

Used by 3 declarations in 1 file

this file: ge0_integral_tuple_map, tuple_prod_map, integrable_tuple_map

lemma tuple_map_cons source, line 215

forall [d d' : measure_display] [T : measurableType d] [T' : measurableType d']
  (g : nat -> T -> T') [n : nat] (t : T) (ts : n.-tuple T),
tuple_map g (tuple_cons (t, ts)) =
tuple_cons (g 0%N t, tuple_map (fun i : nat => g i.+1) ts)

Statement as written in the source

Lemma tuple_map_cons (g : nat -> T -> T') n (t : T) (ts : n.-tuple T) :
  tuple_map g (tuple_cons (t, ts)) =
  tuple_cons (g 0%N t, tuple_map (fun i => g i.+1) ts).

Used by 1 declaration in 1 file

this file: ge0_integral_tuple_map

lemma ge0_integral_tuple_map source, line 227

forall [d d' : measure_display] [T : measurableType d] [T' : measurableType d']
  [R : realType] [nu : nat -> probability T R] [mu : nat -> probability T' R]
  [g : nat -> T -> T'] [n : nat] [G : n.-tuple T' -> \bar R],
(forall i : nat, measurable_fun [set: T] (g i)) ->
(forall (i : nat) (A : set T'), d'.-measurable A -> mu i A = nu i (g i @^-1` A)) ->
measurable_fun [set: n.-tuple _] G ->
(forall y : n.-tuple T', (0%R <= G y)%E) ->
(\int[tuple_prod mu n]_y G y)%E = (\int[tuple_prod nu n]_x G (tuple_map g x))%E

Coordinatewise maps preserve independence: if mu i is the image of nu i under g i for every i, then tuple_prod mu n is the image of tuple_prod nu n under tuple_map g.

Statement as written in the source

Lemma ge0_integral_tuple_map (nu : nat -> probability T R)
    (mu : nat -> probability T' R) (g : nat -> T -> T') n
    (G : n.-tuple T' -> \bar R) :
  (forall i, measurable_fun setT (g i)) ->
  (forall i A, measurable A -> mu i A = nu i (g i @^-1` A)) ->
  measurable_fun setT G -> (forall y, 0 <= G y) ->
  \int[tuple_prod mu n]_y G y = \int[tuple_prod nu n]_x G (tuple_map g x).

Used by 3 declarations in 1 file

this file: tuple_prod_map, integral_tuple_map, integrable_tuple_map

lemma tuple_prod_map main result source, line 280

forall [d d' : measure_display] [T : measurableType d] [T' : measurableType d']
  [R : realType] [nu : nat -> probability T R] [mu : nat -> probability T' R]
  [g : nat -> T -> T'] [n : nat] [A : set (n.-tuple T')],
(forall i : nat, measurable_fun [set: T] (g i)) ->
(forall (i : nat) (B : set T'), d'.-measurable B -> mu i B = nu i (g i @^-1` B)) ->
(measure_tuple_display d').-measurable A ->
tuple_prod mu n A = tuple_prod nu n (tuple_map g @^-1` A)

Main result

Stated in the README together with tuple_rows.

Statement as written in the source

Lemma tuple_prod_map (nu : nat -> probability T R)
    (mu : nat -> probability T' R) (g : nat -> T -> T') n
    (A : set (n.-tuple T')) :
  (forall i, measurable_fun setT (g i)) ->
  (forall i B, measurable B -> mu i B = nu i (g i @^-1` B)) ->
  measurable A -> tuple_prod mu n A = tuple_prod nu n (tuple_map g @^-1` A).

lemma integral_tuple_map main result source, line 302

forall [d d' : measure_display] [T : measurableType d] [T' : measurableType d']
  [R : realType] [nu : nat -> probability T R] [mu : nat -> probability T' R]
  [g : nat -> T -> T'] [n : nat] [G : n.-tuple T' -> \bar R],
(forall i : nat, measurable_fun [set: T] (g i)) ->
(forall (i : nat) (A : set T'), d'.-measurable A -> mu i A = nu i (g i @^-1` A)) ->
measurable_fun [set: n.-tuple _] G ->
(\int[tuple_prod mu n]_y G y)%E = (\int[tuple_prod nu n]_x G (tuple_map g x))%E

The same for every measurable G with values in \bar R, integrable or not.

Main result

Stated in the README together with tuple_rows.

Statement as written in the source

Lemma integral_tuple_map (nu : nat -> probability T R)
    (mu : nat -> probability T' R) (g : nat -> T -> T') n
    (G : n.-tuple T' -> \bar R) :
  (forall i, measurable_fun setT (g i)) ->
  (forall i A, measurable A -> mu i A = nu i (g i @^-1` A)) ->
  measurable_fun setT G ->
  \int[tuple_prod mu n]_y G y = \int[tuple_prod nu n]_x G (tuple_map g x).

Used by 2 declarations in 2 files

this file: Rintegral_tuple_map
GaussianAnalysis.convex.barrier_lindeberg: integral_tuple_prod_free

lemma integrable_tuple_map source, line 316

forall [d d' : measure_display] [T : measurableType d] [T' : measurableType d']
  [R : realType] [nu : nat -> probability T R] [mu : nat -> probability T' R]
  [g : nat -> T -> T'] [n : nat] [G : n.-tuple T' -> \bar R],
(forall i : nat, measurable_fun [set: T] (g i)) ->
(forall (i : nat) (A : set T'), d'.-measurable A -> mu i A = nu i (g i @^-1` A)) ->
measurable_fun [set: n.-tuple _] G ->
(tuple_prod mu n).-integrable [set: n.-tuple T'] G <->
(tuple_prod nu n).-integrable [set: n.-tuple T] (fun x : n.-tuple T => G (tuple_map g x))

Statement as written in the source

Lemma integrable_tuple_map (nu : nat -> probability T R)
    (mu : nat -> probability T' R) (g : nat -> T -> T') n
    (G : n.-tuple T' -> \bar R) :
  (forall i, measurable_fun setT (g i)) ->
  (forall i A, measurable A -> mu i A = nu i (g i @^-1` A)) ->
  measurable_fun setT G ->
  (tuple_prod mu n).-integrable setT G <->
  (tuple_prod nu n).-integrable setT (fun x => G (tuple_map g x)).

lemma Rintegral_tuple_map source, line 335

forall [d d' : measure_display] [T : measurableType d] [T' : measurableType d']
  [R : realType] [nu : nat -> probability T R] [mu : nat -> probability T' R]
  [g : nat -> T -> T'] [n : nat] [G : n.-tuple T' -> R],
(forall i : nat, measurable_fun [set: T] (g i)) ->
(forall (i : nat) (A : set T'), d'.-measurable A -> mu i A = nu i (g i @^-1` A)) ->
measurable_fun [set: n.-tuple _] G ->
\int[tuple_prod mu n]_y G y = \int[tuple_prod nu n]_x G (tuple_map g x)

Statement as written in the source

Lemma Rintegral_tuple_map (nu : nat -> probability T R)
    (mu : nat -> probability T' R) (g : nat -> T -> T') n
    (G : n.-tuple T' -> R) :
  (forall i, measurable_fun setT (g i)) ->
  (forall i A, measurable A -> mu i A = nu i (g i @^-1` A)) ->
  measurable_fun setT G ->
  (\int[tuple_prod mu n]_y G y = \int[tuple_prod nu n]_x G (tuple_map g x))%R.

sectiontuple_cat

Context d (T : measurableType d) (R : realType).
Local Open Scope ereal_scope.

lemma measurable_tuple_cat source, line 353

forall [d : measure_display] [T : measurableType d] [a b : nat],
measurable_fun
  [set: ((a.-tuple _) * (b.-tuple _))]
  (fun p : a.-tuple T * b.-tuple T => [tuple of p.1 ++ p.2])

Statement as written in the source

Lemma measurable_tuple_cat a b :
  measurable_fun setT
    (fun p : a.-tuple T * b.-tuple T => [tuple of p.1 ++ p.2]).

Used by 1 declaration in 1 file

this file: ge0_integral_tuple_prod_cat

lemma ge0_integral_tuple_prod_cat main result source, line 371

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [a b : nat] [F : (a + b).-tuple T -> \bar R],
measurable_fun [set: (a + b).-tuple _] F ->
(forall z : (a + b).-tuple T, (0%R <= F z)%E) ->
(\int[tuple_prod mu (a + b)]_z F z)%E =
(\int[tuple_prod mu a]_x
    \int[tuple_prod (fun i : nat => mu (a + i)%N) b]_y F [tuple of x ++ y])%E

Fubini for blocks: the first a coordinates and the last b coordinates of tuple_prod mu (a + b) are independent, with the product laws of their coordinates.

Main result

Stated in the README together with ge0_integral_tuple_prodS.

Statement as written in the source

Lemma ge0_integral_tuple_prod_cat (mu : nat -> probability T R) a b
    (F : (a + b).-tuple T -> \bar R) :
  measurable_fun setT F -> (forall z, 0 <= F z) ->
  \int[tuple_prod mu (a + b)]_z F z =
  \int[tuple_prod mu a]_x
    \int[tuple_prod (fun i => mu (a + i)%N) b]_y F [tuple of x ++ y].

Used by 3 declarations in 2 files

this file: ge0_integral_tuple_rows
GaussianAnalysis.probability.symmetrization: ge0_integral_tuple_left, ge0_integral_tuple_right

lemma measurable_tuple_rows source, line 405

forall [d : measure_display] [T : measurableType d] [n m : nat],
measurable_fun [set: (n * m).-tuple T] (tuple_rows n m)

Statement as written in the source

Lemma measurable_tuple_rows n m :
  measurable_fun [set: (n * m).-tuple T] (tuple_rows n m).

Used by 2 declarations in 1 file

this file: ge0_integral_tuple_rows, tuple_prod_rows

lemma tuple_rows_cat source, line 414

forall [d : measure_display] [T : measurableType d] [n m : nat] 
  (x : m.-tuple T) (y : (n * m).-tuple T),
tuple_rows n.+1 m [tuple of x ++ y] = tuple_cons (x, tuple_rows n m y)

Statement as written in the source

Lemma tuple_rows_cat n m (x : m.-tuple T) (y : (n * m).-tuple T) :
  tuple_rows n.+1 m [tuple of x ++ y] = tuple_cons (x, tuple_rows n m y).

Used by 1 declaration in 1 file

this file: ge0_integral_tuple_rows

lemma ge0_integral_tuple_rows source, line 430

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n m : nat] [G : n.-tuple (m.-tuple T) -> \bar R],
measurable_fun [set: n.-tuple _] G ->
(forall y : n.-tuple (m.-tuple T), (0%R <= G y)%E) ->
(\int[tuple_prod mu (n * m)]_x G (tuple_rows n m x))%E =
(\int[tuple_prod (fun i : nat => tuple_prod (fun j : nat => mu (i * m + j)%N) m) n]_y G y)%E

The rows of tuple_prod mu (n * m) are independent: tuple_rows n m maps it to the product over i < n of the laws of the rows.

Statement as written in the source

Lemma ge0_integral_tuple_rows (mu : nat -> probability T R) n m
    (G : n.-tuple (m.-tuple T) -> \bar R) :
  measurable_fun setT G -> (forall y, 0 <= G y) ->
  \int[tuple_prod mu (n * m)]_x G (tuple_rows n m x) =
  \int[tuple_prod (fun i => tuple_prod (fun j => mu (i * m + j)%N) m) n]_y G y.

Used by 2 declarations in 1 file

this file: integral_tuple_rows, tuple_prod_rows

lemma integral_tuple_rows main result source, line 458

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n m : nat] [G : n.-tuple (m.-tuple T) -> \bar R],
measurable_fun [set: n.-tuple _] G ->
(\int[tuple_prod mu (n * m)]_x G (tuple_rows n m x))%E =
(\int[tuple_prod (fun i : nat => tuple_prod (fun j : nat => mu (i * m + j)%N) m) n]_y G y)%E

Main result

Stated in the README together with tuple_rows.

Statement as written in the source

Lemma integral_tuple_rows (mu : nat -> probability T R) n m
    (G : n.-tuple (m.-tuple T) -> \bar R) :
  measurable_fun setT G ->
  \int[tuple_prod mu (n * m)]_x G (tuple_rows n m x) =
  \int[tuple_prod (fun i => tuple_prod (fun j => mu (i * m + j)%N) m) n]_y G y.

lemma tuple_prod_rows main result source, line 470

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n m : nat] [A : set (n.-tuple (m.-tuple T))],
(measure_tuple_display (measure_tuple_display d)).-measurable A ->
tuple_prod (fun i : nat => tuple_prod (fun j : nat => mu (i * m + j)%N) m) n A =
tuple_prod mu (n * m) (tuple_rows n m @^-1` A)

Main result

Stated in the README together with tuple_rows.

Statement as written in the source

Lemma tuple_prod_rows (mu : nat -> probability T R) n m
    (A : set (n.-tuple (m.-tuple T))) : measurable A ->
  tuple_prod (fun i => tuple_prod (fun j => mu (i * m + j)%N) m) n A =
  tuple_prod mu (n * m) (tuple_rows n m @^-1` A).

lemma eq_tuple_prod main result source, line 490

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu mu' : nat -> probability T R] [n : nat],
(forall i : nat, (i < n)%N -> mu i = mu' i) -> tuple_prod mu n = tuple_prod mu' n

tuple_prod mu n depends only on mu 0, ..., mu (n - 1).

Main result

Stated in the README together with tuple_rows.

Statement as written in the source

Lemma eq_tuple_prod (mu mu' : nat -> probability T R) n :
  (forall i, (i < n)%N -> mu i = mu' i) -> tuple_prod mu n = tuple_prod mu' n.

Used by 3 declarations in 2 files

GaussianAnalysis.probability.symmetrization: doubled_law_left, doubled_law_right
GaussianAnalysis.convex.barrier_lindeberg: lindeberg_telescope

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.