On this page

GaussianAnalysisprobabilitytotal_variation

The total variation distance

GaussianAnalysis.probability.total_variationlibrary/probability/total_variation.v264 lines18 lemmas and theorems, 1 definitionsource

Imports 1 library modules and 22 external

GaussianAnalysis.probability.lindeberg

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

Required by 2 files of the paper proofs

The total variation distance of two probabilities on a measurable type is the supremum of |P A - Q A| over the measurable sets A. It is a real number in [0, 1], since probabilities are finite.

tv_dist P Q sup {|P A - Q A| : A measurable}, a real number

Main results:

tv_dist_ge, tv_dist_geE, tv_dist_le: |P A - Q A| <= tv_dist P Q for every measurable A (as reals and as extended reals), and tv_dist P Q is the least such bound; tv_distE: as an extended real it is the ereal_sup of the |P A - Q A|;
tv_dist_ge0, tv_dist_le1, tv_distC, tv_dist_triangle, tv_dist_eq0, tv_distxx: a pseudometric with values in [0, 1], zero for laws that agree on the measurable sets;
tuple_prod_tv: for laws mu i and nu i on T and every measurable set A of n-tuples, |tuple_prod mu n A - tuple_prod nu n A| is at most the sum of the tv_dist (mu i) (nu i), i < n (the hybrid argument of lindeberg_replacement with the indicator of A);
one_sub_le_expR, expR_le_one_sub, pow_one_sub_bounds: for 0 <= x < n, exp (- x n / (n - x)) <= (1 - x / n)^n <= exp (- x); pow_one_sub_dist: |(1 - x / n)^n - exp (- x)| <= x^2 / (n - x); pow_one_sub_cvg: (1 - x / n)^n tends to exp (- x) for every x >= 0.

Main results

Results	Statement
tv_disttv_dist_getv_dist_geEtv_dist_letv_distE	The total variation distance of two probabilities `P` and `Q` on a measurable type: `tv_dist P Q = sup {\|P A - Q A\| : A measurable}`, a real number. For every measurable `A`, `\|P A - Q A\| <= tv_dist P Q`, as reals and as extended reals, and `tv_dist P Q` is the least such bound; as an extended real it is the `ereal_sup` of the `\|P A - Q A\|`.
tv_dist_ge0tv_dist_le1tv_distCtv_dist_triangletv_dist_eq0tv_distxx	A pseudometric with values in `[0, 1]`: symmetric, with the triangle inequality, and zero for laws that agree on the measurable sets.
tuple_prod_tv	For laws `mu i` and `nu i` on `T` and every measurable set `A` of `n`-tuples, `\|tuple_prod mu n A - tuple_prod nu n A\| <= sum_(i < n) tv_dist (mu i) (nu i)`: the hybrid argument of `lindeberg_replacement`, with the indicator of `A`.
pow_one_sub_boundspow_one_sub_distpow_one_sub_cvg	For `0 <= x < n`, `exp (- x n / (n - x)) <= (1 - x / n)^n <= exp (- x)` and `\|(1 - x / n)^n - exp (- x)\| <= x^2 / (n - x)`; hence `(1 - x / n)^n` tends to `exp (- x)` for every `x >= 0`.

Declarations19 exported, 2 local

sectiontotal_variation

Context d (T : measurableType d) (R : realType).
Implicit Types P Q S : probability T R.

definition tv_dist main result source, line 53

Type

forall [d : measure_display] [T : measurableType d] [R : realType],
probability T R -> probability T R -> R

Definition

Definition tv_dist P Q : R :=
  sup [set `|fine (P A) - fine (Q A)| | A in measurable].

Main result, as the README states it

The total variation distance of two probabilities P and Q on a measurable type: tv_dist P Q = sup {|P A - Q A| : A measurable}, a real number. For every measurable A, |P A - Q A| <= tv_dist P Q, as reals and as extended reals, and tv_dist P Q is the least such bound; as an extended real it is the ereal_sup of the |P A - Q A|.

Used by 11 declarations in 1 file

this file: tv_dist_ge, tv_dist_geE, tv_dist_le, tv_dist_ge0, tv_dist_le1, tv_distC, tv_dist_triangle, tv_dist_eq0, tv_distxx, tv_distE, tuple_prod_tv

lemma prob_fine_itv source, line 56

forall [d : measure_display] [T : measurableType d] [R : realType] 
  (P : probability T R) [A : set T],
d.-measurable A -> 0 <= fine (P A) <= 1

Statement as written in the source

Lemma prob_fine_itv P (A : set T) : measurable A -> 0 <= fine (P A) <= 1.

Used by 1 declaration in 1 file

this file: prob_fineB_le1

lemma prob_fineB_le1 source, line 64

forall [d : measure_display] [T : measurableType d] [R : realType] 
  (P Q : probability T R) [A : set T],
d.-measurable A -> `|fine (P A) - fine (Q A)| <= 1

Statement as written in the source

Lemma prob_fineB_le1 P Q (A : set T) : measurable A ->
  `|fine (P A) - fine (Q A)| <= 1.

Used by 2 declarations in 1 file

this file: tv_ub, tv_dist_le1

let tv_ub section-local source, line 72

Let tv_ub P Q :
  has_ubound [set `|fine (P A) - fine (Q A)| | A in measurable].

Used by 1 declaration in 1 file

this file: tv_dist_ge

let tv_ne section-local source, line 76

Let tv_ne P Q :
  [set `|fine (P A) - fine (Q A)| | A in measurable] !=set0.

Used by 1 declaration in 1 file

this file: tv_dist_le

lemma tv_dist_ge main result source, line 80

forall [d : measure_display] [T : measurableType d] [R : realType] 
  (P Q : probability T R) [A : set T],
d.-measurable A -> `|fine (P A) - fine (Q A)| <= tv_dist P Q

Main result

Stated in the README together with tv_dist.

Statement as written in the source

Lemma tv_dist_ge P Q (A : set T) : measurable A ->
  `|fine (P A) - fine (Q A)| <= tv_dist P Q.

Used by 5 declarations in 1 file

this file: tv_dist_geE, tv_dist_ge0, tv_distC, tv_dist_triangle, tuple_prod_tv

lemma tv_dist_geE main result source, line 84

forall [d : measure_display] [T : measurableType d] [R : realType] 
  (P Q : probability T R) [A : set T],
d.-measurable A -> (`|P A - Q A| <= (tv_dist P Q)%:E)%E

Main result

Stated in the README together with tv_dist.

Statement as written in the source

Lemma tv_dist_geE P Q (A : set T) : measurable A ->
  (`|P A - Q A| <= (tv_dist P Q)%:E)%E.

lemma tv_dist_le main result source, line 93

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P Q : probability T R] [c : R],
(forall A : set T, d.-measurable A -> `|fine (P A) - fine (Q A)| <= c) -> tv_dist P Q <= c

Main result

Stated in the README together with tv_dist.

Statement as written in the source

Lemma tv_dist_le P Q (c : R) :
  (forall A, measurable A -> `|fine (P A) - fine (Q A)| <= c) ->
  tv_dist P Q <= c.

Used by 4 declarations in 1 file

this file: tv_dist_le1, tv_distC, tv_dist_triangle, tv_dist_eq0

lemma tv_dist_ge0 main result source, line 98

forall [d : measure_display] [T : measurableType d] [R : realType] (P Q : probability T R),
0 <= tv_dist P Q

Main result, as the README states it

A pseudometric with values in [0, 1]: symmetric, with the triangle inequality, and zero for laws that agree on the measurable sets.

Statement as written in the source

Lemma tv_dist_ge0 P Q : 0 <= tv_dist P Q.

Used by 1 declaration in 1 file

this file: tv_dist_eq0

lemma tv_dist_le1 main result source, line 101

forall [d : measure_display] [T : measurableType d] [R : realType] (P Q : probability T R),
tv_dist P Q <= 1

Main result

Stated in the README together with tv_dist_ge0.

Statement as written in the source

Lemma tv_dist_le1 P Q : tv_dist P Q <= 1.

lemma tv_distC main result source, line 104

forall [d : measure_display] [T : measurableType d] [R : realType] (P Q : probability T R),
tv_dist P Q = tv_dist Q P

Main result

Stated in the README together with tv_dist_ge0.

Statement as written in the source

Lemma tv_distC P Q : tv_dist P Q = tv_dist Q P.

lemma tv_dist_triangle main result source, line 110

forall [d : measure_display] [T : measurableType d] [R : realType]
  (P Q S : probability T R),
tv_dist P S <= tv_dist P Q + tv_dist Q S

Main result

Stated in the README together with tv_dist_ge0.

Statement as written in the source

Lemma tv_dist_triangle P Q S : tv_dist P S <= tv_dist P Q + tv_dist Q S.

lemma tv_dist_eq0 main result source, line 117

forall [d : measure_display] [T : measurableType d] [R : realType] [P Q : probability T R],
(forall A : set T, d.-measurable A -> P A = Q A) -> tv_dist P Q = 0

Main result

Stated in the README together with tv_dist_ge0.

Statement as written in the source

Lemma tv_dist_eq0 P Q : (forall A, measurable A -> P A = Q A) ->
  tv_dist P Q = 0.

Used by 1 declaration in 1 file

this file: tv_distxx

lemma tv_distxx main result source, line 124

forall [d : measure_display] [T : measurableType d] [R : realType] (P : probability T R),
tv_dist P P = 0

Main result

Stated in the README together with tv_dist_ge0.

Statement as written in the source

Lemma tv_distxx P : tv_dist P P = 0.

lemma tv_distE main result source, line 127

forall [d : measure_display] [T : measurableType d] [R : realType] (P Q : probability T R),
(tv_dist P Q)%:E = ereal_sup [set `|P A - Q A|%E | A in d.-measurable]

Main result

Stated in the README together with tv_dist.

Statement as written in the source

Lemma tv_distE P Q :
  (tv_dist P Q)%:E = ereal_sup [set (`|P A - Q A|)%E | A in measurable].

The product bound: replace the coordinates one at a time.

sectionproduct_bound

Context d (T : measurableType d) (R : realType).

theorem tuple_prod_tv main result source, line 150

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu nu : nat -> probability T R) [n : nat] [A : set (n.-tuple T)],
(measure_tuple_display d).-measurable A ->
(`|tuple_prod mu n A - tuple_prod nu n A| <= (\sum_(i < n) tv_dist (mu i) (nu i))%:E)%E

Main result, as the README states it

For laws mu i and nu i on T and every measurable set A of n-tuples, |tuple_prod mu n A - tuple_prod nu n A| <= sum_(i < n) tv_dist (mu i) (nu i): the hybrid argument of lindeberg_replacement, with the indicator of A.

Statement as written in the source

Theorem tuple_prod_tv (mu nu : nat -> probability T R) n
    (A : set (n.-tuple T)) : measurable A ->
  (`|tuple_prod mu n A - tuple_prod nu n A| <=
    (\sum_(i < n) tv_dist (mu i) (nu i))%:E)%E.

(1 - x / n)^n tends to exp (- x).

sectionexp_limit

Variable R : realType.

lemma one_sub_le_expR source, line 188

forall [R : realType] (y : R), 1 - y <= expR (- y)

Statement as written in the source

Lemma one_sub_le_expR (y : R) : 1 - y <= expR (- y).

Used by 2 declarations in 1 file

this file: pow_one_sub_bounds, pow_one_sub_dist

lemma expR_le_one_sub source, line 191

forall [R : realType] [y : R], 0 <= y < 1 -> expR (- (y / (1 - y))) <= 1 - y

Statement as written in the source

Lemma expR_le_one_sub (y : R) : 0 <= y < 1 ->
  expR (- (y / (1 - y))) <= 1 - y.

Used by 1 declaration in 1 file

this file: pow_one_sub_bounds

lemma pow_one_sub_bounds main result source, line 202

forall [R : realType] [x : R] [n : nat],
0 <= x -> x < n%:R -> expR (- (x * n%:R / (n%:R - x))) <= (1 - x / n%:R) ^+ n <= expR (- x)

Main result, as the README states it

For 0 <= x < n, exp (- x n / (n - x)) <= (1 - x / n)^n <= exp (- x) and |(1 - x / n)^n - exp (- x)| <= x^2 / (n - x); hence (1 - x / n)^n tends to exp (- x) for every x >= 0.

Statement as written in the source

Lemma pow_one_sub_bounds (x : R) n : 0 <= x -> x < n%:R ->
  expR (- (x * n%:R / (n%:R - x))) <= (1 - x / n%:R) ^+ n <= expR (- x).

Used by 1 declaration in 1 file

this file: pow_one_sub_dist

lemma pow_one_sub_dist main result source, line 225

forall [R : realType] [x : R] [n : nat],
0 <= x -> x < n%:R -> `|(1 - x / n%:R) ^+ n - expR (- x)| <= x ^+ 2 / (n%:R - x)

Main result

Stated in the README together with pow_one_sub_bounds.

Statement as written in the source

Lemma pow_one_sub_dist (x : R) n : 0 <= x -> x < n%:R ->
  `|(1 - x / n%:R) ^+ n - expR (- x)| <= x ^+ 2 / (n%:R - x).

Used by 1 declaration in 1 file

this file: pow_one_sub_cvg

lemma pow_one_sub_cvg main result source, line 245

forall [R : realType] [x : R], 0 <= x -> (1 - x / n%:R) ^+ n @[n --> \oo] --> expR (- x)

Main result

Stated in the README together with pow_one_sub_bounds.

Statement as written in the source

Lemma pow_one_sub_cvg (x : R) : 0 <= x ->
  (fun n : nat => (1 - x / n%:R) ^+ n) @ \oo --> expR (- x).

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.