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 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. This is referred to as expectWith in lemma names.
• 𝔼 (i ∈ s) (j ∈ t), f i j is notation for Finset.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:

1. We don't yet have general convex spaces.
2. 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 over s in the probability theory sense.
• Give a formulation of Jensen's inequality in this language.

def Finset.expect {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (f : ι → M) : M

Average of a function over a finset. If the finset is empty, this is equal to zero.

Equations

• s.expect f = (↑s.card)⁻¹ • ∑ i ∈ s, f i

def BigOperators.bigexpect : Lean.ParserDescr

• 𝔼 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

Equations

• One or more equations did not get rendered due to their size.

def BigOperators.delabFinsetExpect : Lean.PrettyPrinter.Delaborator.Delab

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.

theorem Finset.expect_univ {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {f : ι → M} [Fintype ι] : (univ.expect fun (i : ι) => f i) = (↑(Fintype.card ι))⁻¹ • ∑ i : ι, f i

@[simp]

theorem Finset.expect_empty {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (f : ι → M) : (∅.expect fun (i : ι) => f i) = 0

@[simp]

theorem Finset.expect_singleton {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (f : ι → M) (i : ι) : ({i}.expect fun (j : ι) => f j) = f i

@[simp]

theorem Finset.expect_const_zero {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) : (s.expect fun (_i : ι) => 0) = 0

theorem Finset.expect_congr {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} {f g : ι → M} {t : Finset ι} (hst : s = t) (h : ∀ i ∈ t, f i = g i) : (s.expect fun (i : ι) => f i) = t.expect fun (i : ι) => g i

theorem Finset.expectWith_congr {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s t : Finset ι} {f g : ι → M} {p q : ι → Prop} [DecidablePred p] [DecidablePred q] (hst : s = t) (hpq : ∀ i ∈ t, p i ↔ q i) (h : ∀ i ∈ t, q i → f i = g i) : ({i ∈ s | p i}.expect fun (i : ι) => f i) = {i ∈ t | q i}.expect fun (i : ι) => g i

theorem Finset.expect_sum_comm {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (t : Finset κ) (f : ι → κ → M) : (s.expect fun (i : ι) => ∑ j ∈ t, f i j) = ∑ j ∈ t, s.expect fun (i : ι) => f i j

theorem Finset.expect_comm {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (t : Finset κ) (f : ι → κ → M) : (s.expect fun (i : ι) => t.expect fun (j : κ) => f i j) = t.expect fun (j : κ) => s.expect fun (i : ι) => f i j

theorem Finset.expect_eq_zero {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} {f : ι → M} (h : ∀ i ∈ s, f i = 0) : (s.expect fun (i : ι) => f i) = 0

theorem Finset.exists_ne_zero_of_expect_ne_zero {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} {f : ι → M} (h : (s.expect fun (i : ι) => f i) ≠ 0) : ∃ i ∈ s, f i ≠ 0

theorem Finset.expect_add_distrib {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (f g : ι → M) : (s.expect fun (i : ι) => f i + g i) = (s.expect fun (i : ι) => f i) + s.expect fun (i : ι) => g i

theorem Finset.expect_add_expect_comm {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} (f₁ f₂ g₁ g₂ : ι → M) : ((s.expect fun (i : ι) => f₁ i + f₂ i) + s.expect fun (i : ι) => g₁ i + g₂ i) = (s.expect fun (i : ι) => f₁ i + g₁ i) + s.expect fun (i : ι) => f₂ i + g₂ i

theorem Finset.expect_eq_single_of_mem {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} {f : ι → M} (i : ι) (hi : i ∈ s) (h : ∀ j ∈ s, j ≠ i → f j = 0) : (s.expect fun (i : ι) => f i) = (↑s.card)⁻¹ • f i

theorem Finset.expect_ite_zero {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (p : ι → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : M) : (s.expect fun (i : ι) => if p i then a else 0) = if ∃ i ∈ s, p i then (↑s.card)⁻¹ • a else 0

theorem Finset.expect_ite_mem {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] (s t : Finset ι) (f : ι → M) : (s.expect fun (i : ι) => if i ∈ t then f i else 0) = (↑(s ∩ t).card / ↑s.card) • (s ∩ t).expect fun (i : ι) => f i

@[simp]

theorem Finset.expect_dite_eq {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → M) : (s.expect fun (j : ι) => if h : i = j then f j h else 0) = if i ∈ s then (↑s.card)⁻¹ • f i ⋯ else 0

@[simp]

theorem Finset.expect_dite_eq' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → M) : (s.expect fun (j : ι) => if h : j = i then f j h else 0) = if i ∈ s then (↑s.card)⁻¹ • f i ⋯ else 0

@[simp]

theorem Finset.expect_ite_eq {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} [DecidableEq ι] (i : ι) (f : ι → M) : (s.expect fun (j : ι) => if i = j then f j else 0) = if i ∈ s then (↑s.card)⁻¹ • f i else 0

@[simp]

theorem Finset.expect_ite_eq' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} [DecidableEq ι] (i : ι) (f : ι → M) : (s.expect fun (j : ι) => if j = i then f j else 0) = if i ∈ s then (↑s.card)⁻¹ • f i else 0

theorem Finset.expect_bij {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} {f : ι → M} {t : Finset κ} {g : κ → M} (i : (a : ι) → a ∈ s → κ) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) (h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) (i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ (a : ι) (ha : a ∈ s), i a ha = b) : (s.expect fun (i : ι) => f i) = t.expect fun (i : κ) => g i

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.

theorem Finset.expect_bij' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} {f : ι → M} {t : Finset κ} {g : κ → M} (i : (a : ι) → a ∈ s → κ) (j : (a : κ) → a ∈ t → ι) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) (hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s) (left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) (right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a) (h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) : (s.expect fun (i : ι) => f i) = t.expect fun (i : κ) => g i

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.

theorem Finset.expect_nbij {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} {f : ι → M} {t : Finset κ} {g : κ → M} (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a)) (i_inj : Set.InjOn i ↑s) (i_surj : Set.SurjOn i ↑s ↑t) : (s.expect fun (i : ι) => f i) = t.expect fun (i : κ) => g i

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.

theorem Finset.expect_nbij' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} {f : ι → M} {t : Finset κ} {g : κ → M} (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)) : (s.expect fun (i : ι) => f i) = t.expect fun (i : κ) => g i

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.

theorem Finset.expect_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} {f : ι → M} {t : Finset κ} {g : κ → M} (e : ι ≃ κ) (hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : (s.expect fun (i : ι) => f i) = t.expect fun (i : κ) => g i

Finset.expect_equiv is a specialization of Finset.expect_bij that automatically fills in most arguments.

theorem Finset.expect_product {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (t : Finset κ) (f : ι × κ → M) : ((s ×ˢ t).expect fun (x : ι × κ) => f x) = s.expect fun (i : ι) => t.expect fun (j : κ) => f (i, j)

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

For rewriting in the reverse direction, use Finset.expect_product'.

theorem Finset.expect_product' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (t : Finset κ) (f : ι → κ → M) : ((s ×ˢ t).expect fun (i : ι × κ) => f i.1 i.2) = s.expect fun (i : ι) => t.expect fun (j : κ) => f i j

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

For rewriting in the reverse direction, use Finset.expect_product.

@[simp]

theorem Finset.expect_image {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {f : ι → M} {t : Finset κ} [DecidableEq ι] {m : κ → ι} (hm : Set.InjOn m ↑t) : ((image m t).expect fun (i : ι) => f i) = t.expect fun (i : κ) => f (m i)

@[simp]

theorem Finset.expect_inv_index {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → M) : (s⁻¹.expect fun (i : ι) => f i) = s.expect fun (i : ι) => f i⁻¹

@[simp]

theorem Finset.expect_neg_index {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → M) : ((-s).expect fun (i : ι) => f i) = s.expect fun (i : ι) => f (-i)

theorem map_expect {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [Module ℚ≥0 M] [AddCommMonoid N] [Module ℚ≥0 N] {F : Type u_5} [FunLike F M N] [LinearMapClass F ℚ≥0 M N] (g : F) (f : ι → M) (s : Finset ι) : g (s.expect fun (i : ι) => f i) = s.expect fun (i : ι) => g (f i)

@[simp]

theorem Finset.card_smul_expect {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (f : ι → M) : (s.card • s.expect fun (i : ι) => f i) = ∑ i ∈ s, f i

@[simp]

theorem Fintype.card_smul_expect {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] [Fintype ι] (f : ι → M) : (card ι • Finset.univ.expect fun (i : ι) => f i) = ∑ i : ι, f i

@[simp]

theorem Finset.expect_const {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {s : Finset ι} (hs : s.Nonempty) (a : M) : (s.expect fun (_i : ι) => a) = a

theorem Finset.smul_expect {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] {G : Type u_5} [DistribSMul G M] [SMulCommClass G ℚ≥0 M] (a : G) (s : Finset ι) (f : ι → M) : (a • s.expect fun (i : ι) => f i) = s.expect fun (i : ι) => a • f i

theorem Finset.expect_sub_distrib {ι : Type u_1} {M : Type u_3} [AddCommGroup M] [Module ℚ≥0 M] (s : Finset ι) (f g : ι → M) : (s.expect fun (i : ι) => f i - g i) = (s.expect fun (i : ι) => f i) - s.expect fun (i : ι) => g i

@[simp]

theorem Finset.expect_neg_distrib {ι : Type u_1} {M : Type u_3} [AddCommGroup M] [Module ℚ≥0 M] (s : Finset ι) (f : ι → M) : (s.expect fun (i : ι) => -f i) = -s.expect fun (i : ι) => f i

@[simp]

theorem Finset.card_mul_expect {ι : Type u_1} {M : Type u_3} [Semiring M] [Module ℚ≥0 M] (s : Finset ι) (f : ι → M) : (↑s.card * s.expect fun (i : ι) => f i) = ∑ i ∈ s, f i

@[simp]

theorem Fintype.card_mul_expect {ι : Type u_1} {M : Type u_3} [Semiring M] [Module ℚ≥0 M] [Fintype ι] (f : ι → M) : (↑(card ι) * Finset.univ.expect fun (i : ι) => f i) = ∑ i : ι, f i

theorem Finset.expect_mul {ι : Type u_1} {M : Type u_3} [Semiring M] [Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) : (s.expect fun (i : ι) => f i) * a = s.expect fun (i : ι) => f i * a

theorem Finset.mul_expect {ι : Type u_1} {M : Type u_3} [Semiring M] [Module ℚ≥0 M] [SMulCommClass ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) : (a * s.expect fun (i : ι) => f i) = s.expect fun (i : ι) => a * f i

theorem Finset.expect_mul_expect {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Semiring M] [Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M) : ((s.expect fun (i : ι) => f i) * t.expect fun (j : κ) => g j) = s.expect fun (i : ι) => t.expect fun (j : κ) => f i * g j

theorem Finset.expect_pow {ι : Type u_1} {M : Type u_3} [CommSemiring M] [Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (s : Finset ι) (f : ι → M) (n : ℕ) : (s.expect fun (i : ι) => f i) ^ n = (Fintype.piFinset fun (x : Fin n) => s).expect fun (p : Fin n → ι) => ∏ i : Fin n, f (p i)

theorem Finset.expect_boole_mul {ι : Type u_1} {M : Type u_3} [Semifield M] [CharZero M] [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) : (univ.expect fun (j : ι) => (if i = j then ↑(Fintype.card ι) else 0) * f j) = f i

theorem Finset.expect_boole_mul' {ι : Type u_1} {M : Type u_3} [Semifield M] [CharZero M] [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) : (univ.expect fun (j : ι) => (if j = i then ↑(Fintype.card ι) else 0) * f j) = f i

theorem Finset.expect_eq_sum_div_card {ι : Type u_1} {M : Type u_3} [Semifield M] [CharZero M] (s : Finset ι) (f : ι → M) : (s.expect fun (i : ι) => f i) = (∑ i ∈ s, f i) / ↑s.card

theorem Fintype.expect_eq_sum_div_card {ι : Type u_1} {M : Type u_3} [Semifield M] [CharZero M] [Fintype ι] (f : ι → M) : (Finset.univ.expect fun (i : ι) => f i) = (∑ i : ι, f i) / ↑(card ι)

theorem Finset.expect_div {ι : Type u_1} {M : Type u_3} [Semifield M] [CharZero M] (s : Finset ι) (f : ι → M) (a : M) : (s.expect fun (i : ι) => f i) / a = s.expect fun (i : ι) => f i / a

@[simp]

theorem Finset.expect_apply {ι : Type u_1} {α : Type u_5} {π : α → Type u_6} [(a : α) → CommSemiring (π a)] [(a : α) → Module ℚ≥0 (π a)] (s : Finset ι) (f : ι → (a : α) → π a) (a : α) : s.expect (fun (i : ι) => f i) a = s.expect fun (i : ι) => f i a

@[simp]

theorem algebraMap.coe_expect {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Semifield M] [CharZero M] [Semifield N] [CharZero N] [Algebra M N] (s : Finset ι) (f : ι → M) : ↑(s.expect fun (i : ι) => f i) = s.expect fun (i : ι) => ↑(f i)

theorem Fintype.expect_bijective {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] [Module ℚ≥0 M] (e : ι → κ) (he : Function.Bijective e) (f : ι → M) (g : κ → M) (h : ∀ (i : ι), f i = g (e i)) : (Finset.univ.expect fun (i : ι) => f i) = Finset.univ.expect fun (i : κ) => g i

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

See Function.Bijective.expect_comp for a version without h.

theorem Fintype.expect_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] [Module ℚ≥0 M] (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ (i : ι), f i = g (e i)) : (Finset.univ.expect fun (i : ι) => f i) = Finset.univ.expect fun (i : κ) => g i

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.

theorem Fintype.expect_const {ι : Type u_1} {M : Type u_3} [Fintype ι] [AddCommMonoid M] [Module ℚ≥0 M] [Nonempty ι] (a : M) : (Finset.univ.expect fun (_i : ι) => a) = a

theorem Fintype.expect_ite_zero {ι : Type u_1} {M : Type u_3} [Fintype ι] [AddCommMonoid M] [Module ℚ≥0 M] (p : ι → Prop) [DecidablePred p] (h : ∀ (i j : ι), p i → p j → i = j) (a : M) : (Finset.univ.expect fun (i : ι) => if p i then a else 0) = if ∃ (i : ι), p i then (↑(card ι))⁻¹ • a else 0

@[simp]

theorem Fintype.expect_ite_mem {ι : Type u_1} {M : Type u_3} [Fintype ι] [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] (s : Finset ι) (f : ι → M) : (Finset.univ.expect fun (i : ι) => if i ∈ s then f i else 0) = s.dens • s.expect fun (i : ι) => f i

theorem Fintype.expect_dite_eq {ι : Type u_1} {M : Type u_3} [Fintype ι] [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → M) : (Finset.univ.expect fun (j : ι) => if h : i = j then f j h else 0) = (↑(card ι))⁻¹ • f i ⋯

theorem Fintype.expect_dite_eq' {ι : Type u_1} {M : Type u_3} [Fintype ι] [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → M) : (Finset.univ.expect fun (j : ι) => if h : j = i then f j h else 0) = (↑(card ι))⁻¹ • f i ⋯

theorem Fintype.expect_ite_eq {ι : Type u_1} {M : Type u_3} [Fintype ι] [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] (i : ι) (f : ι → M) : (Finset.univ.expect fun (j : ι) => if i = j then f j else 0) = (↑(card ι))⁻¹ • f i

theorem Fintype.expect_ite_eq' {ι : Type u_1} {M : Type u_3} [Fintype ι] [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] (i : ι) (f : ι → M) : (Finset.univ.expect fun (j : ι) => if j = i then f j else 0) = (↑(card ι))⁻¹ • f i

theorem Fintype.expect_one {ι : Type u_1} {M : Type u_3} [Fintype ι] [Semiring M] [Module ℚ≥0 M] [Nonempty ι] : (Finset.univ.expect fun (_i : ι) => 1) = 1

theorem Fintype.expect_mul_expect {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [Semiring M] [Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (f : ι → M) (g : κ → M) : ((Finset.univ.expect fun (i : ι) => f i) * Finset.univ.expect fun (j : κ) => g j) = Finset.univ.expect fun (i : ι) => Finset.univ.expect fun (j : κ) => f i * g j