On this page

Uniform means on finite types

GaussianAnalysis.probability.finite_meanlibrary/probability/finite_mean.v313 lines32 lemmas and theorems, 2 definitionssource

Imports 0 library modules and 6 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic

Imported by 5

For a finite type T and f : T -> R, unif_mean f = #|T|^-1 \sum_x f x is the mean of f under the uniform law of T, and unif_var f = unif_mean (f - unif_mean f)^2 its variance; R is a realFieldType. A tuple of m independent uniform coordinates is a uniform element of m.-tuple T, so these means express the expectations of functions of independent uniform random elements of finite sets as finite averages, without measure theory.

Linearity, monotonicity and constants (unif_meanD, unif_meanZ, unif_mean_sum, ler_unif_mean, unif_mean_cst), extensionality (eq_unif_mean, eq_unif_var), invariance under bijections (unif_mean_bij, unif_var_bij), and the mean of the indicator of a predicate as the proportion of the elements that satisfy it (unif_mean_indicator).
Fubini: the mean over T1 * T2 is the iterated mean (unif_mean_pair, unif_mean_comm); the mean over m.+1.-tuple T is the mean over the head of the mean over the tail (unif_mean_tuple_cons), and the mean of a product over the coordinates is the product of the means (unif_mean_tuple_prod). The uniform law of T1 + T2 is the mixture of the uniform laws of T1 and T2 with weights #|T1| and #|T2| (unif_mean_sum_type).
The variance: Var f = E f^2 - (E f)^2 (unif_varE), Var f <= E (f - c)^2 for every c (unif_var_le), (E f)^2 <= E f^2 (unif_mean_sqr_le), and the law of total variance for a pair and for the head of a tuple (unif_var_pair, unif_var_tuple_cons).

This file is part of target T7 of phase 12: a Rocq formalization of the finite means of the credited argument of the proposition 'Polynomial concentration' of 'A limiting satisfiability threshold for every fixed clause size' (family 235 of the OpenAI math collection, revision 1581d4cbd, source/sections/concentration.tex), where the expectations over independent uniform data are finite averages; the means of the statement of T7, in its definitions file, unfold to these. It follows the finite means of the Lean development of the collection, in lean/OAI/Probability/RandomSAT:

Lean: uniformMean (FiniteMean.lean, line 17)

Lean: uniformVariance (FiniteMean.lean, line 107)

Lean: uniformVariance_fin_succ (Variance.lean, line 322)

`unif_mean f`	#\|T\|^-1 * \sum_(x : T) f x, the mean of f : T -> R under the uniform law of the finite type T
`unif_var f`	unif_mean (fun x => (f x - unif_mean f) ^+ 2)

Main results

Results	Statement
unif_meanunif_varunif_mean_tuple_consunif_mean_tuple_produnif_var_tuple_consunif_mean_sum_typeunif_mean_indicator	Means and variances under the uniform law of a finite type, as finite averages over a `realFieldType`: linearity, monotonicity, invariance under bijections, the mean of the indicator of a predicate as the proportion of the elements that satisfy it, Fubini for pairs, the mean over `m.+1.-tuple T` as the mean over the head of the mean over the tail, the mean of a product over independent coordinates as the product of the means, the law of `T1 + T2` as a mixture with weights `#\|T1\|` and `#\|T2\|` (the cardinals of `T1` and `T2`), `Var f <= E (f - c)^2`, Jensen `(E f)^2 <= E f^2` and the law of total variance for a pair and for the head of a tuple (nonempty types where needed).

Declarations34 exported

sectionunif_mean

Variable R : realFieldType.

definition unif_mean main result source, line 62

Type

forall [R : realFieldType] [T : finType], (T -> R) -> R

Definition

Definition unif_mean (T : finType) (f : T -> R) : R :=
  (#|T|%:R)^-1 * \sum_(x : T) f x.

Main result, as the README states it

Means and variances under the uniform law of a finite type, as finite averages over a realFieldType: linearity, monotonicity, invariance under bijections, the mean of the indicator of a predicate as the proportion of the elements that satisfy it, Fubini for pairs, the mean over m.+1.-tuple T as the mean over the head of the mean over the tail, the mean of a product over independent coordinates as the product of the means, the law of T1 + T2 as a mixture with weights #|T1| and #|T2| (the cardinals of T1 and T2), Var f <= E (f - c)^2, Jensen (E f)^2 <= E f^2 and the law of total variance for a pair and for the head of a tuple (nonempty types where needed).

Used by 46 declarations in 4 files

this file: unif_var, unif_mean_sumE, eq_unif_mean, unif_mean_cst, unif_meanD, unif_meanN, unif_meanB, unif_meanZ, unif_meanZr, unif_mean_sum, ler_unif_mean, unif_mean_ge0, unif_mean_indicator, unif_mean_le, unif_mean_ge, unif_mean_bij, unif_mean_pair, unif_mean_comm, unif_mean_tuple0, unif_mean_tuple_cons, unif_mean_tuple_prod, unif_mean_sum_type, unif_mean_sqr_dev, unif_varE, unif_var_le, unif_mean_sqr_le, unif_var_pair, unif_var_bij, unif_var_tuple_cons
GaussianApplications.RandomSAT.Model: unif_mean_clause_split
GaussianApplications.RandomSAT.Pivotal: clause_avg, tuple_avg, survival0_set, kill, survival_le_geom, life_mean, second, secondS, life_var_succ_le
GaussianApplications.RandomSAT.Forcing: unif_mean_binom_mean, del_mean, era_mean, del_meanS, head_forced, forced_coord_mean, forced_frac

definition unif_var main result source, line 65

Type

forall [R : realFieldType] [T : finType], (T -> R) -> R

Definition

Definition unif_var (T : finType) (f : T -> R) : R :=
  unif_mean (fun x => (f x - unif_mean f) ^+ 2).

Main result

Stated in the README together with unif_mean.

Used by 12 declarations in 3 files

this file: eq_unif_var, unif_varE, unif_var_le, unif_mean_sqr_le, unif_var_ge0, unif_var_addl, unif_var_pair, unif_var_bij, unif_var_tuple_cons
GaussianApplications.RandomSAT.Pivotal: life_var, life_var_le_occ
GaussianApplications.RandomSAT.Variance: sat_capped_varE

lemma unif_mean_sumE source, line 68

forall [R : realFieldType] [T : finType] (f : T -> R), #|T|%:R * unif_mean f = \sum_x f x

Statement as written in the source

Lemma unif_mean_sumE (T : finType) (f : T -> R) :
  #|T|%:R * unif_mean f = \sum_(x : T) f x.

Used by 1 declaration in 1 file

this file: unif_mean_sum_type

lemma eq_unif_mean source, line 76

forall [R : realFieldType] [T : finType] [f g : T -> R],
f =1 g -> unif_mean f = unif_mean g

Statement as written in the source

Lemma eq_unif_mean (T : finType) (f g : T -> R) :
  f =1 g -> unif_mean f = unif_mean g.

Used by 23 declarations in 4 files

this file: eq_unif_var, unif_meanZr, unif_mean_tuple_prod, unif_mean_sqr_dev, unif_var_addl, unif_var_pair
GaussianApplications.RandomSAT.Pivotal: survival0_set, kill0, killE, life_meanS, life_mean_sum, second0, secondS, second_le_occ
GaussianApplications.RandomSAT.Replacement: killE_forced
GaussianApplications.RandomSAT.Forcing: tuple_avg_add, clause_avg_tuple_avg, del_meanS, era_meanS, del_mean_binom, clause_avg_short_survival, forced_coord_mean, forced_frac_head

lemma eq_unif_var source, line 80

forall [R : realFieldType] [T : finType] [f g : T -> R], f =1 g -> unif_var f = unif_var g

Statement as written in the source

Lemma eq_unif_var (T : finType) (f g : T -> R) :
  f =1 g -> unif_var f = unif_var g.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Variance: sat_capped_varE

lemma unif_mean_cst source, line 87

forall [R : realFieldType] [T : finType] (c : R), (0 < #|T|)%N -> unif_mean (fun=> c) = c

Statement as written in the source

Lemma unif_mean_cst (T : finType) (c : R) : (0 < #|T|)%N ->
  unif_mean (fun _ : T => c) = c.

Used by 18 declarations in 3 files

this file: unif_mean_le, unif_mean_ge, unif_mean_sqr_dev, unif_var_addl
GaussianApplications.RandomSAT.Pivotal: clause_avg_cst, kill0, killE, survival_le_geom, life_meanS, secondS, second_le_occ, life_var_succ_le
GaussianApplications.RandomSAT.Forcing: ler_tuple_avg_cst, survival_antitone, del_meanS, era_meanS, clause_avg_subr, era_mean_replacement

lemma unif_meanD source, line 95

forall [R : realFieldType] [T : finType] (f g : T -> R),
unif_mean (fun x : T => f x + g x) = unif_mean f + unif_mean g

Statement as written in the source

Lemma unif_meanD (T : finType) (f g : T -> R) :
  unif_mean (fun x => f x + g x) = unif_mean f + unif_mean g.

Used by 8 declarations in 3 files

this file: unif_meanB, unif_mean_sqr_dev, unif_var_addl
GaussianApplications.RandomSAT.Pivotal: life_meanS, life_mean_sum, secondS, life_var_succ_le
GaussianApplications.RandomSAT.Forcing: unif_mean_binom_mean

lemma unif_meanN source, line 99

forall [R : realFieldType] [T : finType] (f : T -> R),
unif_mean (fun x : T => - f x) = - unif_mean f

Statement as written in the source

Lemma unif_meanN (T : finType) (f : T -> R) :
  unif_mean (fun x => - f x) = - unif_mean f.

Used by 1 declaration in 1 file

this file: unif_meanB

lemma unif_meanB source, line 103

forall [R : realFieldType] [T : finType] (f g : T -> R),
unif_mean (fun x : T => f x - g x) = unif_mean f - unif_mean g

Statement as written in the source

Lemma unif_meanB (T : finType) (f g : T -> R) :
  unif_mean (fun x => f x - g x) = unif_mean f - unif_mean g.

Used by 8 declarations in 3 files

this file: unif_var_pair
GaussianApplications.RandomSAT.Pivotal: killE, survival_le_geom, life_var_succ_le
GaussianApplications.RandomSAT.Forcing: ler_tuple_avg_cst, clause_avg_subr, era_mean_replacement, head_forced_mean_le

lemma unif_meanZ source, line 107

forall [R : realFieldType] [T : finType] (c : R) (f : T -> R),
unif_mean (fun x : T => c * f x) = c * unif_mean f

Statement as written in the source

Lemma unif_meanZ (T : finType) (c : R) (f : T -> R) :
  unif_mean (fun x => c * f x) = c * unif_mean f.

Used by 8 declarations in 4 files

this file: unif_meanZr, unif_mean_tuple_prod, unif_mean_sqr_dev
GaussianApplications.RandomSAT.Pivotal: secondS, second_le_occ, life_var_le_occ
GaussianApplications.RandomSAT.Forcing: unif_mean_binom_mean
GaussianApplications.RandomSAT.Variance: sat_variance_bound_explicit

lemma unif_meanZr source, line 111

forall [R : realFieldType] [T : finType] (c : R) (f : T -> R),
unif_mean (fun x : T => f x * c) = unif_mean f * c

Statement as written in the source

Lemma unif_meanZr (T : finType) (c : R) (f : T -> R) :
  unif_mean (fun x => f x * c) = unif_mean f * c.

Used by 3 declarations in 3 files

this file: unif_mean_tuple_prod
GaussianApplications.RandomSAT.Pivotal: secondS
GaussianApplications.RandomSAT.Forcing: forced_frac_head

lemma unif_mean_sum source, line 117

forall [R : realFieldType] [T I : finType] (P : pred I) (F : I -> T -> R),
unif_mean (fun x : T => \sum_(i | P i) F i x) = \sum_(i | P i) unif_mean (F i)

Statement as written in the source

Lemma unif_mean_sum (T I : finType) (P : pred I) (F : I -> T -> R) :
  unif_mean (fun x => \sum_(i | P i) F i x) = \sum_(i | P i) unif_mean (F i).

Used by 3 declarations in 2 files

GaussianApplications.RandomSAT.Pivotal: life_mean_sum, occS
GaussianApplications.RandomSAT.Forcing: forced_frac_head

lemma ler_unif_mean source, line 123

forall [R : realFieldType] [T : finType] [f g : T -> R],
(forall x : T, f x <= g x) -> unif_mean f <= unif_mean g

Statement as written in the source

Lemma ler_unif_mean (T : finType) (f g : T -> R) :
  (forall x, f x <= g x) -> unif_mean f <= unif_mean g.

Used by 12 declarations in 4 files

this file: unif_mean_le, unif_mean_ge
GaussianApplications.RandomSAT.Pivotal: ler_clause_avg, ler_tuple_avg, survival_mono, survival_le_geom, second_le_occ, life_var_succ_le, life_var_le_occ
GaussianApplications.RandomSAT.Forcing: survival_antitone, head_forced_mean_le
GaussianApplications.RandomSAT.Variance: sat_variance_bound_explicit

lemma unif_mean_ge0 source, line 130

forall [R : realFieldType] [T : finType] [f : T -> R],
(forall x : T, 0 <= f x) -> 0 <= unif_mean f

Statement as written in the source

Lemma unif_mean_ge0 (T : finType) (f : T -> R) :
  (forall x, 0 <= f x) -> 0 <= unif_mean f.

Used by 8 declarations in 3 files

this file: unif_mean_sqr_le, unif_var_ge0
GaussianApplications.RandomSAT.Pivotal: survival_ge0, kill_ge0, life_mean_ge0, second_ge0, occ_ge0
GaussianApplications.RandomSAT.Variance: sat_variance_bound_explicit

lemma unif_mean_indicator main result source, line 139

forall (R : realFieldType) [T : finType] (P : pred T),
unif_mean (fun x : T => (P x)%:R) = #|[set x | P x]|%:R / #|T|%:R

The mean of an indicator is the proportion of the elements where it holds.

Main result

Stated in the README together with unif_mean.

Statement as written in the source

Lemma unif_mean_indicator (T : finType) (P : pred T) :
  unif_mean (fun x => (P x)%:R) = #|[set x | P x]|%:R / #|T|%:R.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Replacement: killE_forced

lemma unif_mean_le source, line 147

forall [R : realFieldType] [T : finType] [f : T -> R] [c : R],
(0 < #|T|)%N -> (forall x : T, f x <= c) -> unif_mean f <= c

Statement as written in the source

Lemma unif_mean_le (T : finType) (f : T -> R) (c : R) : (0 < #|T|)%N ->
  (forall x, f x <= c) -> unif_mean f <= c.

Used by 2 declarations in 1 file

GaussianApplications.RandomSAT.Pivotal: survival_le1, kill_le1

lemma unif_mean_ge source, line 153

forall [R : realFieldType] [T : finType] [f : T -> R] [c : R],
(0 < #|T|)%N -> (forall x : T, c <= f x) -> c <= unif_mean f

Statement as written in the source

Lemma unif_mean_ge (T : finType) (f : T -> R) (c : R) : (0 < #|T|)%N ->
  (forall x, c <= f x) -> c <= unif_mean f.

lemma unif_mean_bij source, line 160

forall [R : realFieldType] [T1 T2 : finType] [h : T1 -> T2] (f : T2 -> R),
bijective h -> unif_mean (fun x : T1 => f (h x)) = unif_mean f

The mean is invariant under a bijection.

Statement as written in the source

Lemma unif_mean_bij (T1 T2 : finType) (h : T1 -> T2) (f : T2 -> R) :
  bijective h -> unif_mean (fun x => f (h x)) = unif_mean f.

Used by 5 declarations in 3 files

this file: unif_mean_comm, unif_mean_tuple_cons, unif_var_bij
GaussianApplications.RandomSAT.Model: unif_mean_clause_split
GaussianApplications.RandomSAT.Forcing: forced_coord_mean

lemma unif_mean_pair source, line 168

forall [R : realFieldType] [T1 T2 : finType] (f : T1 * T2 -> R),
unif_mean f = unif_mean (fun x : T1 => unif_mean (fun y : T2 => f (x, y)))

Fubini for the uniform law of a product.

Statement as written in the source

Lemma unif_mean_pair (T1 T2 : finType) (f : T1 * T2 -> R) :
  unif_mean f = unif_mean (fun x => unif_mean (fun y => f (x, y))).

Used by 4 declarations in 2 files

this file: unif_mean_comm, unif_mean_tuple_cons, unif_var_pair
GaussianApplications.RandomSAT.Model: unif_mean_clause_split

lemma unif_mean_comm source, line 176

forall [R : realFieldType] [T1 T2 : finType] (f : T1 -> T2 -> R),
unif_mean (fun x : T1 => unif_mean [eta f x]) = unif_mean (fun y : T2 => unif_mean (f^~ y))

Statement as written in the source

Lemma unif_mean_comm (T1 T2 : finType) (f : T1 -> T2 -> R) :
  unif_mean (fun x => unif_mean (fun y => f x y)) =
  unif_mean (fun y => unif_mean (fun x => f x y)).

Used by 2 declarations in 2 files

GaussianApplications.RandomSAT.Pivotal: secondS
GaussianApplications.RandomSAT.Forcing: clause_avg_tuple_avg

lemma bij_tuple_cons source, line 187

forall (T : Type) (m : nat), bijective (fun p : T * m.-tuple T => [tuple of p.1 :: p.2])

Statement as written in the source

Lemma bij_tuple_cons (T : Type) m :
  bijective (fun p : T * m.-tuple T => [tuple of p.1 :: p.2]).

Used by 2 declarations in 1 file

this file: unif_mean_tuple_cons, unif_var_tuple_cons

lemma unif_mean_tuple0 source, line 197

forall [R : realFieldType] [T : finType] (f : 0.-tuple T -> R), unif_mean f = f [tuple]

The coordinates of a uniform tuple: the head and the tail are independent and uniform.

Statement as written in the source

Lemma unif_mean_tuple0 (T : finType) (f : 0.-tuple T -> R) :
  unif_mean f = f [tuple].

Used by 8 declarations in 3 files

this file: unif_mean_tuple_prod
GaussianApplications.RandomSAT.Pivotal: tuple_avg0, life_mean_sum, second0, second_le_occ, life_var_le_occ
GaussianApplications.RandomSAT.Forcing: del_mean0, era_mean0

lemma unif_mean_tuple_cons main result source, line 204

forall [R : realFieldType] [T : finType] [m : nat] (f : (m.+1).-tuple T -> R),
unif_mean f =
unif_mean (fun x : T => unif_mean (fun t : m.-tuple T => f [tuple of x :: t]))

Main result

Stated in the README together with unif_mean.

Statement as written in the source

Lemma unif_mean_tuple_cons (T : finType) m (f : m.+1.-tuple T -> R) :
  unif_mean f =
  unif_mean (fun x => unif_mean (fun t : m.-tuple T => f [tuple of x :: t])).

Used by 6 declarations in 3 files

this file: unif_mean_tuple_prod
GaussianApplications.RandomSAT.Pivotal: tuple_avgS, life_meanS, secondS
GaussianApplications.RandomSAT.Forcing: del_meanS, era_meanS

lemma unif_mean_tuple_prod main result source, line 214

forall [R : realFieldType] [T : finType] (m : nat) (g : T -> R),
unif_mean (fun t : m.-tuple T => \prod_(x <- t) g x) = unif_mean g ^+ m

Independent coordinates: the mean of a product over the coordinates of a uniform tuple is the product of the means.

Main result

Stated in the README together with unif_mean.

Statement as written in the source

Lemma unif_mean_tuple_prod (T : finType) m (g : T -> R) :
  unif_mean (fun t : m.-tuple T => \prod_(x <- t) g x) = unif_mean g ^+ m.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Pivotal: survival_le_geom

lemma unif_mean_sum_type main result source, line 225

forall [R : realFieldType] [T1 T2 : finType] (f : T1 + T2 -> R),
unif_mean f =
#|T1|%:R / (#|T1| + #|T2|)%:R * unif_mean (fun x : T1 => f (inl x)) +
#|T2|%:R / (#|T1| + #|T2|)%:R * unif_mean (fun y : T2 => f (inr y))

The uniform law of a sum type is a mixture of the uniform laws of its summands.

Main result

Stated in the README together with unif_mean.

Statement as written in the source

Lemma unif_mean_sum_type (T1 T2 : finType) (f : T1 + T2 -> R) :
  unif_mean f =
  #|T1|%:R / (#|T1| + #|T2|)%:R * unif_mean (fun x => f (inl x)) +
  #|T2|%:R / (#|T1| + #|T2|)%:R * unif_mean (fun y => f (inr y)).

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Model: unif_mean_clause_split

lemma unif_mean_sqr_dev source, line 237

forall [R : realFieldType] [T : finType] (f : T -> R) (c : R),
(0 < #|T|)%N ->
unif_mean (fun x : T => (f x - c) ^+ 2) =
unif_mean (fun x : T => f x ^+ 2) - 2 * c * unif_mean f + c ^+ 2

The variance: E f^2 - (E f)^2, at most E (f - c)^2, and Jensen.

Statement as written in the source

Lemma unif_mean_sqr_dev (T : finType) (f : T -> R) (c : R) : (0 < #|T|)%N ->
  unif_mean (fun x => (f x - c) ^+ 2) =
  unif_mean (fun x => f x ^+ 2) - 2 * c * unif_mean f + c ^+ 2.

Used by 2 declarations in 1 file

this file: unif_varE, unif_var_le

lemma unif_varE source, line 246

forall [R : realFieldType] [T : finType] (f : T -> R),
(0 < #|T|)%N -> unif_var f = unif_mean (fun x : T => f x ^+ 2) - unif_mean f ^+ 2

Statement as written in the source

Lemma unif_varE (T : finType) (f : T -> R) : (0 < #|T|)%N ->
  unif_var f = unif_mean (fun x => f x ^+ 2) - unif_mean f ^+ 2.

Used by 3 declarations in 1 file

this file: unif_var_le, unif_mean_sqr_le, unif_var_pair

lemma unif_var_le source, line 250

forall [R : realFieldType] [T : finType] (f : T -> R) (c : R),
(0 < #|T|)%N -> unif_var f <= unif_mean (fun x : T => (f x - c) ^+ 2)

Statement as written in the source

Lemma unif_var_le (T : finType) (f : T -> R) (c : R) : (0 < #|T|)%N ->
  unif_var f <= unif_mean (fun x => (f x - c) ^+ 2).

Used by 2 declarations in 2 files

this file: unif_mean_sqr_le
GaussianApplications.RandomSAT.Pivotal: life_var_succ_le

lemma unif_mean_sqr_le source, line 257

forall [R : realFieldType] [T : finType] (f : T -> R),
unif_mean f ^+ 2 <= unif_mean (fun x : T => f x ^+ 2)

Statement as written in the source

Lemma unif_mean_sqr_le (T : finType) (f : T -> R) :
  unif_mean f ^+ 2 <= unif_mean (fun x => f x ^+ 2).

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Pivotal: life_var_succ_le

lemma unif_var_ge0 source, line 270

forall [R : realFieldType] [T : finType] (f : T -> R), 0 <= unif_var f

Statement as written in the source

Lemma unif_var_ge0 (T : finType) (f : T -> R) : 0 <= unif_var f.

lemma unif_var_addl source, line 273

forall [R : realFieldType] [T : finType] (c : R) (f : T -> R),
(0 < #|T|)%N -> unif_var (fun x : T => c + f x) = unif_var f

Statement as written in the source

Lemma unif_var_addl (T : finType) (c : R) (f : T -> R) : (0 < #|T|)%N ->
  unif_var (fun x => c + f x) = unif_var f.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Pivotal: life_var_succ_le

lemma unif_var_pair source, line 281

forall [R : realFieldType] [T1 T2 : finType] (f : T1 -> T2 -> R),
(0 < #|T1|)%N ->
(0 < #|T2|)%N ->
unif_var (fun p : T1 * T2 => f p.1 p.2) =
unif_mean (fun x : T1 => unif_var (f x)) + unif_var (fun x : T1 => unif_mean (f x))

The law of total variance, for a pair and for the head of a tuple.

Statement as written in the source

Lemma unif_var_pair (T1 T2 : finType) (f : T1 -> T2 -> R) :
  (0 < #|T1|)%N -> (0 < #|T2|)%N ->
  unif_var (fun p : T1 * T2 => f p.1 p.2) =
  unif_mean (fun x => unif_var (f x)) + unif_var (fun x => unif_mean (f x)).

Used by 1 declaration in 1 file

this file: unif_var_tuple_cons

lemma unif_var_bij source, line 294

forall [R : realFieldType] [T1 T2 : finType] [h : T1 -> T2] (f : T2 -> R),
bijective h -> unif_var (fun x : T1 => f (h x)) = unif_var f

Statement as written in the source

Lemma unif_var_bij (T1 T2 : finType) (h : T1 -> T2) (f : T2 -> R) :
  bijective h -> unif_var (fun x => f (h x)) = unif_var f.

Used by 1 declaration in 1 file

this file: unif_var_tuple_cons

lemma unif_var_tuple_cons main result source, line 301

forall [R : realFieldType] [T : finType] [m : nat] (f : (m.+1).-tuple T -> R),
(0 < #|T|)%N ->
unif_var f =
unif_mean (fun x : T => unif_var (fun t : m.-tuple T => f [tuple of x :: t])) +
unif_var (fun x : T => unif_mean (fun t : m.-tuple T => f [tuple of x :: t]))

Main result

Stated in the README together with unif_mean.

Statement as written in the source

Lemma unif_var_tuple_cons (T : finType) m (f : m.+1.-tuple T -> R) :
  (0 < #|T|)%N ->
  unif_var f =
  unif_mean (fun x => unif_var (fun t : m.-tuple T => f [tuple of x :: t])) +
  unif_var (fun x => unif_mean (fun t : m.-tuple T => f [tuple of x :: t])).

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Pivotal: life_var_succ_le

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.