Average over a finset #
This file defines Finset.expect
, the average (aka expectation) of a function over a finset.
Notation #
𝔼 i ∈ s, f i
is notation forFinset.expect s f
. It is the expectation off i
wherei
ranges over the finite sets
(either aFinset
or aSet
with aFintype
instance).𝔼 i, f i
is notation forFinset.expect Finset.univ f
. It is the expectation off i
wherei
ranges over the finite domain off
.𝔼 i ∈ s with p i, f i
is notation forFinset.expect (Finset.filter p s) f
. This is referred to asexpectWith
in lemma names.𝔼 (i ∈ s) (j ∈ t), f i j
is notation forFinset.expect (s ×ˢ t) (fun ⟨i, j⟩ ↦ f i j)
.
Implementation notes #
This definition is a special case of the general convex combination operator in a convex space. However:
- We don't yet have general convex spaces.
- The uniform weights case is an overwhelmingly useful special case which should have its own API.
When convex spaces are finally defined, we should redefine Finset.expect
in terms of that convex
combination operator.
TODO #
- Connect
Finset.expect
with the expectation overs
in the probability theory sense. - Give a formulation of Jensen's inequality in this language.
𝔼 i ∈ s, f i
is notation forFinset.expect s f
. It is the expectation off i
wherei
ranges over the finite sets
(either aFinset
or aSet
with aFintype
instance).𝔼 i, f i
is notation forFinset.expect Finset.univ f
. It is the expectation off i
wherei
ranges over the finite domain off
.𝔼 i ∈ s with p i, f i
is notation forFinset.expect (Finset.filter p s) f
.𝔼 (i ∈ s) (j ∈ t), f i j
is notation forFinset.expect (s ×ˢ t) (fun ⟨i, j⟩ ↦ f i j)
.
These support destructuring, for example 𝔼 ⟨i, j⟩ ∈ s ×ˢ t, f i j
.
Notation: "𝔼" bigOpBinders* ("with" term)? "," term
Equations
- One or more equations did not get rendered due to their size.
Instances For
Delaborator for Finset.expect
. The pp.funBinderTypes
option controls whether
to show the domain type when the expect is over Finset.univ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reorder an average.
The difference with Finset.expect_bij'
is that the bijection is specified as a surjective
injection, rather than by an inverse function.
The difference with Finset.expect_nbij
is that the bijection is allowed to use membership of the
domain of the average, rather than being a non-dependent function.
Reorder an average.
The difference with Finset.expect_bij
is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with Finset.expect_nbij'
is that the bijection and its inverse are allowed to use
membership of the domains of the averages, rather than being non-dependent functions.
Reorder an average.
The difference with Finset.expect_nbij'
is that the bijection is specified as a surjective
injection, rather than by an inverse function.
The difference with Finset.expect_bij
is that the bijection is a non-dependent function, rather
than being allowed to use membership of the domain of the average.
Reorder an average.
The difference with Finset.expect_nbij
is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with Finset.expect_bij'
is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the averages.
The difference with Finset.expect_equiv
is that bijectivity is only required to hold on the
domains of the averages, rather than on the entire types.
Finset.expect_equiv
is a specialization of Finset.expect_bij
that automatically fills in
most arguments.
Expectation over a product set equals the expectation of the fiberwise expectations.
For rewriting in the reverse direction, use Finset.expect_product'
.
Expectation over a product set equals the expectation of the fiberwise expectations.
For rewriting in the reverse direction, use Finset.expect_product
.
Fintype.expect_bijective
is a variant of Finset.expect_bij
that accepts
Function.Bijective
.
See Function.Bijective.expect_comp
for a version without h
.
Fintype.expect_equiv
is a specialization of Finset.expect_bij
that automatically fills in
most arguments.
See Equiv.expect_comp
for a version without h
.