On this page
Mixtures of features
Imports 8 library modules and 25 external
- GaussianAnalysis.gaussian.measurable_matrix
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.matrix.opnorm
- GaussianAnalysis.matrix.real_spectral
- GaussianAnalysis.probability.moments
- GaussianAnalysis.probability.mixture
- GaussianAnalysis.convex.least_squares
- GaussianAnalysis.convex.feature_moments
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, 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
Required by 1 files of the paper proofs
A finite mixture (probability/mixture.v) of laws P i on 'rV[R]_N, each centered with second-moment matrix Sig i, with E_i <z, theta>^4 <= A |theta|^4 and Var_i (z T z^T) <= tau^2 |T|_F^2 for T symmetric, is a regular feature (regular_feature of least_squares.v) with covariance Sigma = sum_i w_i Sig i as soon as opnorm Sigma > 0. The law of total variance adds to tau^2 the spread c^2 of the covariances: for T symmetric, E_i z T z^T - E z T z^T = <Sig i - Sigma, T>, so it suffices that sum_i w_i <Sig i - Sigma, T>^2 <= c^2 |T|_F^2 for every symmetric T. By Cauchy-Schwarz for the Frobenius product, c^2 >= sum_i w_i |Sig i - Sigma|_F^2 is enough. No structure of Sig i - Sigma is needed.
- moment4_integrable and its corollaries moment4_int_lin, moment4_int_lin2, moment4_int_quad, moment4_Lfun2_quad: under a law with E <z, theta>^4 <= A |theta|^4 for every theta, a measurable g with |g z| <= a + b |z|^4 is integrable, so the polynomials of degree at most 4 in the coordinates are (as reg_integrable of feature_moments.v for a regular feature);
- quad_expectation: E z T z^T = <Sig^T, T> for a law with second-moment matrix Sig, that is E <z, theta> <z, theta'> = theta Sig theta'^T;
- mixture_regular_feature_dot: the mixture is a regular feature with covariance Sigma, any K with A <= K^4 opnorm Sigma^2, and sqrt (tau^2 + c^2) in place of tau, when sum_i w_i <Sig i - Sigma, T>^2 <= c^2 |T|_F^2 for every symmetric T;
- mixture_regular_feature: the same when sum_i w_i |Sig i - Sigma|_F^2 <= c^2.
Main results
| Results | Statement |
|---|---|
Under a law on 'rV[R]_N with E <z, theta>^4 <= A |theta|^4 for every theta, a measurable g with |g z| <= a + b |z|^4 for every z (a bound on the absolute value) is integrable, so the linear forms, their products and the quadratic forms z T z^T are integrable and z T z^T is square integrable; if moreover E <z, theta> <z, theta'> = theta Sig theta'^T, then E z T z^T = <Sig^T, T>. | |
A finite mixture of laws P i on 'rV[R]_N, each centered with second-moment matrix Sig i, E_i <z, theta>^4 <= A |theta|^4 and Var_i (z T z^T) <= tau^2 |T|_F^2 for T symmetric, is a regular feature with covariance Sigma = sum_i w_i Sig i, any K with A <= K^4 opnorm Sigma^2, and sqrt (tau^2 + c^2) in place of tau, when opnorm Sigma > 0 and sum_i w_i <Sig i - Sigma, T>^2 <= c^2 |T|_F^2 for every symmetric T (the law of total variance, with E_i z T z^T - E z T z^T = <Sig i - Sigma, T> for T symmetric). | |
The same when opnorm Sigma > 0 and sum_i w_i |Sig i - Sigma|_F^2 <= c^2, which implies the hypothesis of mixture_regular_feature_dot by Cauchy-Schwarz for the Frobenius product; no structure of Sig i - Sigma is needed. |
Declarations12 exported, 2 local
Context {R : realType} {N : nat}. Variables (A : R) (mu : probability 'rV[R]_N R). Hypothesis h4 : forall th : 'rV[R]_N, ('E_mu[fun z => (mxdot z th ^+ 4)%R] <= (A * mxdot th th ^+ 2)%:E)%E.
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> forall th : 'rV_N, mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => mxdot z th ^+ 4))
Statement as written in the source
Lemma moment4_int4 (th : 'rV[R]_N) : mu.-integrable setT (EFin \o (fun z => mxdot z th ^+ 4)).
Used by 1 declaration in 1 file
- this file: moment4_int_norm4
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => mxdot z z ^+ 2))
Statement as written in the source
Lemma moment4_int_norm4 : mu.-integrable setT (EFin \o (fun z => mxdot z z ^+ 2)).
Used by 1 declaration in 1 file
- this file: moment4_integrable
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> forall [g : 'rV_N -> R] [a b : R], measurable_fun [set: 'rV_N] g -> (forall z : 'rV_N, `|g z| <= a + b * mxdot z z ^+ 2) -> mu.-integrable [set: 'rV_N] (EFin \o g)
Domination of |g| by a + b |z|^4.
Under a law on 'rV[R]_N with E <z, theta>^4 <= A |theta|^4 for every theta, a measurable g with |g z| <= a + b |z|^4 for every z (a bound on the absolute value) is integrable, so the linear forms, their products and the quadratic forms z T z^T are integrable and z T z^T is square integrable; if moreover E <z, theta> <z, theta'> = theta Sig theta'^T, then E z T z^T = <Sig^T, T>.
Statement as written in the source
Lemma moment4_integrable (g : 'rV[R]_N -> R) (a b : R) : measurable_fun setT g -> (forall z, `|g z| <= a + b * mxdot z z ^+ 2) -> mu.-integrable setT (EFin \o g).
Used by 4 declarations in 1 file
- this file: moment4_int_lin, moment4_int_lin2, moment4_int_quad, moment4_Lfun2_quad
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> forall th : 'rV_N, mu.-integrable [set: 'rV_N] (EFin \o (mxdot (n:=N))^~ th)
Stated in the README together with moment4_integrable.
Statement as written in the source
Lemma moment4_int_lin (th : 'rV[R]_N) : mu.-integrable setT (EFin \o (fun z => mxdot z th)).
Used by 1 declaration in 1 file
- this file: moment4_Lfun1_lin
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> forall th th' : 'rV_N, mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => mxdot z th * mxdot z th'))
Stated in the README together with moment4_integrable.
Statement as written in the source
Used by 2 declarations in 1 file
- this file: moment4_Lfun1_lin2, quad_expectation
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> forall T : 'M_N, mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => mxdot z (z *m T)))
Stated in the README together with moment4_integrable.
Statement as written in the source
Lemma moment4_int_quad (T : 'M[R]_N) : mu.-integrable setT (EFin \o (fun z => mxdot z (z *m T))).
Used by 2 declarations in 1 file
- this file: quad_expectation, mixture_regular_feature_dot
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> forall T : 'M_N, (fun z : 'rV_N => mxdot z (z *m T)) \in Lfun mu 2
Stated in the README together with moment4_integrable.
Statement as written in the source
Lemma moment4_Lfun2_quad (T : 'M[R]_N) : (fun z => mxdot z (z *m T)) \in Lfun mu 2%:E.
Used by 1 declaration in 1 file
- this file: mixture_regular_feature_dot
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> forall th : 'rV_N, (mxdot (n:=N))^~ th \in Lfun mu 1
Statement as written in the source
Lemma moment4_Lfun1_lin (th : 'rV[R]_N) : (fun z => mxdot z th) \in Lfun mu 1.
Used by 1 declaration in 1 file
- this file: mixture_regular_feature_dot
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> forall th th' : 'rV_N, (fun z : 'rV_N => mxdot z th * mxdot z th') \in Lfun mu 1
Statement as written in the source
Used by 1 declaration in 1 file
- this file: mixture_regular_feature_dot
Context {R : realType} {N : nat}. Variables (A : R) (mu : probability 'rV[R]_N R) (Sig : 'M[R]_N). Hypothesis h4 : forall th : 'rV[R]_N, ('E_mu[fun z => (mxdot z th ^+ 4)%R] <= (A * mxdot th th ^+ 2)%:E)%E. Hypothesis h2 : forall th th' : 'rV[R]_N, ('E_mu[fun z => (mxdot z th * mxdot z th')%R] = (mxdot (th *m Sig) th')%:E)%E.
forall {R : realType} {N : nat} [A : R] [mu : probability 'rV_N R] [Sig : 'M_N], (forall th : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> (forall th th' : 'rV_N, ('E_mu[(fun z : 'rV_N => (mxdot z th * mxdot z th')%R)])%E = (mxdot (th *m Sig) th')%:E) -> forall T : 'M_N, ('E_mu[(fun z : 'rV_N => mxdot z (z *m T))])%E = (mxdot Sig^T T)%:E
E z T z^T = sum_(a, b) Sig_(b, a) T_(a, b).
Stated in the README together with moment4_integrable.
Statement as written in the source
Used by 1 declaration in 1 file
- this file: mixture_regular_feature_dot
Context {R : realType} {N : nat} (I : finType). Variables (w : I -> R) (P : I -> probability 'rV[R]_N R). Variable hw : mixture_weights w. Variables (Sig : I -> 'M[R]_N) (Sigma : 'M[R]_N) (A tau c K : R). Hypothesis P2 : forall i (th th' : 'rV[R]_N), ('E_(P i)[fun z => (mxdot z th * mxdot z th')%R] = (mxdot (th *m Sig i) th')%:E)%E. Hypothesis P1 : forall i (th : 'rV[R]_N), ('E_(P i)[fun z => mxdot z th] = 0)%E. Hypothesis P4 : forall i (th : 'rV[R]_N), ('E_(P i)[fun z => (mxdot z th ^+ 4)%R] <= (A * mxdot th th ^+ 2)%:E)%E. Hypothesis PV : forall i (T : 'M[R]_N), T \is symmetricmx -> ('V_(P i)[fun z => mxdot z (z *m T)] <= (tau ^+ 2 * frobenius T ^+ 2)%:E)%E. Hypothesis SigmaE : Sigma = \sum_i w i *: Sig i. Local Notation mu := (mixture P hw).
Let w0 i : 0 <= w i := mixture_weights_ge0 hw i.
Used by 1 declaration in 1 file
- this file: mixture_regular_feature
Let sum_w : \sum_i w i = 1 := mixture_weights_sum hw.
Used by 1 declaration in 1 file
- this file: mixture_regular_feature_dot
forall {R : realType} {N : nat} [I : finType] [w : I -> R] [P : I -> probability 'rV_N R] (hw : mixture_weights w) [Sig : I -> 'M_N] [Sigma : 'M_N] [A tau c K : R], (forall (i : I) (th th' : 'rV_N), ('E_(P i)[(fun z : 'rV_N => (mxdot z th * mxdot z th')%R)])%E = (mxdot (th *m Sig i) th')%:E) -> (forall (i : I) (th : 'rV_N), ('E_(P i)[((mxdot (n:=N))^~ th)])%E = 0) -> (forall (i : I) (th : 'rV_N), ('E_(P i)[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> (forall (i : I) (T : 'M_N), T \is symmetricmx -> ('V_(P i)[(fun z : 'rV_N => mxdot z (z *m T))] <= (tau ^+ 2 * frobenius T ^+ 2)%:E)%E) -> Sigma = \sum_i w i *: Sig i -> 0 < opnorm Sigma -> (forall T : 'M_N, T \is symmetricmx -> \sum_i w i * mxdot (Sig i - Sigma) T ^+ 2 <= c ^+ 2 * frobenius T ^+ 2) -> A <= K ^+ 4 * opnorm Sigma ^+ 2 -> regular_feature K (Num.ExtraDef.sqrtr (tau ^+ 2 + c ^+ 2)) Sigma (mixture P hw)
A finite mixture of laws P i on 'rV[R]_N, each centered with second-moment matrix Sig i, E_i <z, theta>^4 <= A |theta|^4 and Var_i (z T z^T) <= tau^2 |T|_F^2 for T symmetric, is a regular feature with covariance Sigma = sum_i w_i Sig i, any K with A <= K^4 opnorm Sigma^2, and sqrt (tau^2 + c^2) in place of tau, when opnorm Sigma > 0 and sum_i w_i <Sig i - Sigma, T>^2 <= c^2 |T|_F^2 for every symmetric T (the law of total variance, with E_i z T z^T - E z T z^T = <Sig i - Sigma, T> for T symmetric).
Statement as written in the source
Theorem mixture_regular_feature_dot : 0 < opnorm Sigma -> (forall T : 'M[R]_N, T \is symmetricmx -> \sum_i w i * mxdot (Sig i - Sigma) T ^+ 2 <= c ^+ 2 * frobenius T ^+ 2) -> A <= K ^+ 4 * opnorm Sigma ^+ 2 -> regular_feature K (Num.sqrt (tau ^+ 2 + c ^+ 2)) Sigma mu.
Used by 1 declaration in 1 file
- this file: mixture_regular_feature
forall {R : realType} {N : nat} [I : finType] [w : I -> R] [P : I -> probability 'rV_N R] (hw : mixture_weights w) [Sig : I -> 'M_N] [Sigma : 'M_N] [A tau c K : R], (forall (i : I) (th th' : 'rV_N), ('E_(P i)[(fun z : 'rV_N => (mxdot z th * mxdot z th')%R)])%E = (mxdot (th *m Sig i) th')%:E) -> (forall (i : I) (th : 'rV_N), ('E_(P i)[((mxdot (n:=N))^~ th)])%E = 0) -> (forall (i : I) (th : 'rV_N), ('E_(P i)[(fun z : 'rV_N => (mxdot z th ^+ 4)%R)] <= (A * mxdot th th ^+ 2)%:E)%E) -> (forall (i : I) (T : 'M_N), T \is symmetricmx -> ('V_(P i)[(fun z : 'rV_N => mxdot z (z *m T))] <= (tau ^+ 2 * frobenius T ^+ 2)%:E)%E) -> Sigma = \sum_i w i *: Sig i -> 0 < opnorm Sigma -> \sum_i w i * frobenius (Sig i - Sigma) ^+ 2 <= c ^+ 2 -> A <= K ^+ 4 * opnorm Sigma ^+ 2 -> regular_feature K (Num.ExtraDef.sqrtr (tau ^+ 2 + c ^+ 2)) Sigma (mixture P hw)
The hypothesis on the spread of the covariances of mixture_regular_feature_dot follows from a bound on sum_i w_i |Sig i - Sigma|_F^2, by Cauchy-Schwarz for the Frobenius product.
The same when opnorm Sigma > 0 and sum_i w_i |Sig i - Sigma|_F^2 <= c^2, which implies the hypothesis of mixture_regular_feature_dot by Cauchy-Schwarz for the Frobenius product; no structure of Sig i - Sigma is needed.
Statement as written in the source
Theorem mixture_regular_feature : 0 < opnorm Sigma -> \sum_i w i * frobenius (Sig i - Sigma) ^+ 2 <= c ^+ 2 -> A <= K ^+ 4 * opnorm Sigma ^+ 2 -> regular_feature K (Num.sqrt (tau ^+ 2 + c ^+ 2)) Sigma mu.