GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisprobabilityconditioning

Conditioning a product law on a set of coordinates

GaussianAnalysis.probability.conditioninglibrary/probability/conditioning.v521 lines20 lemmas and theorems, 4 definitionssource
Imports 2 library modules and 23 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.classical.cardinality, 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 7
Required by 6 files of the paper proofs

Under the product law tuple_prod mu n of n independent coordinates, the coordinates outside a set S may be resampled independently of those in S (ge0_integral_tuple_prod_merge). This gives, without conditional expectations, the tools of a proof that reveals the coordinates in stages, as the proof of Proposition 3.4 of Koehler and Sohn (arXiv 2608.27372, lines 3610-3805) does. An event E depends only on the coordinates in S when replacing the others does not change it: E (tuple_merge S x y) = E x for all x and y.

  • tuple_prod_box, measure_tuple_box_unique: the measure of a box is the product of the measures of its sides, and two finite measures on the n-tuples that agree on the boxes agree.
  • tuple_prod_merge: resampling the coordinates outside S does not change tuple_prod mu n.
  • tuple_prod_cond_le: if H depends only on the coordinates in S and, for every x in H, resampling the coordinates of x outside S puts it in E with probability at most c x, then P(E and H) <= int_H c.
  • tuple_prod_indepS, tuple_prod_indep_big: events that depend on pairwise disjoint sets of coordinates are independent.
  • tuple_prod_chain_le: if the coordinates are revealed in nested sets S 0, S 1, ..., the event A l depends only on the coordinates in S l.+1 and, given the coordinates in S l of a tuple of the earlier events, has probability at most c l, then the A l, l < L, occur together with probability at most the product of the c l.
  • tuple_prod_pick: for an injective f, the coordinates f 0, ..., f (k - 1) of tuple_prod mu n have the product law of their laws.
tuple_box Athe n-tuples x with x_i in A i for every i
tuple_merge S x ythe n-tuple with the coordinates of x in S and those of y outside S
tuple_pick f xthe k-tuple (x_(f 0), ..., x_(f (k - 1)))

Main results

ResultsStatement
tuple_mergetuple_prod_mergege0_integral_tuple_prod_mergetuple_prod_cond_le
Conditioning tuple_prod mu n on the coordinates in a set S by resampling the others: tuple_merge S x y takes the coordinates in S from x and the others from y, and its law under two independent copies of tuple_prod mu n is tuple_prod mu n. If H depends only on the coordinates in S (H (tuple_merge S x y) = H x) and, for every x in H, tuple_merge S x y is in E with probability at most c x, then P(E and H) <= int_H c.
tuple_prod_indepStuple_prod_indep_bigtuple_prod_chain_le
Events that depend on pairwise disjoint sets of coordinates are independent. Revealing the coordinates in nested sets S 0, S 1, ...: if A l depends only on the coordinates in S (l + 1) and, given those in S l of a tuple of A 0, ..., A (l - 1), has probability at most c l, then P(A 0, ..., A (L - 1)) <= c 0 ... c (L - 1).
tuple_prod_picktuple_prod_boxmeasure_tuple_box_unique
For an injective f : 'I_k -> 'I_n, the coordinates f 0, ..., f (k - 1) of tuple_prod mu n have the law tuple_prod nu k with nu i = mu (f i). The measure of a box is the product of the measures of its sides, and two finite measures on n.-tuple T that agree on the boxes agree.

Declarations24 exported

lemma, theoremdefinitioninstancelocal
sectiontuple_box
Context d (T : measurableType d) (n : nat).
definition tuple_box source, line 61
Type
forall [d : measure_display] [T : measurableType d] [n : nat],
('I_n -> set T) -> set (n.-tuple T)
Definition
Definition tuple_box (A : 'I_n -> set T) : set (n.-tuple T) :=
  [set x | forall i, A i (tnth x i)].

The product of the sets A i.

Used by 12 declarations in 5 files
definition tuple_boxes source, line 64
Type
forall [d : measure_display] [T : measurableType d] [n : nat], set (set (n.-tuple T))
Definition
Definition tuple_boxes : set (set (n.-tuple T)) :=
  [set tuple_box A | A in [set A | forall i, measurable (A i)]].
Used by 3 declarations in 1 file
lemma tuple_boxE source, line 67 
forall [d : measure_display] [T : measurableType d] [n : nat] (A : 'I_n -> set T),
tuple_box A = \bigcap_i (tnth (T:=T))^~ i @^-1` A i
Statement as written in the source
Lemma tuple_boxE (A : 'I_n -> set T) :
  tuple_box A = \bigcap_(i in [set: 'I_n]) ((@tnth n T)^~ i @^-1` A i).
Used by 1 declaration in 1 file
lemma measurable_tuple_box source, line 71 
forall [d : measure_display] [T : measurableType d] [n : nat] [A : 'I_n -> set T],
(forall i : 'I_n, d.-measurable (A i)) ->
(measure_tuple_display d).-measurable (tuple_box A)
Statement as written in the source
Lemma measurable_tuple_box (A : 'I_n -> set T) :
  (forall i, measurable (A i)) -> measurable (tuple_box A).
Used by 3 declarations in 1 file
lemma measurable_tuple_boxes source, line 80 
forall [d : measure_display] (T : measurableType d) (n : nat),
(measure_tuple_display d).-measurable = <<s tuple_boxes (n:=n) >>
Statement as written in the source
Lemma measurable_tuple_boxes : @measurable _ (n.-tuple T) = <<s tuple_boxes >>.
Used by 1 declaration in 1 file
lemma setI_closed_tuple_boxes source, line 95 
forall [d : measure_display] [T : measurableType d] [n : nat],
setI_closed (tuple_boxes (n:=n))
Statement as written in the source
Lemma setI_closed_tuple_boxes : setI_closed tuple_boxes.
Used by 1 declaration in 1 file
lemma measure_tuple_box_unique main result source, line 104 
forall [d : measure_display] [T : measurableType d] [n : nat] [R : realType]
  [mu1 mu2 : measure (n.-tuple T) R],
(mu1 [set: n.-tuple T] < +oo)%E ->
(forall A : 'I_n -> set T,
 (forall i : 'I_n, d.-measurable (A i)) -> mu1 (tuple_box A) = mu2 (tuple_box A)) ->
forall [X : set (n.-tuple T)], (measure_tuple_display d).-measurable X -> mu1 X = mu2 X

Two finite measures that agree on the boxes agree.

Main result

Stated in the README together with tuple_prod_pick.

Statement as written in the source
Lemma measure_tuple_box_unique (R : realType)
    (mu1 mu2 : {measure set (n.-tuple T) -> \bar R}) :
  (mu1 [set: n.-tuple T] < +oo)%E ->
  (forall A, (forall i, measurable (A i)) ->
    mu1 (tuple_box A) = mu2 (tuple_box A)) ->
  forall X, measurable X -> mu1 X = mu2 X.
Used by 6 declarations in 4 files
sectiontuple_prod_box
Context d (T : measurableType d) (R : realType).
lemma tuple_prod_box main result source, line 129 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] [A : 'I_n -> set T],
(forall i : 'I_n, d.-measurable (A i)) ->
tuple_prod mu n (tuple_box A) = (\prod_(i < n) mu i (A i))%E

tuple_prod mu n gives a box the product of the measures of its sides.

Main result

Stated in the README together with tuple_prod_pick.

Statement as written in the source
Lemma tuple_prod_box (mu : nat -> probability T R) n (A : 'I_n -> set T) :
  (forall i, measurable (A i)) ->
  tuple_prod mu n (tuple_box A) = (\prod_(i < n) mu i (A i))%E.
Used by 7 declarations in 5 files
sectiontuple_merge
Context d (T : measurableType d) (R : realType) (n : nat).
Variable S : {pred 'I_n}.
definition tuple_merge main result source, line 158
Type
forall [d : measure_display] [T : measurableType d] [n : nat],
{pred 'I_n} -> n.-tuple T -> n.-tuple T -> n.-tuple T
Definition
Definition tuple_merge (x y : n.-tuple T) : n.-tuple T :=
  [tuple if i \in S then tnth x i else tnth y i | i < n].

The coordinates in S from x, the others from y.

Main result, as the README states it

Conditioning tuple_prod mu n on the coordinates in a set S by resampling the others: tuple_merge S x y takes the coordinates in S from x and the others from y, and its law under two independent copies of tuple_prod mu n is tuple_prod mu n. If H depends only on the coordinates in S (H (tuple_merge S x y) = H x) and, for every x in H, tuple_merge S x y is in E with probability at most c x, then P(E and H) <= int_H c.

Used by 15 declarations in 4 files
lemma tnth_merge source, line 161 
forall [d : measure_display] [T : measurableType d] [n : nat] (S : {pred 'I_n})
  (x y : n.-tuple T) (i : 'I_n),
tnth (tuple_merge S x y) i = (if i \in S then tnth x i else tnth y i)
Statement as written in the source
Lemma tnth_merge x y i :
  tnth (tuple_merge x y) i = if i \in S then tnth x i else tnth y i.
Used by 7 declarations in 3 files
lemma measurable_tuple_merge source, line 165 
forall [d : measure_display] [T : measurableType d] [n : nat] (S : {pred 'I_n}),
measurable_fun
  [set: ((n.-tuple _) * (n.-tuple _))]
  (fun p : n.-tuple T * n.-tuple T => tuple_merge S p.1 p.2)
Statement as written in the source
Lemma measurable_tuple_merge :
  measurable_fun setT (fun p : n.-tuple T * n.-tuple T => tuple_merge p.1 p.2).
Used by 5 declarations in 2 files
Local Open Scope ereal_scope.
lemma tuple_prod_merge main result source, line 182 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [n : nat] (S : {pred 'I_n}) (mu : nat -> probability T R) [X : set (n.-tuple T)],
(measure_tuple_display d).-measurable X ->
(tuple_prod mu n \x tuple_prod mu n)%E
  ((fun p : n.-tuple T * n.-tuple T => tuple_merge S p.1 p.2) @^-1` X) =
tuple_prod mu n X

Resampling the coordinates outside S does not change a product law.

Main result

Stated in the README together with tuple_merge.

Statement as written in the source
Lemma tuple_prod_merge (mu : nat -> probability T R) (X : set (n.-tuple T)) :
  measurable X ->
  (tuple_prod mu n \x tuple_prod mu n)
    ((fun p : n.-tuple T * n.-tuple T => tuple_merge p.1 p.2) @^-1` X) =
  tuple_prod mu n X.
Used by 1 declaration in 1 file
sectiontuple_condition
Context d (T : measurableType d) (R : realType) (n : nat).
Variable S : {pred 'I_n}.
Local Open Scope ereal_scope.
lemma ge0_integral_tuple_prod_merge main result source, line 222 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [n : nat] (S : {pred 'I_n}) (mu : nat -> probability T R) [F : n.-tuple T -> \bar R],
measurable_fun [set: n.-tuple _] F ->
(forall x : n.-tuple T, (0%R <= F x)%E) ->
(\int[tuple_prod mu n]_x F x)%E =
(\int[tuple_prod mu n]_x \int[tuple_prod mu n]_y F (tuple_merge S x y))%E

The coordinates outside S may be resampled independently.

Main result

Stated in the README together with tuple_merge.

Statement as written in the source
Lemma ge0_integral_tuple_prod_merge (mu : nat -> probability T R)
    (F : n.-tuple T -> \bar R) :
  measurable_fun setT F -> (forall x, 0 <= F x) ->
  \int[tuple_prod mu n]_x F x =
  \int[tuple_prod mu n]_x \int[tuple_prod mu n]_y F (tuple_merge S x y).
Used by 3 declarations in 2 files
lemma measurable_merge_section source, line 241 
forall [d : measure_display] [T : measurableType d] [n : nat] (S : {pred 'I_n})
  [E : set (n.-tuple T)] (x : n.-tuple T),
(measure_tuple_display d).-measurable E ->
(measure_tuple_display d).-measurable [set y | E (tuple_merge S x y)]
Statement as written in the source
Lemma measurable_merge_section (E : set (n.-tuple T)) (x : n.-tuple T) :
  measurable E -> measurable [set y | E (tuple_merge S x y)].
Used by 2 declarations in 2 files
lemma tuple_prod_cond_le main result source, line 258 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [n : nat] [S : {pred 'I_n}] [mu : nat -> probability T R] [E H : set (n.-tuple T)]
  [c : n.-tuple T -> \bar R],
(measure_tuple_display d).-measurable E ->
(measure_tuple_display d).-measurable H ->
measurable_fun [set: n.-tuple _] c ->
(forall x : n.-tuple T, (0%R <= c x)%E) ->
(forall x y : n.-tuple T, H (tuple_merge S x y) = H x) ->
(forall x : n.-tuple T, H x -> (tuple_prod mu n [set y | E (tuple_merge S x y)] <= c x)%E) ->
(tuple_prod mu n (E `&` H) <= \int[tuple_prod mu n]_(x in H) c x)%E

If H depends only on the coordinates in S and, for x in H, resampling the coordinates outside S puts the tuple in E with probability at most c x, then E and H occur together with probability at most the integral of c over H.

Main result

Stated in the README together with tuple_merge.

Statement as written in the source
Lemma tuple_prod_cond_le (mu : nat -> probability T R)
    (E H : set (n.-tuple T)) (c : n.-tuple T -> \bar R) :
  measurable E -> measurable H -> measurable_fun setT c ->
  (forall x, 0 <= c x) ->
  (forall x y, H (tuple_merge S x y) = H x) ->
  (forall x, H x -> tuple_prod mu n [set y | E (tuple_merge S x y)] <= c x) ->
  tuple_prod mu n (E `&` H) <= \int[tuple_prod mu n]_(x in H) c x.
Used by 2 declarations in 2 files
lemma tuple_prod_indepS main result source, line 309 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [n : nat] [S : {pred 'I_n}] (mu : nat -> probability T R) [E F : set (n.-tuple T)],
(measure_tuple_display d).-measurable E ->
(measure_tuple_display d).-measurable F ->
(forall x y : n.-tuple T, E (tuple_merge S x y) = E x) ->
(forall x y : n.-tuple T, F (tuple_merge S x y) = F y) ->
tuple_prod mu n (E `&` F) = (tuple_prod mu n E * tuple_prod mu n F)%E

Events that depend on the coordinates in S and outside S are independent.

Main result, as the README states it

Events that depend on pairwise disjoint sets of coordinates are independent. Revealing the coordinates in nested sets S 0, S 1, ...: if A l depends only on the coordinates in S (l + 1) and, given those in S l of a tuple of A 0, ..., A (l - 1), has probability at most c l, then P(A 0, ..., A (L - 1)) <= c 0 ... c (L - 1).

Statement as written in the source
Lemma tuple_prod_indepS (mu : nat -> probability T R)
    (E F : set (n.-tuple T)) :
  measurable E -> measurable F ->
  (forall x y, E (tuple_merge S x y) = E x) ->
  (forall x y, F (tuple_merge S x y) = F y) ->
  tuple_prod mu n (E `&` F) = tuple_prod mu n E * tuple_prod mu n F.
Used by 1 declaration in 1 file
sectiontuple_dep
Context d (T : measurableType d) (n : nat).
lemma tuple_merge_id source, line 344 
forall [d : measure_display] [T : measurableType d] [n : nat] [S : {pred 'I_n}]
  [x y : n.-tuple T],
(forall i : 'I_n, i \in S -> tnth x i = tnth y i) -> tuple_merge S x y = y
Statement as written in the source
Lemma tuple_merge_id (S : {pred 'I_n}) (x y : n.-tuple T) :
  (forall i, i \in S -> tnth x i = tnth y i) -> tuple_merge S x y = y.
Used by 2 declarations in 1 file
lemma tuple_merge_dep_sub source, line 353 
forall [d : measure_display] [T : measurableType d] [n : nat] [S U : {pred 'I_n}]
  [E : set (n.-tuple T)],
(forall x y : n.-tuple T, E (tuple_merge S x y) = E x) ->
{subset S <= U} -> forall x y : n.-tuple T, E (tuple_merge U x y) = E x

An event that depends only on the coordinates in S depends only on the coordinates in any U that contains S.

Statement as written in the source
Lemma tuple_merge_dep_sub (S U : {pred 'I_n}) (E : set (n.-tuple T)) :
  (forall x y, E (tuple_merge S x y) = E x) -> {subset S <= U} ->
  forall x y, E (tuple_merge U x y) = E x.
Used by 2 declarations in 1 file
lemma tuple_merge_dep_disj source, line 364 
forall [d : measure_display] [T : measurableType d] [n : nat] [S U : {pred 'I_n}]
  [E : set (n.-tuple T)],
(forall x y : n.-tuple T, E (tuple_merge S x y) = E x) ->
(forall i : 'I_n, i \in S -> i \notin U) ->
forall x y : n.-tuple T, E (tuple_merge U x y) = E y

It does not depend on the coordinates in a U disjoint from S.

Statement as written in the source
Lemma tuple_merge_dep_disj (S U : {pred 'I_n}) (E : set (n.-tuple T)) :
  (forall x y, E (tuple_merge S x y) = E x) ->
  (forall i, i \in S -> i \notin U) ->
  forall x y, E (tuple_merge U x y) = E y.
Used by 1 declaration in 1 file
sectiontuple_indep
Context d (T : measurableType d) (R : realType) (n : nat).
Local Open Scope ereal_scope.
lemma tuple_prod_indep_big main result source, line 383 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [n : nat] (mu : nat -> probability T R) [k : nat] [S0 : nat -> {pred 'I_n}]
  [E : nat -> set (n.-tuple T)],
(forall j : nat, (j < k)%N -> (measure_tuple_display d).-measurable (E j)) ->
(forall (j j' : nat) (i : 'I_n),
 (j < k)%N -> (j' < k)%N -> j != j' -> i \in S0 j -> i \notin S0 j') ->
(forall (j : nat) (x y : n.-tuple T), (j < k)%N -> E j (tuple_merge (S0 j) x y) = E j x) ->
tuple_prod mu n (\bigcap_(j < k) E j) = (\prod_(j < k) tuple_prod mu n (E j))%E

Events that depend on pairwise disjoint sets of coordinates are independent.

Main result

Stated in the README together with tuple_prod_indepS.

Statement as written in the source
Lemma tuple_prod_indep_big (mu : nat -> probability T R) k
    (S : nat -> {pred 'I_n}) (E : nat -> set (n.-tuple T)) :
  (forall j, (j < k)%N -> measurable (E j)) ->
  (forall j j' i, (j < k)%N -> (j' < k)%N -> j != j' -> i \in S j ->
     i \notin S j') ->
  (forall j x y, (j < k)%N -> E j (tuple_merge (S j) x y) = E j x) ->
  tuple_prod mu n (\bigcap_(j < k) E j) = \prod_(j < k) tuple_prod mu n (E j).
Used by 1 declaration in 1 file
lemma tuple_prod_chain_le main result source, line 422 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [n : nat] [mu : nat -> probability T R] [L : nat] [S0 : nat -> {pred 'I_n}]
  [A : nat -> set (n.-tuple T)] [c : nat -> R],
(forall l : nat, (l < L)%N -> (measure_tuple_display d).-measurable (A l)) ->
(forall l : nat, {subset S0 l <= S0 l.+1}) ->
(forall (l : nat) (x y : n.-tuple T), (l < L)%N -> A l (tuple_merge (S0 l.+1) x y) = A l x) ->
(forall l : nat, (l < L)%N -> 0 <= c l) ->
(forall (l : nat) (x : n.-tuple T),
 (l < L)%N ->
 (\bigcap_(r < l) A r) x ->
 (tuple_prod mu n [set y | A l (tuple_merge (S0 l) x y)] <= (c l)%:E)%E) ->
(tuple_prod mu n (\bigcap_(l < L) A l) <= (\prod_(l < L) c l)%:E)%E

Revealing the coordinates in nested sets S 0, S 1, ...: if the event A l depends only on the coordinates in S l.+1 and, given the coordinates in S l of a tuple of the earlier events, has probability at most c l, then the events A l, l < L, occur together with probability at most the product of the c l.

Main result

Stated in the README together with tuple_prod_indepS.

Statement as written in the source
Lemma tuple_prod_chain_le (mu : nat -> probability T R) L
    (S : nat -> {pred 'I_n}) (A : nat -> set (n.-tuple T)) (c : nat -> R) :
  (forall l, (l < L)%N -> measurable (A l)) ->
  (forall l, {subset S l <= S l.+1}) ->
  (forall l x y, (l < L)%N -> A l (tuple_merge (S l.+1) x y) = A l x) ->
  (forall l, (l < L)%N -> (0 <= c l)%R) ->
  (forall l x, (l < L)%N -> (\bigcap_(r < l) A r) x ->
     tuple_prod mu n [set y | A l (tuple_merge (S l) x y)] <= (c l)%:E) ->
  tuple_prod mu n (\bigcap_(l < L) A l) <= (\prod_(l < L) c l)%:E.
sectiontuple_pick
Context d (T : measurableType d) (R : realType) (n k : nat).
Variable f : 'I_k -> 'I_n.
definition tuple_pick source, line 469
Type
forall [d : measure_display] [T : measurableType d] [n k : nat],
('I_k -> 'I_n) -> n.-tuple T -> k.-tuple T
Definition
Definition tuple_pick (x : n.-tuple T) : k.-tuple T :=
  [tuple tnth x (f i) | i < k].

The coordinates f 0, ..., f (k - 1) of x.

Used by 4 declarations in 2 files
lemma measurable_tuple_pick source, line 472 
forall [d : measure_display] [T : measurableType d] [n k : nat] (f : 'I_k -> 'I_n),
measurable_fun [set: n.-tuple _]
  (tuple_pick f)
Statement as written in the source
Lemma measurable_tuple_pick : measurable_fun setT tuple_pick.
Used by 2 declarations in 2 files
lemma tuple_prod_pick main result source, line 482 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [n k : nat] [f : 'I_k -> 'I_n] [mu nu : nat -> probability T R] 
  [B : set (k.-tuple T)],
injective f ->
(forall i : 'I_k, nu i = mu (f i)) ->
(measure_tuple_display d).-measurable B ->
tuple_prod mu n (tuple_pick f @^-1` B) = tuple_prod nu k B

For an injective f, the coordinates f 0, ..., f (k - 1) of a product law have the product law of their laws.

Main result, as the README states it

For an injective f : 'I_k -> 'I_n, the coordinates f 0, ..., f (k - 1) of tuple_prod mu n have the law tuple_prod nu k with nu i = mu (f i). The measure of a box is the product of the measures of its sides, and two finite measures on n.-tuple T that agree on the boxes agree.

Statement as written in the source
Lemma tuple_prod_pick (mu nu : nat -> probability T R)
    (B : set (k.-tuple T)) :
  injective f -> (forall i : 'I_k, nu i = mu (f i)) -> measurable B ->
  tuple_prod mu n (tuple_pick @^-1` B) = tuple_prod nu k B.
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.