GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisprobabilitylindeberg

The Lindeberg replacement method

GaussianAnalysis.probability.lindeberglibrary/probability/lindeberg.v303 lines17 lemmas and theorems, 3 definitionssource
Imports 0 library modules and 18 external

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 32
Required by 55 files of the paper proofs

Products of probability measures on tuples, that is the laws of tuples of independent random elements, and Lindeberg's replacement principle (lindeberg_replacement): if replacing the law of one coordinate changes the expectation of a bounded measurable function F by at most B_i, uniformly in the other coordinates, then replacing all the laws changes it by at most the sum of the B_i.

tuple_cons pthe tuple p.1 :: p.2 of size n.+1, for p : T * n.-tuple T
tuple_prod mu nthe 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
tuple_set x i tthe tuple x with its coordinate i replaced by t

Main results

ResultsStatementUsed by theories/
tuple_prodRintegral_tuple_prodS
tuple_prod mu n is the law of n independent random elements with laws mu 0, ..., mu (n-1), on n.-tuple T; integrals against it are iterated integrals (Fubini).none
lindeberg_replacement
Lindeberg's replacement principle: for F bounded and measurable on n.-tuple T, if replacing the law mu i of coordinate i by nu i changes the expectation of F by at most B i, uniformly in the other coordinates, then replacing all of them changes it by at most B 0 + ... + B (n-1).none: the proof keeps its own row replacement, Loss/Replacement, which works with the iterated expectation on lists; a bridge would need tuple_prod of the standard law to be identified with gaussian_product_law and a reshaping of rows

Declarations21 exported

lemma, theoremdefinitioninstancelocal
sectiontuple_prod
Context d (T : measurableType d) (R : realType).
definition tuple_cons source, line 40
Type
forall [d : measure_display] [T : measurableType d] [n : nat],
T * n.-tuple T -> (n.+1).-tuple T
Definition
Definition tuple_cons n (p : T * n.-tuple T) : n.+1.-tuple T :=
  [tuple of p.1 :: p.2].
Used by 22 declarations in 5 files
lemma measurable_tuple_cons source, line 43 
forall [d : measure_display] [T : measurableType d] [n : nat],
measurable_fun
  [set: (T * (n.-tuple _))]
  (tuple_cons (n:=n))
Statement as written in the source
Lemma measurable_tuple_cons n : measurable_fun setT (@tuple_cons n).
Used by 7 declarations in 3 files
instance instance at line 46 source, line 46 
HB.instance Definition _ n :=
  isMeasurableFun.Build _ _ _ _ (@tuple_cons n) (@measurable_tuple_cons n).
fixpoint tuple_prod main result source, line 49
Type
forall [d : measure_display] [T : measurableType d] [R : realType],
(nat -> probability T R) -> forall n : nat, probability (n.-tuple T) R
Definition
Fixpoint tuple_prod (mu : nat -> probability T R) n :
    probability (n.-tuple T) R :=
  match n with
  | 0 => dirac [tuple]
  | n'.+1 => distribution (mu 0%N \x tuple_prod (fun i => mu i.+1) n')%E
      (@tuple_cons n')
  end.
Main result, as the README states it

tuple_prod mu n is the law of n independent random elements with laws mu 0, ..., mu (n-1), on n.-tuple T; integrals against it are iterated integrals (Fubini).

Used in theories/ by: none
Used by 121 declarations in 25 files
sectiontuple_set
Context (T : Type).
definition tuple_set source, line 62
Type
forall [T : Type] [n : nat], n.-tuple T -> 'I_n -> T -> n.-tuple T
Definition
Definition tuple_set n (x : n.-tuple T) (i : 'I_n) (t : T) : n.-tuple T :=
  [tuple (if j == i then t else tnth x j) | j < n].
Used by 45 declarations in 8 files
lemma tuple_set_cons0 source, line 65 
forall [T : Type] [n : nat] (t s : T) (ts : n.-tuple T),
tuple_set [tuple of t :: ts] ord0 s = [tuple of s :: ts]
Statement as written in the source
Lemma tuple_set_cons0 n (t s : T) (ts : n.-tuple T) :
  tuple_set [tuple of t :: ts] ord0 s = [tuple of s :: ts].
Used by 3 declarations in 2 files
lemma tuple_set_consS source, line 73 
forall [T : Type] [n : nat] (t s : T) (ts : n.-tuple T) (i : 'I_n),
tuple_set [tuple of t :: ts] (lift ord0 i) s = [tuple of t :: tuple_set ts i s]
Statement as written in the source
Lemma tuple_set_consS n (t s : T) (ts : n.-tuple T) (i : 'I_n) :
  tuple_set [tuple of t :: ts] (lift ord0 i) s =
    [tuple of t :: tuple_set ts i s].
Used by 3 declarations in 2 files
sectionlindeberg
Context d (T : measurableType d) (R : realType).
Local Open Scope ereal_scope.
lemma bounded_integrable source, line 89 
forall [R : realType] [d' : measure_display] [U : measurableType d'] 
  (P : probability U R) [F : U -> R] [C : R],
measurable_fun [set: U] F ->
(forall x : U, `|F x| <= C) -> P.-integrable [set: U] (EFin \o F)
Statement as written in the source
Lemma bounded_integrable d' (U : measurableType d') (P : probability U R)
    (F : U -> R) (C : R) :
  measurable_fun setT F -> (forall x, `|F x| <= C)%R ->
  P.-integrable setT (EFin \o F).
Used by 30 declarations in 11 files
lemma measurable_tuple_set source, line 100 
forall [d : measure_display] [T : measurableType d] [n : nat] (x : n.-tuple T) (i : 'I_n),
measurable_fun [set: T] (tuple_set x i)
Statement as written in the source
Lemma measurable_tuple_set n (x : n.-tuple T) (i : 'I_n) :
  measurable_fun setT (tuple_set x i).
Used by 6 declarations in 4 files
lemma expectation_tuple_prod0 source, line 109 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [F : 0.-tuple T -> R],
measurable_fun [set: 0.-tuple _] F ->
('E_(tuple_prod mu 0)[F])%E = (F [tuple])%:E
Statement as written in the source
Lemma expectation_tuple_prod0 (mu : nat -> probability T R)
    (F : 0.-tuple T -> R) :
  measurable_fun setT F -> 'E_(tuple_prod mu 0)[F] = (F [tuple])%:E.
Used by 1 declaration in 1 file
lemma expectation_tuple_prodS source, line 117 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] [F : (n.+1).-tuple T -> R] 
  [C : R],
measurable_fun [set: n.+1.-tuple _] F ->
(forall x : (n.+1).-tuple T, `|F x| <= C) ->
('E_(tuple_prod mu n.+1)[F])%E =
(\int[mu 0%N]_t
    'E_(tuple_prod (fun i : nat => mu i.+1) n)[(fun ts : n.-tuple T =>
                                                F (tuple_cons (t, ts)))])%E
Statement as written in the source
Lemma expectation_tuple_prodS (mu : nat -> probability T R) n
    (F : n.+1.-tuple T -> R) (C : R) :
  measurable_fun setT F -> (forall x, `|F x| <= C)%R ->
  'E_(tuple_prod mu n.+1)[F] = \int[mu 0%N]_t
    'E_(tuple_prod (fun i => mu i.+1) n)[fun ts => F (tuple_cons (t, ts))].
Used by 1 declaration in 1 file
lemma expectation_tuple_prodS' source, line 131 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] [F : (n.+1).-tuple T -> R] 
  [C : R],
measurable_fun [set: n.+1.-tuple _] F ->
(forall x : (n.+1).-tuple T, `|F x| <= C) ->
('E_(tuple_prod mu n.+1)[F])%E =
(\int[tuple_prod (fun i : nat => mu i.+1) n]_ts
    'E_(mu 0%N)[(fun t : T => F (tuple_cons (t, ts)))])%E
Statement as written in the source
Lemma expectation_tuple_prodS' (mu : nat -> probability T R) n
    (F : n.+1.-tuple T -> R) (C : R) :
  measurable_fun setT F -> (forall x, `|F x| <= C)%R ->
  'E_(tuple_prod mu n.+1)[F] = \int[tuple_prod (fun i => mu i.+1) n]_ts
    'E_(mu 0%N)[fun t => F (tuple_cons (t, ts))].
Used by 1 declaration in 1 file
sectionbounded_Rintegral
Context d (U : measurableType d) (R : realType) (P : probability U R).
lemma EFin_Rintegral_bounded source, line 150 
forall [d : measure_display] [U : measurableType d] [R : realType] 
  (P : probability U R) [F : U -> R] [C : R],
measurable_fun [set: U] F ->
(forall x : U, `|F x| <= C) -> (\int[P]_x F x)%:E = (\int[P]_x (F x)%:E)%E
Statement as written in the source
Lemma EFin_Rintegral_bounded (F : U -> R) (C : R) :
  measurable_fun setT F -> (forall x, `|F x| <= C) ->
  (\int[P]_x F x)%:E = (\int[P]_x (F x)%:E)%E.
Used by 13 declarations in 5 files
lemma Rintegral_bounded source, line 158 
forall [d : measure_display] [U : measurableType d] [R : realType] 
  (P : probability U R) [F : U -> R] [C : R],
measurable_fun [set: U] F -> (forall x : U, `|F x| <= C) -> `|\int[P]_x F x| <= C
Statement as written in the source
Lemma Rintegral_bounded (F : U -> R) (C : R) :
  measurable_fun setT F -> (forall x, `|F x| <= C) -> `|\int[P]_x F x| <= C.
Used by 10 declarations in 6 files
lemma measurable_partial_Rintegral source, line 172 
forall [d1 d2 : measure_display] [U : measurableType d1] [V : measurableType d2]
  [R : realType],
probability U R ->
forall (Q : probability V R) [G : U * V -> R] [C : R],
measurable_fun [set: (U * V)] G ->
(forall z : U * V, `|G z| <= C) ->
measurable_fun [set: U] (fun u : U => \int[Q]_v G (u, v))
Statement as written in the source
Lemma measurable_partial_Rintegral d1 d2 (U : measurableType d1)
    (V : measurableType d2) (R : realType) (m : probability U R)
    (Q : probability V R) (G : U * V -> R) (C : R) :
  measurable_fun setT G -> (forall z, `|G z| <= C) ->
  measurable_fun setT (fun u => \int[Q]_v G (u, v)).
Used by 3 declarations in 2 files
sectionlindeberg_replacement
Context d (T : measurableType d) (R : realType).
lemma measurable_tuple_cons_l source, line 185 
forall [d : measure_display] [T : measurableType d] [n : nat] (t : T),
measurable_fun [set: n.-tuple _]
  (fun ts : n.-tuple T => tuple_cons (t, ts))
Statement as written in the source
Lemma measurable_tuple_cons_l n (t : T) :
  measurable_fun setT (fun ts : n.-tuple T => tuple_cons (t, ts)).
Used by 6 declarations in 3 files
lemma measurable_tuple_cons_r source, line 191 
forall [d : measure_display] [T : measurableType d] [n : nat] (ts : n.-tuple T),
measurable_fun [set: T] (fun t : T => tuple_cons (t, ts))
Statement as written in the source
Lemma measurable_tuple_cons_r n (ts : n.-tuple T) :
  measurable_fun setT (fun t : T => tuple_cons (t, ts)).
Used by 3 declarations in 2 files
lemma Rintegral_tuple_prodS main result source, line 197 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] [F : (n.+1).-tuple T -> R] 
  [C : R],
measurable_fun [set: n.+1.-tuple _] F ->
(forall x : (n.+1).-tuple T, `|F x| <= C) ->
\int[tuple_prod mu n.+1]_x F x =
\int[mu 0%N]_t \int[tuple_prod (fun i : nat => mu i.+1) n]_ts F (tuple_cons (t, ts))
Main result

Stated in the README together with tuple_prod.

Statement as written in the source
Lemma Rintegral_tuple_prodS (mu : nat -> probability T R) n
    (F : n.+1.-tuple T -> R) (C : R) :
  measurable_fun setT F -> (forall x, `|F x| <= C) ->
  \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 2 declarations in 2 files
lemma Rintegral_tuple_prodS' source, line 209 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] [F : (n.+1).-tuple T -> R] 
  [C : R],
measurable_fun [set: n.+1.-tuple _] F ->
(forall x : (n.+1).-tuple T, `|F x| <= C) ->
\int[tuple_prod mu n.+1]_x F x =
\int[tuple_prod (fun i : nat => mu i.+1) n]_ts \int[mu 0%N]_t F (tuple_cons (t, ts))
Statement as written in the source
Lemma Rintegral_tuple_prodS' (mu : nat -> probability T R) n
    (F : n.+1.-tuple T -> R) (C : R) :
  measurable_fun setT F -> (forall x, `|F x| <= C) ->
  \int[tuple_prod mu n.+1]_x F x = \int[tuple_prod (fun i => mu i.+1) n]_ts
    \int[mu 0%N]_t F (tuple_cons (t, ts)).
Used by 1 declaration in 1 file
lemma Rintegral_tuple_prod0 source, line 221 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [F : 0.-tuple T -> R],
measurable_fun [set: 0.-tuple _] F ->
\int[tuple_prod mu 0]_x F x = F [tuple]
Statement as written in the source
Lemma Rintegral_tuple_prod0 (mu : nat -> probability T R)
    (F : 0.-tuple T -> R) :
  measurable_fun setT F -> \int[tuple_prod mu 0]_x F x = F [tuple].
Used by 2 declarations in 2 files
lemma lindeberg_replacement main result source, line 230 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [n : nat] [mu nu : nat -> probability T R] [F : n.-tuple T -> R] 
  [C : R] [B : nat -> R],
measurable_fun [set: n.-tuple _] F ->
(forall x : n.-tuple T, `|F x| <= C) ->
(forall (i : 'I_n) (x : n.-tuple T),
 `|\int[mu i]_t F (tuple_set x i t) - \int[nu i]_t F (tuple_set x i t)| <= B i) ->
`|\int[tuple_prod mu n]_x F x - \int[tuple_prod nu n]_x F x| <= \sum_(i < n) B i

Lindeberg's replacement principle.

Main result, as the README states it

Lindeberg's replacement principle: for F bounded and measurable on n.-tuple T, if replacing the law mu i of coordinate i by nu i changes the expectation of F by at most B i, uniformly in the other coordinates, then replacing all of them changes it by at most B 0 + ... + B (n-1).

Used in theories/ by: none: the proof keeps its own row replacement, Loss/Replacement, which works with the iterated expectation on lists; a bridge would need tuple_prod of the standard law to be identified with gaussian_product_law and a reshaping of rows
Statement as written in the source
Lemma lindeberg_replacement n (mu nu : nat -> probability T R)
    (F : n.-tuple T -> R) (C : R) (B : nat -> R) :
  measurable_fun setT F -> (forall x, `|F x| <= C) ->
  (forall (i : 'I_n) (x : n.-tuple T),
    `|\int[mu i]_t F (tuple_set x i t) - \int[nu i]_t F (tuple_set x i t)|
      <= B i) ->
  `|\int[tuple_prod mu n]_x F x - \int[tuple_prod nu n]_x F x|
    <= \sum_(i < n) B i.
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.