Mathlib.Algebra.BigOperators.Expect

Finset.expect definition

[AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (f : ι → M) : M

Full source

/-- Average of a function over a finset. If the finset is empty, this is equal to zero. -/
def Finset.expect [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (f : ι → M) : M :=
  (#s : ℚ≥0)⁻¹ • ∑ i ∈ s, f i

Expectation (average) over a finite set

Informal description

Given an additive commutative monoid $M$ with a scalar multiplication by nonnegative rational numbers, and a finite set $s$ of type `Finset ι`, the expectation (average) of a function $f : ι \to M$ over $s$ is defined as $(1/|s|) \cdot \sum_{i \in s} f(i)$, where $|s|$ is the cardinality of $s$. If $s$ is empty, the expectation is defined to be zero.

BigOperators.bigexpect definition

: Lean.ParserDescr✝

Full source

/--
* `𝔼 i ∈ s, f i` is notation for `Finset.expect s f`. It is the expectation of `f i` where `i`
  ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
* `𝔼 i, f i` is notation for `Finset.expect Finset.univ f`. It is the expectation of `f i` where `i`
  ranges over the finite domain of `f`.
* `𝔼 i ∈ s with p i, f i` is notation for `Finset.expect (Finset.filter p s) f`.
* `𝔼 (i ∈ s) (j ∈ t), f i j` is notation for `Finset.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` -/
scoped syntax (name := bigexpect) "𝔼 " bigOpBinders ("with " term)? ", " term:67 : term

Expectation notation for finite sets

Informal description

The notation `𝔼 i ∈ s, f i` represents the expectation (average) of the function `f` over the finite set `s`. Variants include: - `𝔼 i, f i` for expectation over the entire domain of `f` - `𝔼 i ∈ s with p i, f i` for expectation over the subset of `s` satisfying predicate `p` - `𝔼 (i ∈ s) (j ∈ t), f i j` for expectation over the product set `s × t` These notations support destructuring patterns like `𝔼 ⟨i, j⟩ ∈ s × t, f i j`.

BigOperators.delabFinsetExpect definition

: Delab

Full source

/-- Delaborator for `Finset.expect`. The `pp.funBinderTypes` option controls whether
to show the domain type when the expect is over `Finset.univ`. -/
@[scoped app_delab Finset.expect] def delabFinsetExpect : Delab :=
  whenPPOption getPPNotation <| withOverApp 6 <| do
  let #[_, _, _, _, s, f] := (← getExpr).getAppArgs | failure
  guardguard <| f.isLambda
  let ppDomain ← getPPOption getPPFunBinderTypes
  let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
    return (i, ← delab)
  if s.isAppOfArity ``Finset.univ 2 then
    let binder ←
      if ppDomain then
        let ty ← withNaryArg 0 delab
        `(bigOpBinder| $(.mk i):ident : $ty)
      else
        `(bigOpBinder| $(.mk i):ident)
    `(𝔼 $binder:bigOpBinder, $body)
  else
    let ss ← withNaryArg 4 <| delab
    `(𝔼 $(.mk i):ident ∈ $ss, $body)

Average over a finite set

Informal description

The average (expectation) of a function $f$ over a finite set $s$ is defined as $\mathbb{E}_{i \in s} f(i) = \left(\sum_{i \in s} f(i)\right) / |s|$, where $|s|$ denotes the cardinality of $s$. This is a special case of convex combination with uniform weights.

Finset.expect_univ theorem

[Fintype ι] : 𝔼 i, f i = (∑ i, f i) /ℚ Fintype.card ι

Full source

lemma expect_univ [Fintype ι] : 𝔼 i, f i = (∑ i, f i) /ℚ Fintype.card ι := by
  rw [expect, card_univ]

Expectation over Universal Finite Set Equals Normalized Sum

Informal description

For a finite type $\iota$ and a function $f \colon \iota \to M$ where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, the expectation (average) of $f$ over the universal finite set is given by \[ \mathbb{E}_{i} f(i) = \frac{\sum_{i} f(i)}{|\iota|}, \] where $|\iota|$ denotes the cardinality of the finite type $\iota$.

Finset.expect_empty theorem

(f : ι → M) : 𝔼 i ∈ ∅, f i = 0

Full source

@[simp] lemma expect_empty (f : ι → M) : 𝔼 i ∈ ∅, f i = 0 := by simp [expect]

Expectation over Empty Set is Zero

Informal description

For any function $f : \iota \to M$ from a type $\iota$ to an additive commutative monoid $M$ with a scalar multiplication by nonnegative rational numbers, the expectation (average) of $f$ over the empty finite set $\emptyset$ is equal to $0$.

Finset.expect_singleton theorem

(f : ι → M) (i : ι) : 𝔼 j ∈ { i }, f j = f i

Full source

@[simp] lemma expect_singleton (f : ι → M) (i : ι) : 𝔼 j ∈ {i}, f j = f i := by simp [expect]

Expectation over Singleton: $\mathbb{E}_{j \in \{i\}} f(j) = f(i)$

Informal description

For any function $f \colon \iota \to M$ and any element $i \in \iota$, the expectation (average) of $f$ over the singleton set $\{i\}$ is equal to $f(i)$, i.e., \[ \mathbb{E}_{j \in \{i\}} f(j) = f(i). \]

Finset.expect_const_zero theorem

(s : Finset ι) : 𝔼 _i ∈ s, (0 : M) = 0

Full source

@[simp] lemma expect_const_zero (s : Finset ι) : 𝔼 _i ∈ s, (0 : M) = 0 := by simp [expect]

Expectation of Zero Function is Zero

Informal description

For any finite set $s$ of type `Finset ι` and the zero function $0 : M$, the expectation (average) of $0$ over $s$ is equal to $0$, i.e., $\mathbb{E}_{i \in s} 0 = 0$.

Finset.expect_congr theorem

{t : Finset ι} (hst : s = t) (h : ∀ i ∈ t, f i = g i) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Full source

@[congr]
lemma expect_congr {t : Finset ι} (hst : s = t) (h : ∀ i ∈ t, f i = g i) :
    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by rw [expect, expect, sum_congr hst h, hst]

Equality of Expectations under Function Equality on Equal Finite Sets

Informal description

Let $s$ and $t$ be finite sets of type $\iota$, and let $f, g : \iota \to M$ be functions where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. If $s = t$ and for every $i \in t$ we have $f(i) = g(i)$, then the expectation (average) of $f$ over $s$ equals the expectation of $g$ over $t$, i.e., \[ \mathbb{E}_{i \in s} f(i) = \mathbb{E}_{i \in t} g(i). \]

Finset.expectWith_congr theorem

 (hst : s = t) (hpq : ∀ i ∈ t, p i ↔ q i) (h : ∀ i ∈ t, q i → f i = g i) : 𝔼 i ∈ s with p i, f i = 𝔼 i ∈ t with q i, g i

Full source

lemma expectWith_congr (hst : s = t) (hpq : ∀ i ∈ t, p i ↔ q i) (h : ∀ i ∈ t, q i → f i = g i) :
    𝔼 i ∈ s with p i, f i = 𝔼 i ∈ t with q i, g i :=
  expect_congr (by rw [hst, filter_inj'.2 hpq]) <| by simpa using h

Equality of Expectations under Predicate and Function Equality on Filtered Finite Sets

Informal description

Let $s$ and $t$ be finite sets of type $\iota$, and let $p, q : \iota \to \text{Prop}$ be predicates and $f, g : \iota \to M$ be functions where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. If $s = t$, for every $i \in t$ we have $p(i) \leftrightarrow q(i)$, and for every $i \in t$ satisfying $q(i)$ we have $f(i) = g(i)$, then the expectation (average) of $f$ over the filtered set $\{i \in s \mid p(i)\}$ equals the expectation of $g$ over the filtered set $\{i \in t \mid q(i)\}$, i.e., \[ \mathbb{E}_{i \in s \text{ with } p(i)} f(i) = \mathbb{E}_{i \in t \text{ with } q(i)} g(i). \]

Finset.expect_sum_comm theorem

 (s : Finset ι) (t : Finset κ) (f : ι → κ → M) : 𝔼 i ∈ s, ∑ j ∈ t, f i j = ∑ j ∈ t, 𝔼 i ∈ s, f i j

Full source

lemma expect_sum_comm (s : Finset ι) (t : Finset κ) (f : ι → κ → M) :
    𝔼 i ∈ s, ∑ j ∈ t, f i j = ∑ j ∈ t, 𝔼 i ∈ s, f i j := by
  simpa only [expect, smul_sum] using sum_comm

Commutation of Expectation and Sum over Finite Sets

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. For any finite sets $s \subseteq \iota$ and $t \subseteq \kappa$, and any function $f : \iota \times \kappa \to M$, the average over $s$ of the sum of $f(i,j)$ over $t$ equals the sum over $t$ of the average of $f(i,j)$ over $s$. That is, $$ \frac{1}{|s|} \sum_{i \in s} \left( \sum_{j \in t} f(i,j) \right) = \sum_{j \in t} \left( \frac{1}{|s|} \sum_{i \in s} f(i,j) \right). $$

Finset.expect_comm theorem

 (s : Finset ι) (t : Finset κ) (f : ι → κ → M) : 𝔼 i ∈ s, 𝔼 j ∈ t, f i j = 𝔼 j ∈ t, 𝔼 i ∈ s, f i j

Full source

lemma expect_comm (s : Finset ι) (t : Finset κ) (f : ι → κ → M) :
    𝔼 i ∈ s, 𝔼 j ∈ t, f i j = 𝔼 j ∈ t, 𝔼 i ∈ s, f i j := by
  rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm]

Commutation of Double Averages over Finite Sets

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. For any finite sets $s \subseteq \iota$ and $t \subseteq \kappa$, and any function $f : \iota \times \kappa \to M$, the average over $s$ of the average over $t$ of $f(i,j)$ equals the average over $t$ of the average over $s$ of $f(i,j)$. That is, $$ \frac{1}{|s|} \sum_{i \in s} \left( \frac{1}{|t|} \sum_{j \in t} f(i,j) \right) = \frac{1}{|t|} \sum_{j \in t} \left( \frac{1}{|s|} \sum_{i \in s} f(i,j) \right). $$

Finset.expect_eq_zero theorem

(h : ∀ i ∈ s, f i = 0) : 𝔼 i ∈ s, f i = 0

Full source

lemma expect_eq_zero (h : ∀ i ∈ s, f i = 0) : 𝔼 i ∈ s, f i = 0 :=
  (expect_congr rfl h).trans s.expect_const_zero

Vanishing Expectation for Zero-Valued Functions

Informal description

For any finite set $s$ and any function $f \colon \iota \to M$ where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, if $f(i) = 0$ for all $i \in s$, then the expectation (average) of $f$ over $s$ is zero, i.e., \[ \mathbb{E}_{i \in s} f(i) = 0. \]

Finset.exists_ne_zero_of_expect_ne_zero theorem

(h : 𝔼 i ∈ s, f i ≠ 0) : ∃ i ∈ s, f i ≠ 0

Full source

lemma exists_ne_zero_of_expect_ne_zero (h : 𝔼 i ∈ s, f i𝔼 i ∈ s, f i ≠ 0) : ∃ i ∈ s, f i ≠ 0 := by
  contrapose! h; exact expect_eq_zero h

Nonzero Expectation Implies Existence of Nonzero Function Value

Informal description

For any finite set $s$ and any function $f \colon \iota \to M$, where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, if the expectation (average) of $f$ over $s$ is nonzero, then there exists an element $i \in s$ such that $f(i) \neq 0$. That is, \[ \mathbb{E}_{i \in s} f(i) \neq 0 \implies \exists i \in s, f(i) \neq 0. \]

Finset.expect_add_distrib theorem

(s : Finset ι) (f g : ι → M) : 𝔼 i ∈ s, (f i + g i) = 𝔼 i ∈ s, f i + 𝔼 i ∈ s, g i

Full source

lemma expect_add_distrib (s : Finset ι) (f g : ι → M) :
    𝔼 i ∈ s, (f i + g i) = 𝔼 i ∈ s, f i + 𝔼 i ∈ s, g i := by
  simp [expect, sum_add_distrib]

Linearity of Expectation over Finite Sets

Informal description

For any finite set $s$ and any functions $f, g \colon \iota \to M$ where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, the expectation (average) of the sum $f + g$ over $s$ is equal to the sum of the expectations of $f$ and $g$ over $s$. That is, \[ \mathbb{E}_{i \in s} [f(i) + g(i)] = \mathbb{E}_{i \in s} f(i) + \mathbb{E}_{i \in s} g(i). \]

Finset.expect_add_expect_comm theorem

 (f₁ f₂ g₁ g₂ : ι → M) :
  𝔼 i ∈ s, (f₁ i + f₂ i) + 𝔼 i ∈ s, (g₁ i + g₂ i) = 𝔼 i ∈ s, (f₁ i + g₁ i) + 𝔼 i ∈ s, (f₂ i + g₂ i)

Full source

lemma expect_add_expect_comm (f₁ f₂ g₁ g₂ : ι → M) :
    𝔼 i ∈ s, (f₁ i + f₂ i) + 𝔼 i ∈ s, (g₁ i + g₂ i) =
      𝔼 i ∈ s, (f₁ i + g₁ i) + 𝔼 i ∈ s, (f₂ i + g₂ i) := by
  simp_rw [expect_add_distrib, add_add_add_comm]

Commutativity of Expectation for Sums over Finite Sets

Informal description

For any finite set $s$ and any functions $f_1, f_2, g_1, g_2 \colon \iota \to M$, where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, the following equality holds: \[ \mathbb{E}_{i \in s} [f_1(i) + f_2(i)] + \mathbb{E}_{i \in s} [g_1(i) + g_2(i)] = \mathbb{E}_{i \in s} [f_1(i) + g_1(i)] + \mathbb{E}_{i \in s} [f_2(i) + g_2(i)]. \]

Finset.expect_eq_single_of_mem theorem

(i : ι) (hi : i ∈ s) (h : ∀ j ∈ s, j ≠ i → f j = 0) : 𝔼 i ∈ s, f i = f i /ℚ #s

Full source

lemma expect_eq_single_of_mem (i : ι) (hi : i ∈ s) (h : ∀ j ∈ s, j ≠ i → f j = 0) :
    𝔼 i ∈ s, f i = f i /ℚ #s := by rw [expect, sum_eq_single_of_mem _ hi h]

Expectation of a Function with Single Nonzero Value on a Finite Set

Informal description

Let $s$ be a finite set and $f \colon \iota \to M$ a function, where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. If there exists an element $i \in s$ such that $f(j) = 0$ for all $j \in s$ with $j \neq i$, then the expectation (average) of $f$ over $s$ is equal to $f(i)$ divided by the cardinality of $s$, i.e., \[ \mathbb{E}_{i \in s} f(i) = \frac{f(i)}{\#s}. \]

Finset.expect_ite_zero theorem

 (s : Finset ι) (p : ι → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : M) :
  𝔼 i ∈ s, ite (p i) a 0 = ite (∃ i ∈ s, p i) (a /ℚ #s) 0

Full source

lemma expect_ite_zero (s : Finset ι) (p : ι → Prop) [DecidablePred p]
    (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : M) :
    𝔼 i ∈ s, ite (p i) a 0 = ite (∃ i ∈ s, p i) (a /ℚ #s) 0 := by
  split_ifs <;> simp [expect, sum_ite_zero _ _ h, *]

Expectation of Indicator Function with Unique Satisfier

Informal description

Let $s$ be a finite set of type $\iota$, $p$ a predicate on $\iota$ with decidable values, and $a$ an element of an additive commutative monoid $M$ with scalar multiplication by nonnegative rational numbers. Suppose that for any $i, j \in s$, if $p(i)$ and $p(j)$ hold, then $i = j$. Then the expectation (average) over $s$ of the function $\mathrm{ite}(p(i), a, 0)$ is equal to $\mathrm{ite}(\exists i \in s, p(i), a / \#s, 0)$, where $\#s$ denotes the cardinality of $s$.

Finset.expect_ite_mem theorem

 (s t : Finset ι) (f : ι → M) : 𝔼 i ∈ s, (if i ∈ t then f i else 0) = (#(s ∩ t) / #s : ℚ≥0) • 𝔼 i ∈ s ∩ t, f i

Full source

lemma expect_ite_mem (s t : Finset ι) (f : ι → M) :
    𝔼 i ∈ s, (if i ∈ t then f i else 0) = (#(s ∩ t) / #s : ℚ≥0) • 𝔼 i ∈ s ∩ t, f i := by
  obtain hst | hst := (s ∩ t).eq_empty_or_nonempty
  · simp [expect, hst]
  · simp [expect, smul_smul, ← inv_mul_eq_div, hst.card_ne_zero]

Expectation of Restricted Function over Finite Set Intersection

Informal description

Let $s$ and $t$ be finite sets of type $\iota$, and let $f \colon \iota \to M$ be a function, where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. The expectation (average) over $s$ of the function that equals $f(i)$ when $i \in t$ and zero otherwise is equal to the scalar multiple of the expectation of $f$ over $s \cap t$, where the scalar is the ratio of the cardinality of $s \cap t$ to the cardinality of $s$. That is, \[ \mathbb{E}_{i \in s} \left( \begin{cases} f(i) & \text{if } i \in t \\ 0 & \text{otherwise} \end{cases} \right) = \left( \frac{\#(s \cap t)}{\#s} \right) \cdot \mathbb{E}_{i \in s \cap t} f(i). \]

Finset.expect_dite_eq theorem

 (i : ι) (f : ∀ j, i = j → M) : 𝔼 j ∈ s, (if h : i = j then f j h else 0) = if i ∈ s then f i rfl /ℚ #s else 0

Full source

@[simp] lemma expect_dite_eq (i : ι) (f : ∀ j, i = j → M) :
    𝔼 j ∈ s, (if h : i = j then f j h else 0) = if i ∈ s then f i rfl /ℚ #s else 0 := by
  split_ifs <;> simp [expect, *]

Expectation of a Dependent Indicator Function at a Fixed Point

Informal description

Let $s$ be a finite set of type `Finset ι`, and let $f : \forall j, (i = j) \to M$ be a function that depends on a proof of equality with a fixed element $i \in \iota$. The expectation (average) over $s$ of the function that is $f(j)$ when $i = j$ and zero otherwise is equal to $f(i) / \#s$ if $i \in s$, and zero otherwise. Here $\#s$ denotes the cardinality of $s$.

Finset.expect_dite_eq' theorem

 (i : ι) (f : ∀ j, j = i → M) : 𝔼 j ∈ s, (if h : j = i then f j h else 0) = if i ∈ s then f i rfl /ℚ #s else 0

Full source

@[simp] lemma expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) :
    𝔼 j ∈ s, (if h : j = i then f j h else 0) = if i ∈ s then f i rfl /ℚ #s else 0 := by
  split_ifs <;> simp [expect, *]

Expectation of Conditional Function over Finite Set

Informal description

For any element $i$ in a type $\iota$ and a function $f$ that maps elements $j$ of $\iota$ to a value in an additive commutative monoid $M$ when $j = i$, the expectation (average) over a finite set $s \subseteq \iota$ of the function $\lambda j, \text{if } j = i \text{ then } f j \text{ else } 0$ is equal to $\frac{f i}{|s|}$ if $i \in s$, and $0$ otherwise. Here, $|s|$ denotes the cardinality of $s$.

Finset.expect_ite_eq theorem

(i : ι) (f : ι → M) : 𝔼 j ∈ s, (if i = j then f j else 0) = if i ∈ s then f i /ℚ #s else 0

Full source

@[simp] lemma expect_ite_eq (i : ι) (f : ι → M) :
    𝔼 j ∈ s, (if i = j then f j else 0) = if i ∈ s then f i /ℚ #s else 0 := by
  split_ifs <;> simp [expect, *]

Expectation of Indicator Function over Finite Set

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and let $s$ be a finite set of type $\iota$. For any element $i \in \iota$ and any function $f \colon \iota \to M$, the expectation (average) of the function $\lambda j, \text{if } i = j \text{ then } f(j) \text{ else } 0$ over $s$ is equal to $f(i)/|s|$ if $i \in s$, and $0$ otherwise. Here $|s|$ denotes the cardinality of $s$.

Finset.expect_ite_eq' theorem

(i : ι) (f : ι → M) : 𝔼 j ∈ s, (if j = i then f j else 0) = if i ∈ s then f i /ℚ #s else 0

Full source

@[simp] lemma expect_ite_eq' (i : ι) (f : ι → M) :
    𝔼 j ∈ s, (if j = i then f j else 0) = if i ∈ s then f i /ℚ #s else 0 := by
  split_ifs <;> simp [expect, *]

Expectation of Indicator Function over Finite Set

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and let $s$ be a finite set of type `Finset ι`. For any element $i \in \iota$ and any function $f : \iota \to M$, the expectation (average) of the function $\lambda j, \text{if } j = i \text{ then } f(j) \text{ else } 0$ over $s$ is equal to $f(i) / \#s$ if $i \in s$, and $0$ otherwise. Here, $\#s$ denotes the cardinality of $s$.

Finset.expect_bij theorem

 (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
  (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) :
  𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Full source

/-- 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. -/
lemma expect_bij (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
  simp_rw [expect, card_bij i hi i_inj i_surj, sum_bij i hi i_inj i_surj h]

Equality of Expectations under Bijection

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and let $s$ and $t$ be finite sets of types $\iota$ and $\kappa$ respectively. Given functions $f \colon \iota \to M$ and $g \colon \kappa \to M$, suppose there exists a function $i \colon \{(a, h_a) \mid a \in s\} \to \kappa$ such that: 1. $i(a, h_a) \in t$ for all $a \in s$ and proof $h_a$ of membership, 2. $f(a) = g(i(a, h_a))$ for all $a \in s$, 3. $i$ is injective (i.e., $i(a_1, h_{a_1}) = i(a_2, h_{a_2})$ implies $a_1 = a_2$), and 4. $i$ is surjective onto $t$ (i.e., for every $b \in t$, there exists $a \in s$ with $i(a, h_a) = b$). Then the expectation (average) of $f$ over $s$ equals the expectation of $g$ over $t$, i.e., \[ \mathbb{E}_{i \in s} f(i) = \mathbb{E}_{i \in t} g(i). \]

Finset.expect_bij' theorem

 (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t) (hj : ∀ a ha, j a ha ∈ s)
  (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a) (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a)
  (h : ∀ a ha, f a = g (i a ha)) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Full source

/-- 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. -/
lemma expect_bij' (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t)
    (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a)
    (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) (h : ∀ a ha, f a = g (i a ha)) :
    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
  simp_rw [expect, card_bij' i j hi hj left_inv right_inv, sum_bij' i j hi hj left_inv right_inv h]

Equality of Expectations under Bijection with Explicit Inverse

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. Let $s$ and $t$ be finite sets of types $\iota$ and $\kappa$ respectively, and let $f \colon \iota \to M$ and $g \colon \kappa \to M$ be functions. Suppose there exist functions: - $i \colon \{(a, h_a) \mid a \in s\} \to \kappa$ with $i(a, h_a) \in t$ for all $a \in s$, - $j \colon \{(b, h_b) \mid b \in t\} \to \iota$ with $j(b, h_b) \in s$ for all $b \in t$, such that: 1. $j$ is a left inverse of $i$ (i.e., $j(i(a, h_a), h_{i(a, h_a)}) = a$ for all $a \in s$), 2. $i$ is a right inverse of $j$ (i.e., $i(j(b, h_b), h_{j(b, h_b)}) = b$ for all $b \in t$), 3. $f(a) = g(i(a, h_a))$ for all $a \in s$. Then the expectations (averages) of $f$ over $s$ and $g$ over $t$ are equal, i.e., \[ \mathbb{E}_{i \in s} f(i) = \mathbb{E}_{i \in t} g(i). \]

Finset.expect_nbij theorem

 (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a)) (i_inj : (s : Set ι).InjOn i)
  (i_surj : (s : Set ι).SurjOn i t) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Full source

/-- 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. -/
lemma expect_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a))
    (i_inj : (s : Set ι).InjOn i) (i_surj : (s : Set ι).SurjOn i t) :
    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
  simp_rw [expect, card_nbij i hi i_inj i_surj, sum_nbij i hi i_inj i_surj h]

Equality of Averages under Non-Dependent Bijection

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and let $s \subseteq \iota$ and $t \subseteq \kappa$ be finite sets. Given functions $f \colon \iota \to M$ and $g \colon \kappa \to M$, suppose there exists a function $i \colon \iota \to \kappa$ such that: 1. $i(a) \in t$ for all $a \in s$, 2. $f(a) = g(i(a))$ for all $a \in s$, 3. $i$ is injective on $s$ (i.e., for any $x_1, x_2 \in s$, $i(x_1) = i(x_2)$ implies $x_1 = x_2$), and 4. $i$ is surjective from $s$ onto $t$ (i.e., for every $b \in t$, there exists $a \in s$ such that $i(a) = b$). Then the average of $f$ over $s$ equals the average of $g$ over $t$, i.e., \[ \mathbb{E}_{a \in s} f(a) = \mathbb{E}_{b \in t} g(b). \]

Finset.expect_nbij' theorem

 (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s) (left_inv : ∀ a ∈ s, j (i a) = a)
  (right_inv : ∀ a ∈ t, i (j a) = a) (h : ∀ a ∈ s, f a = g (i a)) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Full source

/-- 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. -/
lemma expect_nbij' (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s)
    (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a)
    (h : ∀ a ∈ s, f a = g (i a)) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
  simp_rw [expect, card_nbij' i j hi hj left_inv right_inv,
    sum_nbij' i j hi hj left_inv right_inv h]

Equality of Averages under Bijection with Explicit Inverse

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. Let $s \subseteq \iota$ and $t \subseteq \kappa$ be finite sets, and let $f \colon \iota \to M$ and $g \colon \kappa \to M$ be functions. Suppose there exist functions $i \colon \iota \to \kappa$ and $j \colon \kappa \to \iota$ such that: 1. $i(a) \in t$ for all $a \in s$, 2. $j(b) \in s$ for all $b \in t$, 3. $j$ is a left inverse of $i$ on $s$ (i.e., $j(i(a)) = a$ for all $a \in s$), 4. $i$ is a right inverse of $j$ on $t$ (i.e., $i(j(b)) = b$ for all $b \in t$), 5. $f(a) = g(i(a))$ for all $a \in s$. Then the average of $f$ over $s$ equals the average of $g$ over $t$, i.e., \[ \mathbb{E}_{a \in s} f(a) = \mathbb{E}_{b \in t} g(b). \]

Finset.expect_equiv theorem

 (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Full source

/-- `Finset.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in
most arguments. -/
lemma expect_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ si ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by simp_rw [expect, card_equiv e hst, sum_equiv e hst hfg]

Equality of Averages under Bijection: $\mathbb{E}_{i \in s} f(i) = \mathbb{E}_{j \in t} g(j)$ via $e$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and let $s \subseteq \iota$ and $t \subseteq \kappa$ be finite sets. Given functions $f \colon \iota \to M$ and $g \colon \kappa \to M$, suppose there exists a bijection $e \colon \iota \simeq \kappa$ such that: 1. For every $i \in \iota$, $i \in s$ if and only if $e(i) \in t$, 2. For every $i \in s$, $f(i) = g(e(i))$. Then the average of $f$ over $s$ equals the average of $g$ over $t$, i.e., \[ \mathbb{E}_{i \in s} f(i) = \mathbb{E}_{j \in t} g(j). \]

Finset.expect_product theorem

(s : Finset ι) (t : Finset κ) (f : ι × κ → M) : 𝔼 x ∈ s ×ˢ t, f x = 𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j)

Full source

/-- Expectation over a product set equals the expectation of the fiberwise expectations.

For rewriting in the reverse direction, use `Finset.expect_product'`. -/
lemma expect_product (s : Finset ι) (t : Finset κ) (f : ι × κ → M) :
    𝔼 x ∈ s ×ˢ t, f x = 𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j) := by
  simp only [expect, card_product, sum_product, smul_sum, mul_inv, mul_smul, Nat.cast_mul]

Fubini's Theorem for Finite Expectation: $\mathbb{E}_{(i,j) \in s \times t} f(i,j) = \mathbb{E}_{i \in s} \mathbb{E}_{j \in t} f(i,j)$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. For any finite sets $s \subseteq \iota$ and $t \subseteq \kappa$, and any function $f : \iota \times \kappa \to M$, the expectation (average) of $f$ over the product set $s \times t$ equals the expectation over $s$ of the fiberwise expectations over $t$. That is, \[ \mathbb{E}_{(i,j) \in s \times t} f(i,j) = \mathbb{E}_{i \in s} \mathbb{E}_{j \in t} f(i,j). \]

Finset.expect_product' theorem

 (s : Finset ι) (t : Finset κ) (f : ι → κ → M) : 𝔼 i ∈ s ×ˢ t, f i.1 i.2 = 𝔼 i ∈ s, 𝔼 j ∈ t, f i j

Full source

/-- Expectation over a product set equals the expectation of the fiberwise expectations.

For rewriting in the reverse direction, use `Finset.expect_product`. -/
lemma expect_product' (s : Finset ι) (t : Finset κ) (f : ι → κ → M) :
    𝔼 i ∈ s ×ˢ t, f i.1 i.2 = 𝔼 i ∈ s, 𝔼 j ∈ t, f i j := by
  simp only [expect, card_product, sum_product', smul_sum, mul_inv, mul_smul, Nat.cast_mul]

Fubini's Theorem for Finite Expectation: $\mathbb{E}_{(i,j) \in s \times t} f(i,j) = \mathbb{E}_{i \in s} \mathbb{E}_{j \in t} f(i,j)$

Informal description

For any finite sets $s \subseteq \iota$ and $t \subseteq \kappa$, and any function $f \colon \iota \times \kappa \to M$ where $M$ is an additive commutative monoid with scalar multiplication by nonnegative rational numbers, the expectation (average) of $f$ over the product set $s \times t$ equals the expectation over $s$ of the fiberwise expectations over $t$. That is, \[ \mathbb{E}_{(i,j) \in s \times t} f(i,j) = \mathbb{E}_{i \in s} \mathbb{E}_{j \in t} f(i,j). \]

Finset.expect_image theorem

[DecidableEq ι] {m : κ → ι} (hm : (t : Set κ).InjOn m) : 𝔼 i ∈ t.image m, f i = 𝔼 i ∈ t, f (m i)

Full source

@[simp]
lemma expect_image [DecidableEq ι] {m : κ → ι} (hm : (t : Set κ).InjOn m) :
    𝔼 i ∈ t.image m, f i = 𝔼 i ∈ t, f (m i) := by
  simp_rw [expect, card_image_of_injOn hm, sum_image hm]

Expectation over Image of Injective Function: $\mathbb{E}_{i \in m(t)} f(i) = \mathbb{E}_{i \in t} f(m(i))$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and let $f : \iota \to M$ be a function. For any finite set $t \subseteq \kappa$ and any injective function $m : \kappa \to \iota$ on $t$, the expectation (average) of $f$ over the image $m(t)$ equals the expectation of $f \circ m$ over $t$. That is, \[ \mathbb{E}_{i \in m(t)} f(i) = \mathbb{E}_{i \in t} f(m(i)). \]

Finset.expect_inv_index theorem

[DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s⁻¹, f i = 𝔼 i ∈ s, f i⁻¹

Full source

@[simp] lemma expect_inv_index [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → M) :
    𝔼 i ∈ s⁻¹, f i = 𝔼 i ∈ s, f i⁻¹ := expect_image inv_injective.injOn

Invariance of Expectation under Inversion: $\mathbb{E}_{i \in s^{-1}} f(i) = \mathbb{E}_{i \in s} f(i^{-1})$

Informal description

Let $M$ be an additive commutative monoid with scalar multiplication by nonnegative rational numbers, and let $\iota$ be a type with an involutive inversion operation (i.e., $(i^{-1})^{-1} = i$ for all $i \in \iota$). For any finite set $s \subseteq \iota$ and any function $f : \iota \to M$, the expectation (average) of $f$ over the inverted set $s^{-1} = \{i^{-1} \mid i \in s\}$ equals the expectation of the inverted function $i \mapsto f(i^{-1})$ over $s$. That is, \[ \mathbb{E}_{i \in s^{-1}} f(i) = \mathbb{E}_{i \in s} f(i^{-1}). \]

Finset.expect_neg_index theorem

[DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → M) : 𝔼 i ∈ -s, f i = 𝔼 i ∈ s, f (-i)

Full source

@[simp] lemma expect_neg_index [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → M) :
    𝔼 i ∈ -s, f i = 𝔼 i ∈ s, f (-i) := expect_image neg_injective.injOn

Expectation over Negated Set Equals Expectation of Negated Function

Informal description

Let $M$ be an additive commutative monoid with scalar multiplication by nonnegative rational numbers, and let $\iota$ be a type with an involutive negation operation (i.e., $-(-i) = i$ for all $i \in \iota$). For any finite set $s \subseteq \iota$ and any function $f : \iota \to M$, the expectation (average) of $f$ over the negated set $-s$ equals the expectation of $f \circ (-)$ over $s$. That is, \[ \mathbb{E}_{i \in -s} f(i) = \mathbb{E}_{i \in s} f(-i). \]

map_expect theorem

 {F : Type*} [FunLike F M N] [LinearMapClass F ℚ≥0 M N] (g : F) (f : ι → M) (s : Finset ι) :
  g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i)

Full source

lemma _root_.map_expect {F : Type*} [FunLike F M N] [LinearMapClass F ℚ≥0 M N]
    (g : F) (f : ι → M) (s : Finset ι) :
    g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i) := by simp only [expect, map_smul, map_natCast, map_sum]

Linearity of Expectation over Finite Sets

Informal description

Let $M$ and $N$ be additive commutative monoids with scalar multiplication by nonnegative rational numbers, and let $F$ be a type of linear maps from $M$ to $N$. For any linear map $g \in F$, any function $f : \iota \to M$, and any finite set $s \subseteq \iota$, the image of the expectation (average) of $f$ over $s$ under $g$ equals the expectation of $g \circ f$ over $s$. That is, \[ g\left(\mathbb{E}_{i \in s} f(i)\right) = \mathbb{E}_{i \in s} g(f(i)). \]

Finset.card_smul_expect theorem

(s : Finset ι) (f : ι → M) : #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Full source

@[simp]
lemma card_smul_expect (s : Finset ι) (f : ι → M) : #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i := by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp
  · rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]
    exact mod_cast hs.card_ne_zero

Cardinality-Scaled Expectation Equals Sum over Finite Set

Informal description

For any finite set $s$ of type `Finset ι` and any function $f : ι \to M$ where $M$ is an additive commutative monoid with scalar multiplication by nonnegative rational numbers, the scalar multiplication of the cardinality of $s$ with the expectation (average) of $f$ over $s$ equals the sum of $f$ over $s$. That is, \[ |s| \cdot \mathbb{E}_{i \in s} f(i) = \sum_{i \in s} f(i). \]

Fintype.card_smul_expect theorem

[Fintype ι] (f : ι → M) : Fintype.card ι • 𝔼 i, f i = ∑ i, f i

Full source

@[simp] lemma _root_.Fintype.card_smul_expect [Fintype ι] (f : ι → M) :
    Fintype.card ι • 𝔼 i, f i = ∑ i, f i := Finset.card_smul_expect _ _

Cardinality-Scaled Expectation Equals Total Sum over Finite Type

Informal description

For any finite type $\iota$ and any function $f \colon \iota \to M$ where $M$ is an additive commutative monoid with scalar multiplication by nonnegative rational numbers, the scalar multiplication of the cardinality of $\iota$ with the expectation (average) of $f$ over all elements of $\iota$ equals the sum of $f$ over all elements of $\iota$. That is, \[ |\iota| \cdot \mathbb{E}_{i} f(i) = \sum_{i} f(i). \]

Finset.expect_const theorem

(hs : s.Nonempty) (a : M) : 𝔼 _i ∈ s, a = a

Full source

@[simp] lemma expect_const (hs : s.Nonempty) (a : M) : 𝔼 _i ∈ s, a = a := by
  rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]
  exact mod_cast hs.card_ne_zero

Expectation of a Constant Function over a Nonempty Finite Set

Informal description

For any nonempty finite set $s$ and any element $a$ in an additive commutative monoid $M$ with scalar multiplication by nonnegative rational numbers, the expectation (average) of the constant function $f(i) = a$ over $s$ is equal to $a$. That is, \[ \mathbb{E}_{i \in s} a = a. \]

Finset.smul_expect theorem

 {G : Type*} [DistribSMul G M] [SMulCommClass G ℚ≥0 M] (a : G) (s : Finset ι) (f : ι → M) :
  a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i

Full source

lemma smul_expect {G : Type*} [DistribSMul G M] [SMulCommClass G ℚ≥0 M] (a : G)
    (s : Finset ι) (f : ι → M) : a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i := by
  simp only [expect, smul_sum, smul_comm]

Linearity of Expectation under Scalar Multiplication

Informal description

Let $G$ be a type with a distributive scalar multiplication action on an additive commutative monoid $M$, and suppose the scalar multiplications by $G$ and by nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ on $M$ commute. Then for any scalar $a \in G$, any finite set $s$ of type `Finset ι`, and any function $f : ι \to M$, we have: \[ a \cdot \left( \mathbb{E}_{i \in s} f(i) \right) = \mathbb{E}_{i \in s} (a \cdot f(i)) \] where $\mathbb{E}_{i \in s} f(i)$ denotes the expectation (average) of $f$ over $s$.

Finset.expect_sub_distrib theorem

(s : Finset ι) (f g : ι → M) : 𝔼 i ∈ s, (f i - g i) = 𝔼 i ∈ s, f i - 𝔼 i ∈ s, g i

Full source

lemma expect_sub_distrib (s : Finset ι) (f g : ι → M) :
    𝔼 i ∈ s, (f i - g i) = 𝔼 i ∈ s, f i - 𝔼 i ∈ s, g i := by
  simp only [expect, sum_sub_distrib, smul_sub]

Linearity of Expectation for Differences: $\mathbb{E}(f - g) = \mathbb{E}f - \mathbb{E}g$

Informal description

For any finite set $s$ and functions $f, g : \iota \to M$ where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, the expectation of the difference $f - g$ over $s$ equals the difference of the expectations of $f$ and $g$ over $s$. That is, \[ \mathbb{E}_{i \in s} (f(i) - g(i)) = \mathbb{E}_{i \in s} f(i) - \mathbb{E}_{i \in s} g(i). \]

Finset.expect_neg_distrib theorem

(s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, -f i = -𝔼 i ∈ s, f i

Full source

@[simp]
lemma expect_neg_distrib (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, -f i = -𝔼 i ∈ s, f i := by
  simp [expect]

Negation Distributes Over Expectation

Informal description

For any finite set $s$ and any function $f$ from the elements of $s$ to an additive commutative monoid $M$ with a scalar multiplication by nonnegative rational numbers, the expectation (average) of $-f$ over $s$ is equal to the negation of the expectation of $f$ over $s$, i.e., \[ \mathbb{E}_{i \in s} (-f(i)) = -\mathbb{E}_{i \in s} f(i). \]

Finset.card_mul_expect theorem

(s : Finset ι) (f : ι → M) : #s * 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Full source

@[simp] lemma card_mul_expect (s : Finset ι) (f : ι → M) :
    #s * 𝔼 i ∈ s, f i = ∑ i ∈ s, f i := by rw [← nsmul_eq_mul, card_smul_expect]

Cardinality-Expectation Product Equals Sum: $|s| \cdot \mathbb{E} f = \sum f$

Informal description

For any finite set $s$ and any function $f : \iota \to M$ where $M$ is an additive commutative monoid with scalar multiplication by nonnegative rational numbers, the product of the cardinality of $s$ and the expectation (average) of $f$ over $s$ equals the sum of $f$ over $s$. That is, \[ |s| \cdot \mathbb{E}_{i \in s} f(i) = \sum_{i \in s} f(i). \]

Fintype.card_mul_expect theorem

[Fintype ι] (f : ι → M) : Fintype.card ι * 𝔼 i, f i = ∑ i, f i

Full source

@[simp] lemma _root_.Fintype.card_mul_expect [Fintype ι] (f : ι → M) :
    Fintype.card ι * 𝔼 i, f i = ∑ i, f i := Finset.card_mul_expect _ _

Cardinality-Expectation Product Equals Sum for Finite Types: $|\iota| \cdot \mathbb{E} f = \sum f$

Informal description

For any finite type $\iota$ and any function $f \colon \iota \to M$, where $M$ is an additive commutative monoid with scalar multiplication by nonnegative rational numbers, the product of the cardinality of $\iota$ and the expectation (average) of $f$ over all elements of $\iota$ equals the sum of $f$ over all elements of $\iota$. That is, \[ |\iota| \cdot \mathbb{E}_{i} f(i) = \sum_{i} f(i). \]

Finset.expect_mul theorem

[IsScalarTower ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a

Full source

lemma expect_mul [IsScalarTower ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) :
    (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a := by rw [expect, expect, smul_mul_assoc, sum_mul]

Right Multiplication Property of Expectation: $(\mathbb{E} f) * a = \mathbb{E} (f * a)$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers such that the scalar multiplication satisfies the tower property `IsScalarTower ℚ≥0 M M`. For any finite set $s$ of type `Finset ι`, any function $f : ι \to M$, and any element $a \in M$, we have: $$ \left( \mathbb{E}_{i \in s} f(i) \right) * a = \mathbb{E}_{i \in s} (f(i) * a), $$ where $\mathbb{E}_{i \in s} f(i)$ denotes the expectation (average) of $f$ over $s$.

Finset.mul_expect theorem

[SMulCommClass ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) : a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i

Full source

lemma mul_expect [SMulCommClass ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) :
    a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i := by rw [expect, expect, mul_smul_comm, mul_sum]

Commutativity of Multiplication and Expectation: $a \cdot \mathbb{E}_{i \in s} f(i) = \mathbb{E}_{i \in s} (a \cdot f(i))$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and assume that the scalar multiplications by $\mathbb{Q}_{\geq 0}$ and $M$ on $M$ commute. For any finite set $s$ of type `Finset ι`, any function $f \colon \iota \to M$, and any element $a \in M$, we have the identity: $$ a \cdot \left( \mathbb{E}_{i \in s} f(i) \right) = \mathbb{E}_{i \in s} (a \cdot f(i)), $$ where $\mathbb{E}_{i \in s} f(i)$ denotes the expectation (average) of $f$ over $s$.

Finset.expect_mul_expect theorem

 [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M) :
  (𝔼 i ∈ s, f i) * 𝔼 j ∈ t, g j = 𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j

Full source

lemma expect_mul_expect [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (s : Finset ι)
    (t : Finset κ) (f : ι → M) (g : κ → M) :
    (𝔼 i ∈ s, f i) * 𝔼 j ∈ t, g j = 𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j := by
  simp_rw [expect_mul, mul_expect]

Product of Expectations Equals Expectation of Products: $(\mathbb{E} f) * (\mathbb{E} g) = \mathbb{E}_{i,j} (f(i) * g(j))$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, where the scalar multiplication satisfies both the tower property `IsScalarTower ℚ≥0 M M` and the commutativity property `SMulCommClass ℚ≥0 M M`. For any finite sets $s \subseteq \iota$ and $t \subseteq \kappa$, and any functions $f \colon \iota \to M$ and $g \colon \kappa \to M$, the following equality holds: $$ \left( \mathbb{E}_{i \in s} f(i) \right) * \left( \mathbb{E}_{j \in t} g(j) \right) = \mathbb{E}_{i \in s} \mathbb{E}_{j \in t} (f(i) * g(j)), $$ where $\mathbb{E}$ denotes the expectation (average) over the respective finite sets.

Finset.expect_pow theorem

 (s : Finset ι) (f : ι → M) (n : ℕ) : (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun _ : Fin n ↦ s, ∏ i, f (p i)

Full source

lemma expect_pow (s : Finset ι) (f : ι → M) (n : ℕ) :
    (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun _ : Fin n ↦ s, ∏ i, f (p i) := by
  classical
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]

Power of Expectation Equals Expectation of Products: $(\mathbb{E} f)^n = \mathbb{E}_{p \in s^n} \prod_{i=1}^n f(p_i)$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers. For any finite set $s \subseteq \iota$, any function $f \colon \iota \to M$, and any natural number $n$, the $n$-th power of the expectation (average) of $f$ over $s$ equals the expectation of the product $\prod_{i=1}^n f(p_i)$ over all $n$-tuples $p \in s^n$. That is, $$ \left( \mathbb{E}_{i \in s} f(i) \right)^n = \mathbb{E}_{p \in s^n} \prod_{i=1}^n f(p_i). $$

Finset.expect_boole_mul theorem

 [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) : 𝔼 j, ite (i = j) (Fintype.card ι : M) 0 * f j = f i

Full source

lemma expect_boole_mul [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) :
    𝔼 j, ite (i = j) (Fintype.card ι : M) 0 * f j = f i := by
  simp_rw [expect_univ, ite_mul, zero_mul, sum_ite_eq, if_pos (mem_univ _)]
  rw [← @NNRat.cast_natCast M, ← NNRat.smul_def, inv_smul_smul₀]
  simp [Fintype.card_ne_zero]

Expectation of Indicator Function: $\mathbb{E}_j [\mathbb{1}_{i=j} \cdot |\iota| \cdot f(j)] = f(i)$

Informal description

Let $\iota$ be a finite nonempty type with decidable equality, and let $M$ be an additive commutative monoid with scalar multiplication by nonnegative rational numbers. For any function $f \colon \iota \to M$ and any element $i \in \iota$, the expectation (average) over $\iota$ of the function \[ j \mapsto \begin{cases} |\iota| \cdot f(j) & \text{if } i = j, \\ 0 & \text{otherwise}, \end{cases} \] equals $f(i)$, where $|\iota|$ denotes the cardinality of $\iota$.

Finset.expect_boole_mul' theorem

 [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) : 𝔼 j, ite (j = i) (Fintype.card ι : M) 0 * f j = f i

Full source

lemma expect_boole_mul' [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) :
    𝔼 j, ite (j = i) (Fintype.card ι : M) 0 * f j = f i := by
  simp_rw [@eq_comm _ _ i, expect_boole_mul]

Expectation of Indicator Function (Variant): $\mathbb{E}_j [\mathbb{1}_{j=i} \cdot |\iota| \cdot f(j)] = f(i)$

Informal description

Let $\iota$ be a finite nonempty type with decidable equality, and let $M$ be an additive commutative monoid with scalar multiplication by nonnegative rational numbers. For any function $f \colon \iota \to M$ and any element $i \in \iota$, the expectation (average) over $\iota$ of the function \[ j \mapsto \begin{cases} |\iota| \cdot f(j) & \text{if } j = i, \\ 0 & \text{otherwise}, \end{cases} \] equals $f(i)$, where $|\iota|$ denotes the cardinality of $\iota$.

Finset.expect_eq_sum_div_card theorem

(s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / #s

Full source

lemma expect_eq_sum_div_card (s : Finset ι) (f : ι → M) :
    𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / #s := by
  rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]

Expectation as Normalized Sum: $\mathbb{E}_{i \in s} f(i) = \frac{1}{|s|}\sum_{i \in s} f(i)$

Informal description

For any finite set $s$ and any function $f$ from $s$ to an additive commutative monoid $M$ with scalar multiplication by nonnegative rational numbers, the expectation (average) of $f$ over $s$ equals the sum of $f$ over $s$ divided by the cardinality of $s$, i.e., \[ \mathbb{E}_{i \in s} f(i) = \frac{\sum_{i \in s} f(i)}{|s|}. \]

Fintype.expect_eq_sum_div_card theorem

[Fintype ι] (f : ι → M) : 𝔼 i, f i = (∑ i, f i) / Fintype.card ι

Full source

lemma _root_.Fintype.expect_eq_sum_div_card [Fintype ι] (f : ι → M) :
    𝔼 i, f i = (∑ i, f i) / Fintype.card ι := Finset.expect_eq_sum_div_card _ _

Expectation over Finite Type as Normalized Sum: $\mathbb{E} f = \frac{1}{|\iota|}\sum f$

Informal description

For any finite type $\iota$ and any function $f \colon \iota \to M$ where $M$ is an additive commutative monoid with scalar multiplication by nonnegative rational numbers, the expectation (average) of $f$ over all elements of $\iota$ is equal to the sum of $f$ over $\iota$ divided by the cardinality of $\iota$, i.e., \[ \mathbb{E}_{i \in \iota} f(i) = \frac{\sum_{i \in \iota} f(i)}{|\iota|}. \]

Finset.expect_div theorem

(s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a

Full source

lemma expect_div (s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a := by
  simp_rw [div_eq_mul_inv, expect_mul]

Division Property of Expectation: $(\mathbb{E} f) / a = \mathbb{E} (f / a)$

Informal description

For any finite set $s$ of type $\iota$, any function $f \colon \iota \to M$ where $M$ is an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and any element $a \in M$, the following equality holds: $$ \frac{\mathbb{E}_{i \in s} f(i)}{a} = \mathbb{E}_{i \in s} \left( \frac{f(i)}{a} \right), $$ where $\mathbb{E}_{i \in s} f(i)$ denotes the expectation (average) of $f$ over $s$.

Finset.expect_apply theorem

 {α : Type*} {π : α → Type*} [∀ a, CommSemiring (π a)] [∀ a, Module ℚ≥0 (π a)] (s : Finset ι) (f : ι → ∀ a, π a)
  (a : α) : (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a

Full source

@[simp] lemma expect_apply {α : Type*} {π : α → Type*} [∀ a, CommSemiring (π a)]
    [∀ a, Module ℚ≥0 (π a)] (s : Finset ι) (f : ι → ∀ a, π a) (a : α) :
    (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a := by simp [expect]

Linearity of Expectation over Componentwise Evaluation

Informal description

Let $\alpha$ be a type, and for each $a \in \alpha$, let $\pi(a)$ be a commutative semiring with a scalar multiplication by nonnegative rational numbers. Given a finite set $s$ of type `Finset ι` and a function $f : \iota \to \prod_{a \in \alpha} \pi(a)$, for any $a \in \alpha$, the evaluation of the expectation of $f$ at $a$ equals the expectation of the evaluations of $f$ at $a$. That is, \[ \left(\mathbb{E}_{i \in s} f(i)\right)(a) = \mathbb{E}_{i \in s} (f(i)(a)). \]

algebraMap.coe_expect theorem

(s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : N)

Full source

@[simp, norm_cast]
lemma coe_expect (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : N) :=
  map_expect (algebraMap _ _) _ _

Preservation of Expectation under Canonical Map: $\mathbb{E}_{i \in s} f(i) = \mathbb{E}_{i \in s} (f(i) : N)$

Informal description

Let $M$ and $N$ be additive commutative monoids with scalar multiplication by nonnegative rational numbers, and let $s$ be a finite set of type `Finset ι`. For any function $f \colon \iota \to M$, the expectation (average) of $f$ over $s$ equals the expectation of the composition of $f$ with the canonical map from $M$ to $N$. That is, \[ \mathbb{E}_{i \in s} f(i) = \mathbb{E}_{i \in s} (f(i) : N). \]

Fintype.expect_bijective theorem

(e : ι → κ) (he : Bijective e) (f : ι → M) (g : κ → M) (h : ∀ i, f i = g (e i)) : 𝔼 i, f i = 𝔼 i, g i

Full source

/-- `Fintype.expect_bijective` is a variant of `Finset.expect_bij` that accepts
`Function.Bijective`.

See `Function.Bijective.expect_comp` for a version without `h`. -/
lemma expect_bijective (e : ι → κ) (he : Bijective e) (f : ι → M) (g : κ → M)
    (h : ∀ i, f i = g (e i)) : 𝔼 i, f i = 𝔼 i, g i :=
  expect_nbij e (fun _ _ ↦ mem_univ _) (fun i _ ↦ h i) he.injective.injOn <| by
    simpa using he.surjective.surjOn _

Equality of Averages under Bijective Transformation

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and let $\iota$ and $\kappa$ be finite types. Given a bijective function $e \colon \iota \to \kappa$ and functions $f \colon \iota \to M$ and $g \colon \kappa \to M$ such that $f(i) = g(e(i))$ for all $i \in \iota$, the average of $f$ over $\iota$ equals the average of $g$ over $\kappa$, i.e., \[ \mathbb{E}_{i \in \iota} f(i) = \mathbb{E}_{j \in \kappa} g(j). \]

Fintype.expect_equiv theorem

(e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ i, f i = g (e i)) : 𝔼 i, f i = 𝔼 i, g i

Full source

/-- `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`. -/
lemma expect_equiv (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ i, f i = g (e i)) :
    𝔼 i, f i = 𝔼 i, g i := expect_bijective _ e.bijective f g h

Equality of Averages under Type Equivalence

Informal description

Let $M$ be an additive commutative monoid with scalar multiplication by nonnegative rational numbers, and let $\iota$ and $\kappa$ be finite types. Given an equivalence (bijection) $e \colon \iota \simeq \kappa$ and functions $f \colon \iota \to M$ and $g \colon \kappa \to M$ such that $f(i) = g(e(i))$ for all $i \in \iota$, the average of $f$ over $\iota$ equals the average of $g$ over $\kappa$, i.e., \[ \mathbb{E}_{i \in \iota} f(i) = \mathbb{E}_{j \in \kappa} g(j). \]

Fintype.expect_const theorem

[Nonempty ι] (a : M) : 𝔼 _i : ι, a = a

Full source

lemma expect_const [Nonempty ι] (a : M) : 𝔼 _i : ι, a = a := Finset.expect_const univ_nonempty _

Expectation of Constant Function over Nonempty Finite Type

Informal description

For any nonempty finite type $\iota$ and any element $a$ in an additive commutative monoid $M$ with scalar multiplication by nonnegative rational numbers, the expectation (average) of the constant function $f(i) = a$ over $\iota$ is equal to $a$. That is, \[ \mathbb{E}_{i \in \iota} a = a. \]

Fintype.expect_ite_zero theorem

 (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) (a : M) :
  𝔼 i, ite (p i) a 0 = ite (∃ i, p i) (a /ℚ Fintype.card ι) 0

Full source

lemma expect_ite_zero (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) (a : M) :
    𝔼 i, ite (p i) a 0 = ite (∃ i, p i) (a /ℚ Fintype.card ι) 0 := by
  simp [univ.expect_ite_zero p (by simpa using h)]

Expectation of Indicator Function with Unique Satisfier over Finite Type

Informal description

Let $\iota$ be a finite type, $p$ a decidable predicate on $\iota$, and $a$ an element of an additive commutative monoid $M$ with scalar multiplication by nonnegative rational numbers. Suppose that for any $i, j \in \iota$, if $p(i)$ and $p(j)$ hold, then $i = j$. Then the expectation (average) over $\iota$ of the function $\mathrm{ite}(p(i), a, 0)$ is equal to $\mathrm{ite}(\exists i \in \iota, p(i), a / |\iota|, 0)$, where $|\iota|$ denotes the cardinality of $\iota$.

Fintype.expect_ite_mem theorem

(s : Finset ι) (f : ι → M) : 𝔼 i, (if i ∈ s then f i else 0) = s.dens • 𝔼 i ∈ s, f i

Full source

@[simp] lemma expect_ite_mem (s : Finset ι) (f : ι → M) :
    𝔼 i, (if i ∈ s then f i else 0) = s.dens • 𝔼 i ∈ s, f i := by
  simp [Finset.expect_ite_mem, dens]

Expectation of Restricted Function over Finite Type: $\mathbb{E}_i [\mathbb{1}_{i \in s} f(i)] = \text{dens}(s) \cdot \mathbb{E}_{i \in s} f(i)$

Informal description

Let $\iota$ be a finite type and $s$ a finite subset of $\iota$. For any function $f \colon \iota \to M$, where $M$ is an additive commutative monoid with scalar multiplication by nonnegative rational numbers, the expectation (average) over $\iota$ of the function that equals $f(i)$ when $i \in s$ and zero otherwise is equal to the density of $s$ (i.e., $\frac{|s|}{|\iota|}$) multiplied by the expectation of $f$ over $s$. That is, \[ \mathbb{E}_{i \in \iota} \left( \begin{cases} f(i) & \text{if } i \in s \\ 0 & \text{otherwise} \end{cases} \right) = \left( \frac{|s|}{|\iota|} \right) \cdot \mathbb{E}_{i \in s} f(i). \]

Fintype.expect_dite_eq theorem

(i : ι) (f : ∀ j, i = j → M) : 𝔼 j, (if h : i = j then f j h else 0) = f i rfl /ℚ card ι

Full source

lemma expect_dite_eq (i : ι) (f : ∀ j, i = j → M) :
    𝔼 j, (if h : i = j then f j h else 0) = f i rfl /ℚ card ι := by simp

Expectation of a Dependent Indicator Function over a Finite Type

Informal description

Let $\iota$ be a finite type, and let $f : \forall j, (i = j) \to M$ be a function that depends on a proof of equality with a fixed element $i \in \iota$. The expectation (average) over all elements of $\iota$ of the function that is $f(j)$ when $i = j$ and zero otherwise is equal to $f(i) / \#\iota$, where $\#\iota$ denotes the cardinality of $\iota$.

Fintype.expect_dite_eq' theorem

(i : ι) (f : ∀ j, j = i → M) : 𝔼 j, (if h : j = i then f j h else 0) = f i rfl /ℚ card ι

Full source

lemma expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) :
    𝔼 j, (if h : j = i then f j h else 0) = f i rfl /ℚ card ι := by simp

Expectation of Conditional Function over Finite Type: $\mathbb{E}_j [\mathbb{1}_{j=i} f(j)] = \frac{f(i)}{|\iota|}$

Informal description

For any element $i$ in a finite type $\iota$ and a function $f$ that maps elements $j$ of $\iota$ to a value in an additive commutative monoid $M$ when $j = i$, the expectation (average) over the entire type $\iota$ of the function $\lambda j, \text{if } j = i \text{ then } f j \text{ else } 0$ is equal to $\frac{f i}{|\iota|}$, where $|\iota|$ denotes the cardinality of $\iota$.

Fintype.expect_ite_eq theorem

(i : ι) (f : ι → M) : 𝔼 j, (if i = j then f j else 0) = f i /ℚ card ι

Full source

lemma expect_ite_eq (i : ι) (f : ι → M) :
    𝔼 j, (if i = j then f j else 0) = f i /ℚ card ι := by simp

Expectation of Indicator Function over Finite Type: $\mathbb{E}_j [\mathbb{1}_{i=j} f(j)] = f(i)/|\iota|$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and let $\iota$ be a finite type. For any element $i \in \iota$ and any function $f \colon \iota \to M$, the expectation (average) of the function $\lambda j, \text{if } i = j \text{ then } f(j) \text{ else } 0$ over all elements of $\iota$ is equal to $f(i)/|\iota|$, where $|\iota|$ denotes the cardinality of $\iota$.

Fintype.expect_ite_eq' theorem

(i : ι) (f : ι → M) : 𝔼 j, (if j = i then f j else 0) = f i /ℚ card ι

Full source

lemma expect_ite_eq' (i : ι) (f : ι → M) :
    𝔼 j, (if j = i then f j else 0) = f i /ℚ card ι := by simp

Expectation of Indicator Function over Finite Type: $\mathbb{E}_j [\mathbb{1}_{j=i} f(j)] = f(i)/|\iota|$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, and let $\iota$ be a finite type. For any element $i \in \iota$ and any function $f : \iota \to M$, the expectation (average) of the function $\lambda j, \text{if } j = i \text{ then } f(j) \text{ else } 0$ over all elements of $\iota$ is equal to $f(i) / |\iota|$, where $|\iota|$ denotes the cardinality of $\iota$.

Fintype.expect_one theorem

[Nonempty ι] : 𝔼 _i : ι, (1 : M) = 1

Full source

lemma expect_one [Nonempty ι] : 𝔼 _i : ι, (1 : M) = 1 := expect_const _

Expectation of Constant One Function over Nonempty Finite Type: $\mathbb{E} 1 = 1$

Informal description

For any nonempty finite type $\iota$ and any additive commutative monoid $M$ with scalar multiplication by nonnegative rational numbers, the expectation (average) of the constant function $1$ over $\iota$ is equal to $1$. That is, \[ \mathbb{E}_{i \in \iota} 1 = 1. \]

Fintype.expect_mul_expect theorem

 [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (f : ι → M) (g : κ → M) : (𝔼 i, f i) * 𝔼 j, g j = 𝔼 i, 𝔼 j, f i * g j

Full source

lemma expect_mul_expect [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (f : ι → M)
    (g : κ → M) : (𝔼 i, f i) * 𝔼 j, g j = 𝔼 i, 𝔼 j, f i * g j :=
  Finset.expect_mul_expect ..

Product of Expectations Equals Expectation of Products over Finite Types: $(\mathbb{E} f) * (\mathbb{E} g) = \mathbb{E}_{i,j} (f(i) * g(j))$

Informal description

Let $M$ be an additive commutative monoid with a scalar multiplication by nonnegative rational numbers, where the scalar multiplication satisfies both the tower property and the commutativity property. For any finite types $\iota$ and $\kappa$, and any functions $f \colon \iota \to M$ and $g \colon \kappa \to M$, the following equality holds: $$ \left( \mathbb{E}_{i \in \iota} f(i) \right) * \left( \mathbb{E}_{j \in \kappa} g(j) \right) = \mathbb{E}_{i \in \iota} \mathbb{E}_{j \in \kappa} (f(i) * g(j)), $$ where $\mathbb{E}$ denotes the expectation (average) over the respective finite types.

Mathlib.Algebra.BigOperators.Expect

Notation

Implementation notes

TODO