On this page

Finite mixtures of probabilities

GaussianAnalysis.probability.mixturelibrary/probability/mixture.v400 lines18 lemmas and theorems, 2 definitionssource

Imports 4 library modules and 24 external

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.exp, 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.hoelder, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 2

Required by 19 files of the paper proofs

The mixture of probabilities P i, i in a finite type I, with weights w i: the law of a variable drawn from P i with probability w i. The weights are nonnegative of sum one, a proof argument of the mixture, as uniform_prob takes a < b.

`mixture_weights w`	w i >= 0 for every i and \sum_i w i = 1
`mixture P hw`	for hw : mixture_weights w, the probability A \|-> \sum_i w i P i (A)

Main results:

mixtureE: mixture P hw A = \sum_i w i P i (A);
ge0_integral_mixture, integrable_mixture, integral_mixture, expectation_mixture: \int f d(mixture P hw) = \sum_i w i \int f dP_i for f nonnegative and measurable, or integrable under every P i, and then f is integrable under the mixture; Lfun1_mixture and Lfun2_mixture for L^1 and L^2;

variance_mixture: the law of total variance,

Var X = \sum_i w i (Var_i X + (E_i X - E X)^2);

subgaussian_mixture, subexponential_mixture: a variable subgaussian (subexponential) with constant K under every P i is so under the mixture;
distribution_mixture: the image of a mixture by a measurable map is the mixture of the images;
big_tuple_distr, mixture_weights_prod: \sum over s : n.-tuple I of \prod_k F k (s_k) is \prod_k \sum_i F k i, so the product weights are mixture weights;
tuple_prod_mixture: the product of n copies of a mixture is the mixture, over the label tuples s with the product weights, of the products tuple_prod (fun k => P (s_k)) n: on boxes by bigA_distr_bigA, then measure_tuple_box_unique;
mixture_cover: measurable sets E i with P i (E i) <= eps that all contain a set F have a measurable intersection, containing F, of mixture probability at most eps.

Main results

Results	Statement
mixture_weightsmixturemixtureEge0_integral_mixtureintegrable_mixtureintegral_mixtureexpectation_mixtureLfun1_mixtureLfun2_mixture	The finite mixture of probabilities `P i` (`i` in a finite type) with weights `w i >= 0` of sum one, a probability; for `f` nonnegative and measurable, or integrable under every `P i`, `int f d(mixture) = sum_i w_i int f dP_i`, and an integrable (square integrable) variable under every `P i` is so under the mixture.
variance_mixturesubgaussian_mixturesubexponential_mixturedistribution_mixturemixture_cover	The law of total variance, `Var X = sum_i w_i (Var_i X + (E_i X - E X)^2)`, for `X` square integrable under every `P i` (`X \in Lfun (P i) 2`); a variable subgaussian (subexponential) with constant `K` under every `P i` is so under the mixture; the image of a mixture by a measurable map is the mixture of the images; measurable sets `E i` with `P i (E i) <= eps` that all contain `F` have a measurable intersection, containing `F`, of mixture probability at most `eps`.
big_tuple_distrmixture_weights_prodtuple_prod_mixture	`sum_(s : n-tuples) prod_k F k (s_k) = prod_k sum_i F k i`, so the product weights `prod_k w (s_k)` of the label tuples are mixture weights; the product `tuple_prod` of `n` copies of a mixture is the mixture, over the label tuples `s`, of the products `tuple_prod (fun k => P (s_k)) n`.

Declarations22 exported, 9 local

definition mixture_weights main result source, line 60

Type

forall [I : finType] [R : realType], (I -> R) -> Prop

Definition

Definition mixture_weights (I : finType) (R : realType) (w : I -> R) : Prop :=
  (forall i, 0 <= w i) /\ \sum_i w i = 1.

Main result, as the README states it

The finite mixture of probabilities P i (i in a finite type) with weights w i >= 0 of sum one, a probability; for f nonnegative and measurable, or integrable under every P i, int f d(mixture) = sum_i w_i int f dP_i, and an integrable (square integrable) variable under every P i is so under the mixture.

Used by 2 declarations in 1 file

this file: mixture, mixture_weights_prod

sectionmixture_weights_props

Context (I : finType) (R : realType) (w : I -> R) (hw : mixture_weights w).

lemma mixture_weights_ge0 source, line 66

forall [I : finType] [R : realType] [w : I -> R],
mixture_weights w -> forall i : I, 0 <= w i

Statement as written in the source

Lemma mixture_weights_ge0 i : 0 <= w i.

Used by 3 declarations in 2 files

this file: w0, mixture_weights_prod
GaussianAnalysis.convex.feature_mixture: w0

lemma mixture_weights_sum source, line 69

forall [I : finType] [R : realType] [w : I -> R], mixture_weights w -> \sum_i w i = 1

Statement as written in the source

Lemma mixture_weights_sum : \sum_i w i = 1.

Used by 8 declarations in 2 files

this file: mixture_weights_inhabited, mixture_setT, variance_mixture, subgaussian_mixture, subexponential_mixture, mixture_cover, mixture_weights_prod
GaussianAnalysis.convex.feature_mixture: sum_w

lemma mixture_weights_inhabited source, line 73

forall [I : finType] [R : realType] [w : I -> R], mixture_weights w -> exists _ : I, true

Weights of sum one live on a nonempty type.

Statement as written in the source

Lemma mixture_weights_inhabited : exists i : I, true.

Used by 5 declarations in 1 file

this file: integrable_mixture, integral_mixture, Lfun2_mixture, subgaussian_mixture, subexponential_mixture

HB declares canonical projections that the structures of the measure already provide; the warning says so. The setting lasts until the end of this file and is not exported.

Set Warnings "-redundant-canonical-projection".

sectionmixture

Context d (T : measurableType d) (R : realType) (I : finType).
Variables (w : I -> R) (P : I -> probability T R).
Local Open Scope ereal_scope.

definition mixture main result source, line 92

Type

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R],
(I -> probability T R) -> mixture_weights w -> set T -> \bar R

Definition

Definition mixture (hw : mixture_weights w) (A : set T) : \bar R :=
  \sum_i (w i)%:E * P i A.

Main result

Stated in the README together with mixture_weights.

Used by 22 declarations in 2 files

this file: mixture0, mixture_ge0, mixture_sigma_additive, instance at line 115, mixture_setT, instance at line 125, mixtureE, mixture_msum, ge0_integral_mixture, integrable_mixture, integral_mixture, expectation_mixture, Lfun1_mixture, Lfun2_mixture, variance_mixture, subgaussian_mixture, subexponential_mixture, mixture_cover, distribution_mixture, tuple_prod_mixture
GaussianAnalysis.convex.feature_mixture: mixture_regular_feature_dot, mixture_regular_feature

Variable hw : mixture_weights w.

let w0 section-local source, line 97

Let w0 i : (0 <= w i)%R.

Used by 2 declarations in 1 file

this file: mterm, mtermE

let mixture0 section-local source, line 99

Let mixture0 : mixture hw set0 = 0.

Used by 1 declaration in 1 file

this file: instance at line 115

let mixture_ge0 section-local source, line 102

Let mixture_ge0 A : 0 <= mixture hw A.

Used by 2 declarations in 1 file

this file: mixture_sigma_additive, instance at line 115

let mixture_sigma_additive section-local source, line 105

Let mixture_sigma_additive : semi_sigma_additive (mixture hw).

Used by 1 declaration in 1 file

this file: instance at line 115

instance instance at line 115 source, line 115

HB.instance Definition _ := isMeasure.Build _ _ _ (mixture hw)
  mixture0 mixture_ge0 mixture_sigma_additive.

let mixture_setT section-local source, line 118

Let mixture_setT : mixture hw [set: T] = 1.

Used by 1 declaration in 1 file

this file: instance at line 125

instance instance at line 125 source, line 125

HB.instance Definition _ :=
  @Measure_isProbability.Build _ _ R (mixture hw) mixture_setT.

lemma mixtureE main result source, line 128

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] (P : I -> probability T R) (hw : mixture_weights w)
  (A : set T),
mixture P hw A = \sum_i ((w i)%:E * P i A)%E

Main result

Stated in the README together with mixture_weights.

Statement as written in the source

Lemma mixtureE A : mixture hw A = \sum_i (w i)%:E * P i A.

Used by 2 declarations in 1 file

this file: mixture_cover, tuple_prod_mixture

let mterm section-local source, line 132

Let mterm (k : nat) : {measure set T -> \bar R} :=
  if insub k : option 'I_#|I| is Some o then
    mscale (NngNum (w0 (enum_val o))) (P (enum_val o))
  else mzero.

The mixture as a finite sum of scaled measures, indexed by nat.

Used by 3 declarations in 1 file

this file: mtermE, mixture_msum, ge0_integral_mixture

let mtermE section-local source, line 137

Let mtermE (k : 'I_#|I|) :
  mterm k = mscale (NngNum (w0 (enum_val k))) (P (enum_val k)).

Used by 2 declarations in 1 file

this file: mixture_msum, ge0_integral_mixture

let sum_enum section-local source, line 141

Let sum_enum (F : I -> \bar R) : \sum_i F i = \sum_(k < #|I|) F (enum_val k).

Used by 2 declarations in 1 file

this file: mixture_msum, ge0_integral_mixture

let mixture_msum section-local source, line 144

Let mixture_msum A : mixture hw A = msum mterm #|I| A.

Used by 1 declaration in 1 file

this file: ge0_integral_mixture

lemma ge0_integral_mixture main result source, line 150

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] (P : I -> probability T R) (hw : mixture_weights w)
  [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[mixture P hw]_(x in D) f x)%E = \sum_i ((w i)%:E * \int[P i]_(x in D) f x)%E

Main result

Stated in the README together with mixture_weights.

Statement as written in the source

Lemma ge0_integral_mixture (D : set T) (f : T -> \bar R) :
  measurable D -> measurable_fun D f -> (forall x, D x -> 0 <= f x) ->
  \int[mixture hw]_(x in D) f x = \sum_i (w i)%:E * \int[P i]_(x in D) f x.

Used by 5 declarations in 2 files

this file: integrable_mixture, integral_mixture, subgaussian_mixture, subexponential_mixture
GaussianAnalysis.convex.feature_mixture: mixture_regular_feature_dot

lemma integrable_mixture main result source, line 161

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] [P : I -> probability T R] (hw : mixture_weights w)
  [D : set T] [f : T -> \bar R],
d.-measurable D -> (forall i : I, (P i).-integrable D f) -> (mixture P hw).-integrable D f

Main result

Stated in the README together with mixture_weights.

Statement as written in the source

Lemma integrable_mixture (D : set T) (f : T -> \bar R) : measurable D ->
  (forall i, (P i).-integrable D f) -> (mixture hw).-integrable D f.

Used by 2 declarations in 1 file

this file: Lfun1_mixture, Lfun2_mixture

lemma integral_mixture main result source, line 175

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] [P : I -> probability T R] (hw : mixture_weights w)
  [D : set T] [f : T -> \bar R],
d.-measurable D ->
(forall i : I, (P i).-integrable D f) ->
(\int[mixture P hw]_(x in D) f x)%E = \sum_i ((w i)%:E * \int[P i]_(x in D) f x)%E

Main result

Stated in the README together with mixture_weights.

Statement as written in the source

Lemma integral_mixture (D : set T) (f : T -> \bar R) : measurable D ->
  (forall i, (P i).-integrable D f) ->
  \int[mixture hw]_(x in D) f x = \sum_i (w i)%:E * \int[P i]_(x in D) f x.

Used by 1 declaration in 1 file

this file: expectation_mixture

lemma expectation_mixture main result source, line 204

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] [P : I -> probability T R] (hw : mixture_weights w)
  [X : T -> R],
(forall i : I, X \in Lfun (P i) 1) ->
('E_(mixture P hw)[X])%E = \sum_i ((w i)%:E * 'E_(P i)[X])%E

Main result

Stated in the README together with mixture_weights.

Statement as written in the source

Lemma expectation_mixture (X : T -> R) : (forall i, X \in Lfun (P i) 1) ->
  'E_(mixture hw)[X] = \sum_i (w i)%:E * 'E_(P i)[X].

Used by 2 declarations in 2 files

this file: variance_mixture
GaussianAnalysis.convex.feature_mixture: mixture_regular_feature_dot

lemma Lfun1_mixture main result source, line 211

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] [P : I -> probability T R] (hw : mixture_weights w)
  [X : T -> R],
(forall i : I, X \in Lfun (P i) 1) -> X \in Lfun (mixture P hw) 1

Main result

Stated in the README together with mixture_weights.

Statement as written in the source

Lemma Lfun1_mixture (X : T -> R) : (forall i, X \in Lfun (P i) 1) ->
  X \in Lfun (mixture hw) 1.

lemma Lfun2_mixture main result source, line 218

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] [P : I -> probability T R] (hw : mixture_weights w)
  [X : T -> R],
(forall i : I, X \in Lfun (P i) 2) -> X \in Lfun (mixture P hw) 2

Main result

Stated in the README together with mixture_weights.

Statement as written in the source

Lemma Lfun2_mixture (X : T -> R) : (forall i, X \in Lfun (P i) 2%:E) ->
  X \in Lfun (mixture hw) 2%:E.

Used by 1 declaration in 1 file

this file: variance_mixture

lemma variance_mixture main result source, line 228

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] [P : I -> probability T R] (hw : mixture_weights w)
  [X : T -> R],
(forall i : I, X \in Lfun (P i) 2) ->
'V_(mixture P hw)[X] =
\sum_i ((w i)%:E * ('V_(P i)[X] + ('E_(P i)[X] - 'E_(mixture P hw)[X]) ^+ 2))%E

The law of total variance.

Main result, as the README states it

The law of total variance, Var X = sum_i w_i (Var_i X + (E_i X - E X)^2), for X square integrable under every P i (X \in Lfun (P i) 2); a variable subgaussian (subexponential) with constant K under every P i is so under the mixture; the image of a mixture by a measurable map is the mixture of the images; measurable sets E i with P i (E i) <= eps that all contain F have a measurable intersection, containing F, of mixture probability at most eps.

Statement as written in the source

Lemma variance_mixture (X : T -> R) : (forall i, X \in Lfun (P i) 2%:E) ->
  'V_(mixture hw)[X] =
    \sum_i (w i)%:E * ('V_(P i)[X] + ('E_(P i)[X] - 'E_(mixture hw)[X]) ^+ 2).

Used by 1 declaration in 1 file

GaussianAnalysis.convex.feature_mixture: mixture_regular_feature_dot

lemma subgaussian_mixture main result source, line 259

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] [P : I -> probability T R] (hw : mixture_weights w)
  [X : T -> R] [K : R],
(forall i : I, subgaussian (P i) X K) -> subgaussian (mixture P hw) X K

Main result

Stated in the README together with variance_mixture.

Statement as written in the source

Lemma subgaussian_mixture (X : T -> R) (K : R) :
  (forall i, subgaussian (P i) X K) -> subgaussian (mixture hw) X K.

lemma subexponential_mixture main result source, line 277

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] [P : I -> probability T R] (hw : mixture_weights w)
  [Y : T -> R] [L : R],
(forall i : I, subexponential (P i) Y L) -> subexponential (mixture P hw) Y L

Main result

Stated in the README together with variance_mixture.

Statement as written in the source

Lemma subexponential_mixture (Y : T -> R) (L : R) :
  (forall i, subexponential (P i) Y L) -> subexponential (mixture hw) Y L.

lemma mixture_cover main result source, line 298

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] [P : I -> probability T R] (hw : mixture_weights w)
  [E : I -> set T] [F : set T] [eps : R],
(forall i : I, d.-measurable (E i)) ->
(forall i : I, F `<=` E i) ->
(forall i : I, (P i (E i) <= eps%:E)%E) ->
[/\ d.-measurable (\bigcap_i E i), F `<=` \bigcap_i E i
  & (mixture P hw (\bigcap_i E i) <= eps%:E)%E]

Sets E i of small P i-probability that contain a set F: their intersection is a measurable event of small mixture probability that contains F.

Main result

Stated in the README together with variance_mixture.

Statement as written in the source

Lemma mixture_cover (E : I -> set T) (F : set T) (eps : R) :
  (forall i, measurable (E i)) -> (forall i, F `<=` E i) ->
  (forall i, P i (E i) <= eps%:E) ->
  [/\ measurable (\bigcap_(i in [set: I]) E i),
      F `<=` \bigcap_(i in [set: I]) E i &
      mixture hw (\bigcap_(i in [set: I]) E i) <= eps%:E].

sectionmixture_maps

Context d (T : measurableType d) (R : realType) (I : finType).
Variables (w : I -> R) (P : I -> probability T R) (hw : mixture_weights w).
Local Open Scope ereal_scope.

lemma distribution_mixture main result source, line 326

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] (P : I -> probability T R) (hw : mixture_weights w)
  [d' : measure_display] [T' : measurableType d'] (f : {mfun T >-> T'}) 
  (A : set T'),
distribution (mixture P hw) f A = mixture (fun i : I => distribution (P i) f) hw A

The image of a mixture is the mixture of the images.

Main result

Stated in the README together with variance_mixture.

Statement as written in the source

Lemma distribution_mixture d' (T' : measurableType d') (f : {mfun T >-> T'})
    (A : set T') :
  distribution (mixture P hw) f A =
  mixture (fun i => distribution (P i) f) hw A.

lemma big_tuple_distr main result source, line 335

forall [R : comPzSemiRingType] [I : finType] [n : nat] (F : 'I_n -> I -> R),
\sum_s \prod_(k < n) F k (tnth s k) = \prod_(k < n) \sum_i F k i

A sum over n-tuples of products is a product of sums.

Main result, as the README states it

sum_(s : n-tuples) prod_k F k (s_k) = prod_k sum_i F k i, so the product weights prod_k w (s_k) of the label tuples are mixture weights; the product tuple_prod of n copies of a mixture is the mixture, over the label tuples s, of the products tuple_prod (fun k => P (s_k)) n.

Statement as written in the source

Lemma big_tuple_distr (R : comPzSemiRingType) (I : finType) n
    (F : 'I_n -> I -> R) :
  \sum_(s : n.-tuple I) \prod_(k < n) F k (tnth s k) =
  \prod_(k < n) \sum_i F k i.

Used by 3 declarations in 2 files

this file: mixture_weights_prod, tuple_prod_mixture
GaussianAnalysis.probability.countable_mixture: label_coupling

lemma mixture_weights_prod main result source, line 348

forall [I : finType] [R : realType] [w : I -> R] (n : nat),
mixture_weights w -> mixture_weights (fun s : n.-tuple I => \prod_(k < n) w (tnth s k))

Main result

Stated in the README together with big_tuple_distr.

Statement as written in the source

Lemma mixture_weights_prod (I : finType) (R : realType) (w : I -> R) n :
  mixture_weights w ->
  mixture_weights (fun s : n.-tuple I => \prod_(k < n) w (tnth s k)).

Used by 1 declaration in 1 file

this file: tuple_prod_mixture

sectiontuple_prod_mixture

Context d (T : measurableType d) (R : realType) (I : finType).
Variables (w : I -> R) (P : I -> probability T R) (hw : mixture_weights w).
Local Open Scope ereal_scope.

lemma tuple_prod_mixture main result source, line 366

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : finType] [w : I -> R] (P : I -> probability T R) (hw : mixture_weights w) 
  (i0 : I) [n : nat] [A : set (n.-tuple T)],
(measure_tuple_display d).-measurable A ->
tuple_prod (fun=> mixture P hw) n A =
\sum_s ((\prod_(k < n) w (tnth s k))%:E * tuple_prod (fun k : nat => P (nth i0 s k)) n A)%E

The product of n copies of a mixture is the mixture, over the label tuples s with weights \prod_k w (s_k), of the products of the P (s_k); i0 is any label, for the indices past n.

Main result

Stated in the README together with big_tuple_distr.

Statement as written in the source

Lemma tuple_prod_mixture (i0 : I) n (A : set (n.-tuple T)) : measurable A ->
  tuple_prod (fun=> mixture P hw) n A =
  \sum_(s : n.-tuple I) (\prod_(k < n) w (tnth s k))%:E *
    tuple_prod (fun k => P (nth i0 s k)) n A.

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.