On this page

Laws given by a density

GaussianAnalysis.probability.density_lawlibrary/probability/density_law.v426 lines20 lemmas and theorems, 3 definitionssource

Imports 3 library modules and 20 external

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.classical.cardinality, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, 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.charge, mathcomp.analysis.probability_theory.probability

Required by 6 files of the paper proofs

For a probability mu on a measurable type T and a measurable f : T -> R, nonnegative everywhere, of integral one against mu, density_prob mu f is the probability A |-> int_A f dmu. Its measure is the integral of a nonnegative function, sigma-additive by semi_sigma_additive_nng_induced of MathComp-Analysis. When f is not such a density, density_prob mu f is mu itself (density_prob_default), so that density_prob mu f is a probability for every f; the results below assume prob_density mu f. density_law mu f hf is the same probability, built from a proof hf of prob_density mu f: its value on A is int_A f dmu by definition, with no fallback.

density_probE: density_prob mu f A = int_A f dmu.
density_prob_dominates: density_prob mu f is absolutely continuous with respect to mu.
ge0_integral_density_prob, integrable_density_prob, integral_density_prob: integrating g against density_prob mu f is integrating g f against mu, for g nonnegative or integrable.
density_prob_ae, eq_density_prob: a density may be changed on a mu-null set: int_A f' dmu = density_prob mu f A for measurable A when f' = f mu-almost everywhere, even if f' is negative somewhere, and two densities equal mu-almost everywhere give the same probability.
prob_density_tuple_prod, tuple_prod_density: if f_k is a density against nu_k for every k < n, the product of the laws density_prob nu_k f_k, k < n, has the density x |-> prod_k f_k (x_k) against tuple_prod nu n. indic_tuple_box: the indicator of a box is the product of the indicators of its sides.
density_lawE: density_law mu f hf A = int_A f dmu. density_law_prob: density_law mu f hf is density_prob mu f. integral_density_law_prob: integrals against the two agree, so every result on density_prob holds for density_law. density_law_dominates, ge0_integral_density_law, integrable_density_law, integral_density_law, eq_density_law and tuple_prod_density_law restate the results above for density_law.

`prob_density mu f`	f is measurable, nonnegative everywhere, and of integral one against mu
`density_prob mu f`	the probability with density f against mu, if prob_density mu f, and mu otherwise
`density_law mu f hf`	the probability with density f against mu, for a proof hf of prob_density mu f

Main results

Results	Statement
prob_densitydensity_probdensity_probEdensity_prob_dominatesdensity_prob_default	For a probability `mu` and a measurable `f >= 0` with `int f dmu = 1` (`prob_density mu f`), `density_prob mu f` is the probability `A \|-> int_A f dmu`, absolutely continuous with respect to `mu`; it is `mu` itself when `f` is not such a density.
ge0_integral_density_probintegrable_density_probintegral_density_probdensity_prob_aeeq_density_prob	Integrating `g` against `density_prob mu f` is integrating `g f` against `mu`, for `g` nonnegative or integrable. A density may be changed on a `mu`-null set, even to negative values: `int_A f' dmu = density_prob mu f A` when `f' = f` `mu`-almost everywhere.
prob_density_tuple_prodtuple_prod_densityindic_tuple_box	If `f_k` is a density against `nu_k` for every `k < n`, the product of the laws `density_prob nu_k f_k` has the density `x \|-> prod_k f_k (x_k)` against `tuple_prod nu n`.
density_lawdensity_lawEdensity_law_probintegral_density_law_prob	The constructor with a proof that `f` is a density: for `hf : prob_density mu f`, `density_law mu f hf` is the probability `A \|-> int_A f dmu`, by definition and with no fallback to `mu`. It is `density_prob mu f`, and integrals against the two agree; `density_law_dominates`, `ge0_integral_density_law`, `integrable_density_law`, `integral_density_law`, `eq_density_law` and `tuple_prod_density_law` restate the three rows above for it.

Declarations27 exported, 13 local

definition prob_density main result source, line 64

Type

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

Definition

Definition prob_density d (T : measurableType d) (R : realType)
    (mu : probability T R) (f : T -> R) : Prop :=
  [/\ measurable_fun [set: T] f, forall x, 0 <= f x &
      (\int[mu]_x (f x)%:E = 1)%E].

Main result, as the README states it

For a probability mu and a measurable f >= 0 with int f dmu = 1 (prob_density mu f), density_prob mu f is the probability A |-> int_A f dmu, absolutely continuous with respect to mu; it is mu itself when f is not such a density.

Used by 8 declarations in 1 file

this file: density_prob, density_prob_default, eq_density_prob, density_law, eq_density_law, prob_density_tuple_prod, tuple_prod_density, tuple_prod_density_law

definition density_prob main result source, line 69

Type

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

Definition

Definition density_prob d (T : measurableType d) (R : realType)
    (mu : probability T R) (f : T -> R) : set T -> \bar R :=
  if pselect (prob_density mu f) then fun A => (\int[mu]_(x in A) (f x)%:E)%E
  else mu.

Main result

Stated in the README together with prob_density.

Used by 20 declarations in 1 file

this file: P0, P_ge0, P_sigma_additive, instance at line 105, P_setT, instance at line 113, density_prob_default, density_probE, density_prob_dominates, RN_density, ge0_integral_density_prob, integrable_density_prob, integral_density_prob, density_prob_ae, eq_density_prob, density_law_prob, integral_density_law_prob, integrable_density_law, tuple_prod_density, tuple_prod_density_law

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".

sectiondensity_prob_measure

Context d (T : measurableType d) (R : realType).
Variables (mu : probability T R) (f : T -> R).
Local Notation P := (density_prob mu f).

let P0 section-local source, line 84

Let P0 : P set0 = 0%E.

Used by 1 declaration in 1 file

this file: instance at line 105

let P_ge0 section-local source, line 90

Let P_ge0 A : (0 <= P A)%E.

Used by 1 declaration in 1 file

this file: instance at line 105

let P_sigma_additive section-local source, line 97

Let P_sigma_additive : semi_sigma_additive P.

Used by 1 declaration in 1 file

this file: instance at line 105

instance instance at line 105 source, line 105

HB.instance Definition _ := isMeasure.Build _ _ _ P P0 P_ge0 P_sigma_additive.

let P_setT section-local source, line 107

Let P_setT : P [set: T] = 1%E.

Used by 1 declaration in 1 file

this file: instance at line 113

instance instance at line 113 source, line 113

HB.instance Definition _ := @Measure_isProbability.Build _ _ R P P_setT.

lemma density_prob_default main result source, line 115

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R],
~ prob_density mu f -> density_prob mu f = mu

Main result

Stated in the README together with prob_density.

Statement as written in the source

Lemma density_prob_default : ~ prob_density mu f -> P = mu.

sectiondensity_prob_integral

Context d (T : measurableType d) (R : realType).
Variables (mu : probability T R) (f : T -> R).
Hypothesis hf : prob_density mu f.
Local Notation P := (density_prob mu f).
Local Open Scope ereal_scope.

let mF section-local source, line 127

Let mF : measurable_fun [set: T] (fun x => (f x)%:E).

Used by 3 declarations in 1 file

this file: density_prob_dominates, RN_density, integrable_density_prob

let F0 section-local source, line 130

Let F0 x : 0 <= (f x)%:E.

Used by 3 declarations in 1 file

this file: density_prob_dominates, integrable_density_prob, integral_density_prob

lemma density_probE main result source, line 133

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R],
prob_density mu f -> forall A : set T, density_prob mu f A = (\int[mu]_(x in A) (f x)%:E)%E

Main result

Stated in the README together with prob_density.

Statement as written in the source

Lemma density_probE A : P A = \int[mu]_(x in A) (f x)%:E.

Used by 7 declarations in 1 file

this file: density_prob_dominates, RN_density, density_prob_ae, eq_density_prob, density_law_prob, integral_density_law_prob, tuple_prod_density

lemma density_prob_dominates main result source, line 136

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R],
prob_density mu f -> density_prob mu f `<< mu

Main result

Stated in the README together with prob_density.

Statement as written in the source

Lemma density_prob_dominates : P `<< mu.

Used by 3 declarations in 1 file

this file: RN_density, ge0_integral_density_prob, density_law_dominates

let RN_density section-local source, line 144

Let RN_density : ae_eq mu [set: T] (Radon_Nikodym_SigmaFinite.f P mu)
  (fun x => (f x)%:E).

Used by 1 declaration in 1 file

this file: ge0_integral_density_prob

lemma ge0_integral_density_prob main result source, line 156

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R],
prob_density mu f ->
forall [g : T -> \bar R] [E : set T],
d.-measurable E ->
(forall x : T, (0%R <= g x)%E) ->
measurable_fun E g ->
(\int[density_prob mu f]_(x in E) g x)%E = (\int[mu]_(x in E) (g x * (f x)%:E))%E

Main result, as the README states it

Integrating g against density_prob mu f is integrating g f against mu, for g nonnegative or integrable. A density may be changed on a mu-null set, even to negative values: int_A f' dmu = density_prob mu f A when f' = f mu-almost everywhere.

Statement as written in the source

Lemma ge0_integral_density_prob (g : T -> \bar R) E : measurable E ->
  (forall x, 0 <= g x) -> measurable_fun E g ->
  \int[P]_(x in E) g x = \int[mu]_(x in E) (g x * (f x)%:E).

Used by 3 declarations in 1 file

this file: integrable_density_prob, integral_density_prob, ge0_integral_density_law

lemma integrable_density_prob main result source, line 171

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R],
prob_density mu f ->
forall [g : T -> \bar R] [E : set T],
d.-measurable E ->
measurable_fun E g ->
(density_prob mu f).-integrable E g <-> mu.-integrable E (fun x : T => (g x * (f x)%:E)%E)

Main result

Stated in the README together with ge0_integral_density_prob.

Statement as written in the source

Lemma integrable_density_prob (g : T -> \bar R) E : measurable E ->
  measurable_fun E g ->
  P.-integrable E g <-> mu.-integrable E (fun x => g x * (f x)%:E).

Used by 2 declarations in 1 file

this file: integrable_density_law, integral_density_law

lemma integral_density_prob main result source, line 187

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R],
prob_density mu f ->
forall [g : T -> \bar R] [E : set T],
d.-measurable E ->
(density_prob mu f).-integrable E g ->
(\int[density_prob mu f]_(x in E) g x)%E = (\int[mu]_(x in E) (g x * (f x)%:E))%E

Main result

Stated in the README together with ge0_integral_density_prob.

Statement as written in the source

Lemma integral_density_prob (g : T -> \bar R) E : measurable E ->
  P.-integrable E g ->
  \int[P]_(x in E) g x = \int[mu]_(x in E) (g x * (f x)%:E).

Used by 1 declaration in 1 file

this file: integral_density_law

lemma density_prob_ae main result source, line 203

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R],
prob_density mu f ->
forall [f' : T -> R] [A : set T],
d.-measurable A ->
measurable_fun [set: T] f' ->
ae_eq mu [set: T] (fun x : T => (f x)%:E) (fun x : T => (f' x)%:E) ->
density_prob mu f A = (\int[mu]_(x in A) (f' x)%:E)%E

The density may be changed on a mu-null set, even to negative values.

Main result

Stated in the README together with ge0_integral_density_prob.

Statement as written in the source

Lemma density_prob_ae (f' : T -> R) A : measurable A ->
  measurable_fun [set: T] f' ->
  ae_eq mu [set: T] (fun x => (f x)%:E) (fun x => (f' x)%:E) ->
  P A = \int[mu]_(x in A) (f' x)%:E.

Used by 1 declaration in 1 file

this file: eq_density_prob

lemma eq_density_prob main result source, line 217

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f f' : T -> R],
prob_density mu f ->
prob_density mu f' ->
ae_eq mu [set: T] (fun x : T => (f x)%:E) (fun x : T => (f' x)%:E) ->
forall [A : set T], d.-measurable A -> density_prob mu f A = density_prob mu f' A

Main result

Stated in the README together with ge0_integral_density_prob.

Statement as written in the source

Lemma eq_density_prob d (T : measurableType d) (R : realType)
    (mu : probability T R) (f f' : T -> R) :
  prob_density mu f -> prob_density mu f' ->
  ae_eq mu [set: T] (fun x => (f x)%:E) (fun x => (f' x)%:E) ->
  forall A, measurable A -> density_prob mu f A = density_prob mu f' A.

Used by 1 declaration in 1 file

this file: eq_density_law

definition density_law main result source, line 229

Type

forall {d : measure_display} {T : measurableType d} {R : realType} 
  (mu : probability T R) (f : T -> R),
prob_density mu f -> set T -> \bar R

Definition

Definition density_law d (T : measurableType d) (R : realType)
    (mu : probability T R) (f : T -> R) (hf : prob_density mu f) :
    set T -> \bar R :=
  fun A => (\int[mu]_(x in A) (f x)%:E)%E.

The constructor with the proof that f is a density: the set function A |-> int_A f dmu itself, with no fallback.

Main result, as the README states it

The constructor with a proof that f is a density: for hf : prob_density mu f, density_law mu f hf is the probability A |-> int_A f dmu, by definition and with no fallback to mu. It is density_prob mu f, and integrals against the two agree; density_law_dominates, ge0_integral_density_law, integrable_density_law, integral_density_law, eq_density_law and tuple_prod_density_law restate the three rows above for it.

Used by 15 declarations in 1 file

this file: L0, L_ge0, L_sigma_additive, instance at line 256, L_setT, instance at line 261, density_lawE, density_law_prob, integral_density_law_prob, density_law_dominates, ge0_integral_density_law, integrable_density_law, integral_density_law, eq_density_law, tuple_prod_density_law

Arguments density_law {d T R} mu f hf.

sectiondensity_law_measure

Context d (T : measurableType d) (R : realType).
Variables (mu : probability T R) (f : T -> R) (hf : prob_density mu f).
Local Notation L := (density_law mu f hf).
Local Open Scope ereal_scope.

let mF section-local source, line 241

Let mF : measurable_fun [set: T] (fun x => (f x)%:E).

Used by 1 declaration in 1 file

this file: L_sigma_additive

let F0 section-local source, line 244

Let F0 x : 0 <= (f x)%:E.

Used by 2 declarations in 1 file

this file: L_ge0, L_sigma_additive

let L0 section-local source, line 247

Let L0 : L set0 = 0.

Used by 1 declaration in 1 file

this file: instance at line 256

let L_ge0 section-local source, line 250

Let L_ge0 A : 0 <= L A.

Used by 1 declaration in 1 file

this file: instance at line 256

let L_sigma_additive section-local source, line 253

Let L_sigma_additive : semi_sigma_additive L.

Used by 1 declaration in 1 file

this file: instance at line 256

instance instance at line 256 source, line 256

HB.instance Definition _ := isMeasure.Build _ _ _ L L0 L_ge0 L_sigma_additive.

let L_setT section-local source, line 258

Let L_setT : L [set: T] = 1.

Used by 1 declaration in 1 file

this file: instance at line 261

instance instance at line 261 source, line 261

HB.instance Definition _ := @Measure_isProbability.Build _ _ R L L_setT.

lemma density_lawE main result source, line 263

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R] (hf : prob_density mu f) 
  (A : set T),
density_law mu f hf A = (\int[mu]_(x in A) (f x)%:E)%E

Main result

Stated in the README together with density_law.

Statement as written in the source

Lemma density_lawE A : L A = \int[mu]_(x in A) (f x)%:E.

sectiondensity_law_integral

Context d (T : measurableType d) (R : realType).
Variables (mu : probability T R) (f : T -> R) (hf : prob_density mu f).
Local Notation L := (density_law mu f hf).
Local Open Scope ereal_scope.

lemma density_law_prob main result source, line 275

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R] (hf : prob_density mu f),
density_law mu f hf = density_prob mu f

density_law and density_prob agree when f is a density.

Main result

Stated in the README together with density_law.

Statement as written in the source

Lemma density_law_prob : L = density_prob mu f.

Used by 3 declarations in 1 file

this file: density_law_dominates, eq_density_law, tuple_prod_density_law

lemma integral_density_law_prob main result source, line 278

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R] (hf : prob_density mu f) 
  (g : T -> \bar R) (D : set T),
(\int[density_law mu f hf]_(x in D) g x)%E = (\int[density_prob mu f]_(x in D) g x)%E

Main result

Stated in the README together with density_law.

Statement as written in the source

Lemma integral_density_law_prob (g : T -> \bar R) D :
  \int[L]_(x in D) g x = \int[density_prob mu f]_(x in D) g x.

Used by 3 declarations in 1 file

this file: ge0_integral_density_law, integrable_density_law, integral_density_law

lemma density_law_dominates source, line 284

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R] (hf : prob_density mu f),
density_law mu f hf `<< mu

Statement as written in the source

Lemma density_law_dominates : L `<< mu.

lemma ge0_integral_density_law source, line 287

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R] (hf : prob_density mu f) 
  [g : T -> \bar R] [E : set T],
d.-measurable E ->
(forall x : T, (0%R <= g x)%E) ->
measurable_fun E g ->
(\int[density_law mu f hf]_(x in E) g x)%E = (\int[mu]_(x in E) (g x * (f x)%:E))%E

Statement as written in the source

Lemma ge0_integral_density_law (g : T -> \bar R) E : measurable E ->
  (forall x, 0 <= g x) -> measurable_fun E g ->
  \int[L]_(x in E) g x = \int[mu]_(x in E) (g x * (f x)%:E).

lemma integrable_density_law source, line 295

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R] (hf : prob_density mu f) 
  [g : T -> \bar R] [E : set T],
d.-measurable E ->
measurable_fun E g ->
(density_law mu f hf).-integrable E g <->
mu.-integrable E (fun x : T => (g x * (f x)%:E)%E)

Statement as written in the source

Lemma integrable_density_law (g : T -> \bar R) E : measurable E ->
  measurable_fun E g ->
  L.-integrable E g <-> mu.-integrable E (fun x => g x * (f x)%:E).

Used by 1 declaration in 1 file

this file: integral_density_law

lemma integral_density_law source, line 308

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f : T -> R] [hf : prob_density mu f] 
  [g : T -> \bar R] [E : set T],
d.-measurable E ->
(density_law mu f hf).-integrable E g ->
(\int[density_law mu f hf]_(x in E) g x)%E = (\int[mu]_(x in E) (g x * (f x)%:E))%E

Statement as written in the source

Lemma integral_density_law (g : T -> \bar R) E : measurable E ->
  L.-integrable E g ->
  \int[L]_(x in E) g x = \int[mu]_(x in E) (g x * (f x)%:E).

lemma eq_density_law source, line 319

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : probability T R] [f f' : T -> R] (hf : prob_density mu f)
  (hf' : prob_density mu f'),
ae_eq mu [set: T] (fun x : T => (f x)%:E) (fun x : T => (f' x)%:E) ->
forall [A : set T], d.-measurable A -> density_law mu f hf A = density_law mu f' hf' A

Statement as written in the source

Lemma eq_density_law d (T : measurableType d) (R : realType)
    (mu : probability T R) (f f' : T -> R) (hf : prob_density mu f)
    (hf' : prob_density mu f') :
  ae_eq mu [set: T] (fun x => (f x)%:E) (fun x => (f' x)%:E) ->
  forall A, measurable A -> density_law mu f hf A = density_law mu f' hf' A.

sectiontuple_prod_density

Context d (T : measurableType d) (R : realType).
Local Open Scope ereal_scope.

lemma indic_tuple_box main result source, line 333

forall [d : measure_display] [T : measurableType d] (R : realType) 
  [n : nat] (A : 'I_n -> set T) (x : n.-tuple T),
\1_(tuple_box A) x = \prod_(k < n) \1_(A k) (tnth x k)

The indicator of a box is the product of the indicators of its sides.

Main result

Stated in the README together with prob_density_tuple_prod.

Statement as written in the source

Lemma indic_tuple_box n (A : 'I_n -> set T) (x : n.-tuple T) :
  (\1_(tuple_box A) x = \prod_(k < n) \1_(A k) (tnth x k) :> R)%R.

Used by 1 declaration in 1 file

this file: tuple_prod_density

lemma prob_density_tuple_prod main result source, line 345

forall [d : measure_display] [T : measurableType d] [R : realType]
  [nu : nat -> probability T R] [f : nat -> T -> R] [n : nat],
(forall k : nat, (k < n)%N -> prob_density (nu k) (f k)) ->
prob_density (tuple_prod nu n) (fun x : n.-tuple T => \prod_(k < n) f k (tnth x k))

Main result, as the README states it

If f_k is a density against nu_k for every k < n, the product of the laws density_prob nu_k f_k has the density x |-> prod_k f_k (x_k) against tuple_prod nu n.

Statement as written in the source

Lemma prob_density_tuple_prod (nu : nat -> probability T R)
    (f : nat -> T -> R) n :
  (forall k, (k < n)%N -> prob_density (nu k) (f k)) ->
  prob_density (tuple_prod nu n) (fun x => \prod_(k < n) f k (tnth x k))%R.

Used by 1 declaration in 1 file

this file: tuple_prod_density

lemma tuple_prod_density main result source, line 370

forall [d : measure_display] [T : measurableType d] [R : realType]
  [nu : nat -> probability T R] [f : nat -> T -> R] [n : nat] [E : set (n.-tuple T)],
(forall k : nat, (k < n)%N -> prob_density (nu k) (f k)) ->
(measure_tuple_display d).-measurable E ->
tuple_prod (fun k : nat => density_prob (nu k) (f k)) n E =
(\int[tuple_prod nu n]_(x in E) (\prod_(k < n) f k (tnth x k))%:E)%E

Main result

Stated in the README together with prob_density_tuple_prod.

Statement as written in the source

Lemma tuple_prod_density (nu : nat -> probability T R) (f : nat -> T -> R)
    n E :
  (forall k, (k < n)%N -> prob_density (nu k) (f k)) -> measurable E ->
  tuple_prod (fun k => density_prob (nu k) (f k)) n E =
  \int[tuple_prod nu n]_(x in E) (\prod_(k < n) f k (tnth x k))%:E.

Used by 1 declaration in 1 file

this file: tuple_prod_density_law

lemma tuple_prod_density_law source, line 409

forall [d : measure_display] [T : measurableType d] [R : realType]
  [nu : nat -> probability T R] [f : nat -> T -> R]
  (hf : forall k : nat, prob_density (nu k) (f k)) [n : nat] [E : set (n.-tuple T)],
(measure_tuple_display d).-measurable E ->
tuple_prod (fun k : nat => density_law (nu k) (f k) (hf k)) n E =
(\int[tuple_prod nu n]_(x in E) (\prod_(k < n) f k (tnth x k))%:E)%E

Statement as written in the source

Lemma tuple_prod_density_law (nu : nat -> probability T R) (f : nat -> T -> R)
    (hf : forall k, prob_density (nu k) (f k)) n E : measurable E ->
  tuple_prod (fun k => density_law (nu k) (f k) (hf k)) n E =
  \int[tuple_prod nu n]_(x in E) (\prod_(k < n) f k (tnth x k))%:E.

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.