On this page
Countable mixtures of probabilities
Imports 3 library modules and 25 external
- GaussianAnalysis.probability.lindeberg
- GaussianAnalysis.probability.conditioning
- GaussianAnalysis.probability.mixture
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.boot.finfun, 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.esum, mathcomp.analysis.exp, mathcomp.classical.cardinality, 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, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic
The mixture of probabilities P s, s : nat, with weights p s >= 0 of sum one, and the sums over the tuples of labels that describe n independent draws from it. The weights are a proof argument of the mixture, as in probability/mixture.v.
cmixture_ | p s >= 0 for every s and \sum_(s <oo) p s = 1 |
cmixture P hp | for hp : cmixture_weights p, the probability A |-> \sum_(s <oo) p s P s (A) |
cmixture_ | r_m = \sum_(s > m) p s, the weight of the labels above m |
cmixture_ | p s / r_m for s > m and 0 otherwise, the weights of the normalized tail |
labels_ | the n-tuples of labels in nat that are all <= m |
Main results:
- cmixtureE: cmixture P hp A = \sum_(s <oo) p s P s (A); the mixture is the measure series mseries of the scaled probabilities p s P s;
- ge0_integral_cmixture, integral_cmixture: \int f d(cmixture P hp) = \sum_s p s \int f dP_s for f nonnegative and measurable, and for f integrable under every P s with \sum_s p s \int |f| dP_s < +oo, which is then integrable under the mixture (from ge0_integral_measure_series and integral_measure_series);
- cmixture_tailE, cmixture_tail_small, cmixture_tail_series, cmixture_tail_weights: \sum_(s <= m) p s + r_m = 1, r_m tends to 0, and for r_m > 0 the normalized tail weights are mixture weights, so that cmixture P with them is the normalized tail \sum_(s > m) p s P s / r_m;
- esumZl, esum_fin, esum_tuple_distr, esum_tuple_prod: an esum of nonnegative terms commutes with a nonnegative factor; over a subset of a finite type it is a finite sum; if the esum of a_i over nat is a real number x_i for every i < n, the esum over s : n.-tuple nat of \prod_i a_i (s_i) is \prod_i x_i (the countable big_tuple_distr), so it is x^n when every a_i is a;
- label_esum1, label_esum_le: the product weights \prod_i p (s_i) of the label tuples have sum one, and sum (1 - r_m)^n over labels_le n m;
- label_coupling, bernoulli_tail: an esum over the label tuples in nat and a finite sum over the label tuples in 'I_N, of product weights times probabilities, whose weights and probabilities agree on the tuples with all labels at most m, differ by at most 1 - (1 - r_m)^n <= n r_m on every measurable set;
- tuple_prod_cmixture: n independent draws from a countable mixture: on every measurable set A of n-tuples, tuple_prod (fun=> cmixture P hp) n A is the esum over the label tuples s : n.-tuple nat of \prod_i p (s_i) times tuple_prod (fun k => P (s_k)) n A (the countable form of tuple_prod_mixture; both sides are measures that agree on boxes, the right one written as a countable mixture over nat through pickle).
Main results
| Results | Statement |
|---|---|
The countable mixture of probabilities P s, s : nat, with weights p s >= 0 of sum one (\sum_(s <oo) p s = 1), a probability: the measure series of the scaled P s. For f nonnegative and measurable, and for f integrable under every P s with sum_s p_s int |f| dP_s < +oo, int f d(mixture) = sum_s p_s int f dP_s; in the second case f is integrable under the mixture. | |
The weight r_m = sum_(s > m) p_s of the labels above m, with sum_(s <= m) p_s + r_m = 1; r_m is at most any eps > 0 for some m. For r_m > 0 the weights p_s / r_m, s > m, are mixture weights (the normalized tail sum_(s > m) p_s P_s / r_m), and a series of nonnegative terms against them is 1 / r_m times the series over s > m against p. | |
For nonnegative terms, esum (c x_i) = c esum x_i (c >= 0); an esum over a subset of a finite type is a finite sum; if the esum over nat of the nonnegative a_i is a real number x_i for every i < n, the esum over s : n.-tuple nat of prod_i a_i (s_i) is prod_i x_i (the countable form of big_tuple_distr), in particular x^n when every a_i is a. Hence the product weights prod_i p (s_i) of the label tuples have sum one, and sum (1 - r_m)^n over the tuples whose labels are all at most m (labels_le n m). | |
The coupling of label tuples. A mixture esum_(s : n.-tuple nat) prod_i p (s_i) Q_s(A) and a finite mixture sum_(t : n.-tuple 'I_N) prod_i q (t_i) Q'_t(A), m < N, whose weights and probabilities agree on the tuples with all labels at most m, differ by at most 1 - (1 - r_m)^n on every measurable A; and 1 - (1 - r)^n <= n r for 0 <= r <= 1. | |
n independent draws from a countable mixture: for weights p with cmixture_weights p, probabilities P s (s : nat) and every measurable set A of n-tuples, tuple_prod (fun=> cmixture P hp) n A is the esum over the label tuples s : n.-tuple nat of prod_k p (s_k) times tuple_prod (fun k => P (s_k)) n A; the countable form of tuple_prod_mixture. |
Declarations24 exported, 16 local
forall [R : realType], (nat -> R) -> Prop
Definition cmixture_weights (R : realType) (p : nat -> R) : Prop := (forall s, 0 <= p s) /\ (\sum_(s <oo) (p s)%:E = 1)%E.
Weights p s >= 0, s : nat, of sum one.
The countable mixture of probabilities P s, s : nat, with weights p s >= 0 of sum one (\sum_(s <oo) p s = 1), a probability: the measure series of the scaled P s. For f nonnegative and measurable, and for f integrable under every P s with sum_s p_s int |f| dP_s < +oo, int f d(mixture) = sum_s p_s int f dP_s; in the second case f is integrable under the mixture.
Used by 3 declarations in 1 file
- this file: cmixture, cmixture_tail_weights, qw_weights
Context d (T : measurableType d) (R : realType). Variables (P : nat -> probability T R) (p : nat -> R). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType], (nat -> probability T R) -> forall [p : nat -> R], cmixture_weights p -> set T -> \bar R
Definition cmixture (hp : cmixture_weights p) (A : set T) : \bar R := \sum_(s <oo) (p s)%:E * P s A.
Stated in the README together with cmixture_weights.
Used by 12 declarations in 1 file
Variable hp : cmixture_weights p.
Let p0 s : (0 <= p s)%R.
Used by 2 declarations in 1 file
- this file: mterm, integral_cmixture
Let mterm (s : nat) : {measure set T -> \bar R} := mscale (NngNum (p0 s)) (P s).
Used by 4 declarations in 1 file
Used by 5 declarations in 1 file
Let cmixture0 : cmixture hp set0 = 0.
Used by 1 declaration in 1 file
- this file: instance at line 106
Let cmixture_ge0 A : 0 <= cmixture hp A.
Used by 1 declaration in 1 file
- this file: instance at line 106
Let cmixture_sigma_additive : semi_sigma_additive (cmixture hp).
Used by 1 declaration in 1 file
- this file: instance at line 106
HB.instance Definition _ := isMeasure.Build _ _ _ (cmixture hp) cmixture0 cmixture_ge0 cmixture_sigma_additive.
Let cmixture_setT : cmixture hp [set: T] = 1.
Used by 1 declaration in 1 file
- this file: instance at line 115
HB.instance Definition _ := @Measure_isProbability.Build _ _ R (cmixture hp) cmixture_setT.
forall [d : measure_display] [T : measurableType d] [R : realType] (P : nat -> probability T R) [p : nat -> R] (hp : cmixture_weights p) (A : set T), cmixture P hp A = \big[+%E/0]_(0 <= s <oo) ((p s)%:E * P s A)%E
Stated in the README together with cmixture_weights.
Statement as written in the source
Lemma cmixtureE A : cmixture hp A = \sum_(s <oo) (p s)%:E * P s A.
Used by 2 declarations in 1 file
- this file: cmixture_pickle, tuple_prod_cmixture
forall [d : measure_display] [T : measurableType d] [R : realType] (P : nat -> probability T R) [p : nat -> R] (hp : cmixture_weights p) [D : set T] [f : T -> \bar R], d.-measurable D -> measurable_fun D f -> (forall x : T, D x -> (0%R <= f x)%E) -> (\int[cmixture P hp]_(x in D) f x)%E = \big[+%E/0]_(0 <= s <oo) ((p s)%:E * \int[P s]_(x in D) f x)%E
Stated in the README together with cmixture_weights.
Statement as written in the source
Lemma ge0_integral_cmixture (D : set T) (f : T -> \bar R) : measurable D -> measurable_fun D f -> (forall x, D x -> 0 <= f x) -> \int[cmixture hp]_(x in D) f x = \sum_(s <oo) (p s)%:E * \int[P s]_(x in D) f x.
Used by 1 declaration in 1 file
- this file: integral_cmixture
forall [d : measure_display] [T : measurableType d] [R : realType] [P : nat -> probability T R] [p : nat -> R] (hp : cmixture_weights p) [D : set T] [f : T -> \bar R], d.-measurable D -> measurable_fun D f -> (forall s : nat, (P s).-integrable D f) -> (\big[+%E/0%R]_(0 <= s <oo) ((p s)%:E * \int[P s]_(x in D) `|f x|) < +oo)%E -> (cmixture P hp).-integrable D f /\ (\int[cmixture P hp]_(x in D) f x)%E = \big[+%E/0]_(0 <= s <oo) ((p s)%:E * \int[P s]_(x in D) f x)%E
Stated in the README together with cmixture_weights.
Statement as written in the source
Lemma integral_cmixture (D : set T) (f : T -> \bar R) : measurable D -> measurable_fun D f -> (forall s, (P s).-integrable D f) -> \sum_(s <oo) (p s)%:E * \int[P s]_(x in D) `|f x| < +oo -> (cmixture hp).-integrable D f /\ \int[cmixture hp]_(x in D) f x = \sum_(s <oo) (p s)%:E * \int[P s]_(x in D) f x.
Context (R : realType) (p : nat -> R). Hypothesis hp : cmixture_weights p. Local Open Scope ereal_scope.
Let p0 s : (0 <= p s)%R.
Used by 2 declarations in 1 file
- this file: cmixture_tail_small, cmixture_tail_weights
forall [R : realType], (nat -> R) -> nat -> R
Definition cmixture_tail (m : nat) : R := fine (\sum_(s <oo | (m < s)%N) (p s)%:E).
The mass of the labels s > m.
The weight r_m = sum_(s > m) p_s of the labels above m, with sum_(s <= m) p_s + r_m = 1; r_m is at most any eps > 0 for some m. For r_m > 0 the weights p_s / r_m, s > m, are mixture weights (the normalized tail sum_(s > m) p_s P_s / r_m), and a series of nonnegative terms against them is 1 / r_m times the series over s > m against p.
Used by 7 declarations in 1 file
forall [R : realType] [p : nat -> R], cmixture_weights p -> forall m : nat, \big[+%E/0]_(0 <= s <oo | (m < s)%N) (p s)%:E = (cmixture_tail p m)%:E /\ \sum_(s < m.+1) p s + cmixture_tail p m = 1
Stated in the README together with cmixture_tail.
Statement as written in the source
Lemma cmixture_tailE (m : nat) : \sum_(s <oo | (m < s)%N) (p s)%:E = (cmixture_tail m)%:E /\ (\sum_(s < m.+1) p s + cmixture_tail m = 1)%R.
Used by 4 declarations in 1 file
- this file: cmixture_tail_small, cmixture_tail_weights, label_esum_le, label_coupling
forall [R : realType] [p : nat -> R], cmixture_weights p -> forall [eps : R], 0 < eps -> exists m : nat, cmixture_tail p m <= eps
The tail mass tends to zero: it is at most any eps > 0 from some m on.
Stated in the README together with cmixture_tail.
Statement as written in the source
Lemma cmixture_tail_small (eps : R) : (0 < eps)%R -> exists m, (cmixture_tail m <= eps)%R.
forall [R : realType], (nat -> R) -> nat -> nat -> R
Definition cmixture_tail_w (m s : nat) : R := (if (m < s)%N then p s / cmixture_tail m else 0)%R.
The normalized tail: the weights p s / r_m for s > m, and 0 for s <= m.
Stated in the README together with cmixture_tail.
Used by 2 declarations in 1 file
- this file: cmixture_tail_series, cmixture_tail_weights
forall [R : realType] [p : nat -> R], cmixture_weights p -> forall [m : nat] [F : nat -> \bar R], 0 < cmixture_tail p m -> (forall s : nat, (0%R <= F s)%E) -> \big[+%E/0]_(0 <= s <oo) ((cmixture_tail_w p m s)%:E * F s)%E = (((cmixture_tail p m)^-1)%:E * \big[+%E/0%R]_(0 <= s <oo | (m < s)%N) ((p s)%:E * F s))%E
Stated in the README together with cmixture_tail.
Statement as written in the source
Lemma cmixture_tail_series m (F : nat -> \bar R) : (0 < cmixture_tail m)%R -> (forall s, 0 <= F s) -> \sum_(s <oo) (cmixture_tail_w m s)%:E * F s = ((cmixture_tail m)^-1)%:E * \sum_(s <oo | (m < s)%N) (p s)%:E * F s.
Used by 1 declaration in 1 file
- this file: cmixture_tail_weights
forall [R : realType] [p : nat -> R], cmixture_weights p -> forall [m : nat], 0 < cmixture_tail p m -> cmixture_weights (cmixture_tail_w p m)
Stated in the README together with cmixture_tail.
Statement as written in the source
Lemma cmixture_tail_weights m : (0 < cmixture_tail m)%R -> cmixture_weights (cmixture_tail_w m).
Context (R : realType). Local Open Scope ereal_scope.
forall [R : realType] [I : choiceType] [S : set I] [a : I -> \bar R] [c : R], 0 <= c -> (forall i : I, S i -> (0%R <= a i)%E) -> \esum_(i in S) (c%:E * a i)%E = (c%:E * (\esum_(i in S) a i))%E
For nonnegative terms, esum (c x_i) = c esum x_i (c >= 0); an esum over a subset of a finite type is a finite sum; if the esum over nat of the nonnegative a_i is a real number x_i for every i < n, the esum over s : n.-tuple nat of prod_i a_i (s_i) is prod_i x_i (the countable form of big_tuple_distr), in particular x^n when every a_i is a. Hence the product weights prod_i p (s_i) of the label tuples have sum one, and sum (1 - r_m)^n over the tuples whose labels are all at most m (labels_le n m).
Statement as written in the source
Lemma esumZl (I : choiceType) (S : set I) (a : I -> \bar R) (c : R) : (0 <= c)%R -> (forall i, S i -> 0 <= a i) -> \esum_(i in S) (c%:E * a i) = c%:E * \esum_(i in S) a i.
Used by 1 declaration in 1 file
- this file: esum_tuple_distr
forall [R : realType] [n : nat] [a : 'I_n -> nat -> R] [x : 'I_n -> R], (forall (i : 'I_n) (k : nat), 0 <= a i k) -> (forall i : 'I_n, \esum_(k in [set: nat]) (a i k)%:E = (x i)%:E) -> \esum_(s in [set: n.-tuple nat]) (\prod_(i < n) a i (tnth s i))%:E = (\prod_(i < n) x i)%:E
The esum over the n-tuples of labels of products is the product of the esums over the labels: the countable form of big_tuple_distr.
Stated in the README together with esumZl.
Statement as written in the source
Lemma esum_tuple_distr (n : nat) (a : 'I_n -> nat -> R) (x : 'I_n -> R) : (forall i k, (0 <= a i k)%R) -> (forall i, \esum_(k in [set: nat]) (a i k)%:E = (x i)%:E) -> \esum_(s in [set: n.-tuple nat]) (\prod_(i < n) a i (tnth s i))%:E = (\prod_(i < n) x i)%:E.
Used by 2 declarations in 1 file
- this file: esum_tuple_prod, tuple_prod_cmixture
forall [R : realType] [a : nat -> R] [x : R] (n : nat), (forall k : nat, 0 <= a k) -> \esum_(k in [set: nat]) (a k)%:E = x%:E -> \esum_(s in [set: n.-tuple nat]) (\prod_(i < n) a (tnth s i))%:E = (x ^+ n)%:E
The sum over the n-tuples of labels of the product weights is the n-th power of the sum of the weights.
Stated in the README together with esumZl.
Statement as written in the source
Lemma esum_tuple_prod (a : nat -> R) (x : R) (n : nat) : (forall k, (0 <= a k)%R) -> \esum_(k in [set: nat]) (a k)%:E = x%:E -> \esum_(s in [set: n.-tuple nat]) (\prod_(i < n) a (tnth s i))%:E = (x ^+ n)%:E.
Used by 2 declarations in 1 file
- this file: label_esum1, label_esum_le
forall [R : realType] [T : finType] [P : pred T] [a : T -> \bar R], (forall t : T, P t -> (0%R <= a t)%E) -> \esum_(t in [set t | P t]) a t = \sum_(t | P t) a t
An esum over a subset of a finite type is a finite sum.
Stated in the README together with esumZl.
Statement as written in the source
Lemma esum_fin (T : finType) (P : pred T) (a : T -> \bar R) : (forall t, P t -> 0 <= a t) -> \esum_(t in [set t | P t]) a t = \sum_(t | P t) a t.
Used by 1 declaration in 1 file
- this file: label_coupling
forall [R : realType] [r : R] (n : nat), 0 <= r <= 1 -> 1 - (1 - r) ^+ n <= n%:R * r
Bernoulli's inequality, as used for the mass of the label tuples with some label above m.
Stated in the README together with label_coupling.
Statement as written in the source
Lemma bernoulli_tail (r : R) (n : nat) : (0 <= r <= 1)%R -> (1 - (1 - r) ^+ n <= n%:R * r)%R.
Context (R : realType) (p : nat -> R). Hypothesis hp : cmixture_weights p. Local Open Scope ereal_scope.
forall [R : realType] [p : nat -> R], cmixture_weights p -> \esum_(k in [set: nat]) (p k)%:E = 1%E
Statement as written in the source
Lemma cmixture_weights_esum : \esum_(k in [set: nat]) (p k)%:E = 1.
Used by 1 declaration in 1 file
- this file: label_esum1
forall [R : realType] [p : nat -> R], cmixture_weights p -> forall n : nat, \esum_(s in [set: n.-tuple nat]) (\prod_(i < n) p (tnth s i))%:E = 1%E
The label tuples s : n.-tuple nat: the product weights have sum one.
Stated in the README together with esumZl.
Statement as written in the source
Lemma label_esum1 n : \esum_(s in [set: n.-tuple nat]) (\prod_(i < n) p (tnth s i))%:E = 1.
Used by 2 declarations in 1 file
- this file: label_coupling, qw_weights
forall [n : nat], nat -> set (n.-tuple nat)
Definition labels_le (n m : nat) : set (n.-tuple nat) := [set s | all (fun k => (k <= m)%N) s].
The label tuples whose labels are all at most m.
Used by 2 declarations in 1 file
- this file: label_esum_le, label_coupling
Arguments labels_le : clear implicits.
forall [R : realType] [p : nat -> R], cmixture_weights p -> forall n m : nat, \esum_(s in labels_le m) (\prod_(i < n) p (tnth s i))%:E = ((1 - cmixture_tail p m) ^+ n)%:E
Stated in the README together with esumZl.
Statement as written in the source
Lemma label_esum_le n m : \esum_(s in labels_le n m) (\prod_(i < n) p (tnth s i))%:E = ((1 - cmixture_tail p m) ^+ n)%:E.
Used by 1 declaration in 1 file
- this file: label_coupling
forall [R : realType] [p : nat -> R], cmixture_weights p -> forall [dT : measure_display] [T : measurableType dT] [n m N : nat] [q : nat -> R] [Q : n.-tuple nat -> probability T R] [Q' : n.-tuple 'I_N -> probability T R] [A : set T], dT.-measurable A -> (m < N)%N -> (forall k : nat, (k < N)%N -> 0 <= q k) -> \sum_(k < N) q k = 1 -> (forall k : nat, (k <= m)%N -> q k = p k) -> (forall t : n.-tuple 'I_N, all (fun k : 'I_N => (k <= m)%N) t -> Q' t A = Q (map_tuple (nat_of_ord (n:=N)) t) A) -> (`|\esum_(s in [set: n.-tuple nat]) (\prod_(i < n) p (tnth s i))%:E * Q s A - (\sum_t ((\prod_(i < n) q (tnth t i))%:E * Q' t A)%E)%R| <= (1 - (1 - cmixture_tail p m) ^+ n)%:E)%E
The coupling of label tuples. A mixture over the tuples s of labels in nat, with the product weights of p, and a mixture over the tuples t of labels in 'I_N, with the product weights of q, whose weights and laws agree on the tuples with all labels at most m, differ by at most the mass 1 - (1 - r_m)^n of the tuples with some label above m.
The coupling of label tuples. A mixture esum_(s : n.-tuple nat) prod_i p (s_i) Q_s(A) and a finite mixture sum_(t : n.-tuple 'I_N) prod_i q (t_i) Q'_t(A), m < N, whose weights and probabilities agree on the tuples with all labels at most m, differ by at most 1 - (1 - r_m)^n on every measurable A; and 1 - (1 - r)^n <= n r for 0 <= r <= 1.
Statement as written in the source
Lemma label_coupling dT (T : measurableType dT) (n m N : nat) (q : nat -> R) (Q : n.-tuple nat -> probability T R) (Q' : n.-tuple 'I_N -> probability T R) (A : set T) : measurable A -> (m < N)%N -> (forall k, (k < N)%N -> (0 <= q k)%R) -> (\sum_(k < N) q k = 1)%R -> (forall k, (k <= m)%N -> q k = p k) -> (forall t : n.-tuple 'I_N, all (fun k : 'I_N => (k <= m)%N) t -> Q' t A = Q (map_tuple (@nat_of_ord N) t) A) -> `|\esum_(s in [set: n.-tuple nat]) (\prod_(i < n) p (tnth s i))%:E * Q s A - \sum_(t : n.-tuple 'I_N) (\prod_(i < n) q (tnth t i))%:E * Q' t A| <= (1 - (1 - cmixture_tail p m) ^+ n)%:E.
Context d (T : measurableType d) (R : realType). Variables (P : nat -> probability T R) (p : nat -> R). Hypothesis hp : cmixture_weights p. Variable n : nat. Local Open Scope ereal_scope.
Let lw (s : n.-tuple nat) : R := \prod_(i < n) p (tnth s i).
The weight and the law of the label tuple s.
Used by 4 declarations in 1 file
- this file: lw0, qw, qw_weights, cmixture_pickle
Let lQ (s : n.-tuple nat) : probability (n.-tuple T) R := tuple_prod (fun k => P (nth 0%N s k)) n.
Used by 3 declarations in 1 file
- this file: qP, cmixture_pickle, tuple_prod_cmixture
Let lw0 s : (0 <= lw s)%R.
Used by 1 declaration in 1 file
- this file: qw_weights
Let esum_pickle (G : n.-tuple nat -> \bar R) : (forall s, 0 <= G s) -> \esum_(k in [set: nat]) (if pickle_inv k is Some s then G s else 0) = \esum_(s in [set: n.-tuple nat]) G s.
An esum over the label tuples, read through the enumeration pickle.
Used by 2 declarations in 1 file
- this file: qw_weights, cmixture_pickle
Let qw (k : nat) : R := if pickle_inv k is Some s then lw s else 0%R.
The label tuples as a countable mixture indexed by nat.
Used by 2 declarations in 1 file
- this file: qw_weights, cmixture_pickle
Let qP (k : nat) : probability (n.-tuple T) R := if pickle_inv k is Some s then lQ s else lQ [tuple 0%N | _ < n].
Used by 2 declarations in 1 file
- this file: cmixture_pickle, tuple_prod_cmixture
Let qw_weights : cmixture_weights qw.
Used by 2 declarations in 1 file
- this file: cmixture_pickle, tuple_prod_cmixture
Let cmixture_pickle (A : set (n.-tuple T)) : cmixture qP qw_weights A = \esum_(s in [set: n.-tuple nat]) (lw s)%:E * lQ s A.
Used by 1 declaration in 1 file
- this file: tuple_prod_cmixture
forall [d : measure_display] [T : measurableType d] [R : realType] (P : nat -> probability T R) [p : nat -> R] (hp : cmixture_weights p) [n : nat] [A : set (n.-tuple T)], (measure_tuple_display d).-measurable A -> tuple_prod (fun=> cmixture P hp) n A = \esum_(s in [set: n.-tuple nat]) ((\prod_(i < n) p (tnth s i))%:E * tuple_prod (fun k : nat => P (nth 0%N s k)) n A)%E
n independent draws from a countable mixture: the countable form of tuple_prod_mixture.
n independent draws from a countable mixture: for weights p with cmixture_weights p, probabilities P s (s : nat) and every measurable set A of n-tuples, tuple_prod (fun=> cmixture P hp) n A is the esum over the label tuples s : n.-tuple nat of prod_k p (s_k) times tuple_prod (fun k => P (s_k)) n A; the countable form of tuple_prod_mixture.
Statement as written in the source
Lemma tuple_prod_cmixture (A : set (n.-tuple T)) : measurable A -> tuple_prod (fun=> cmixture P hp) n A = \esum_(s in [set: n.-tuple nat]) (\prod_(i < n) p (tnth s i))%:E * tuple_prod (fun k => P (nth 0%N s k)) n A.