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 comnination operator in a convex space. However:

1. We don't yet have general convex spaces.
2. The uniform weights case is a 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.piBinderTypes 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 ι] : (Finset.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 : ι → M} {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 : Finset ι} {t : Finset ι} {f : ι → M} {g : ι → M} {p : ι → Prop} {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) : ((Finset.filter (fun (i : ι) => p i) s).expect fun (i : ι) => f i) = (Finset.filter (fun (i : ι) => q i) t).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 : ι → M) (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₁ : ι → M) (f₂ : ι → M) (g₁ : ι → M) (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 : Finset ι) (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) : ((Finset.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) : (Fintype.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 : ι → M) (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) : (↑(Fintype.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 : ι) : (Finset.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 : ι) : (Finset.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) / ↑(Fintype.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 (↑(Fintype.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) = (↑(Fintype.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) = (↑(Fintype.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) = (↑(Fintype.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) = (↑(Fintype.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