Documentation

Mathlib.Algebra.BigOperators.Expect

Average over a finset #

This file defines Finset.expect, the average (aka expectation) of a function over a finset.

Notation #

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 #

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

          Delaborator for Finset.expect. The pp.funBinderTypes option controls whether to show the domain type when the expect is over Finset.univ.

          Equations
            Instances For
              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 : it, 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 : it, p i q i) (h : it, q if i = g i) :
              ({is | p i}.expect fun (i : ι) => f i) = {it | 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 : ι) => jt, f i j) = jt, 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 : is, 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) :
              is, 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 : js, j if 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 : is, js, p ip ji = j) (a : M) :
              (s.expect fun (i : ι) => if p i then a else 0) = if is, 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 = jM) :
              (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 = iM) :
              (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 : bt, ∃ (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 : as, i a t) (h : as, 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 : as, i a t) (hj : at, j a s) (left_inv : as, j (i a) = a) (right_inv : at, i (j a) = a) (h : as, 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 : is, 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) = is, 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) = is, 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) = (∑ is, 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 ip ji = 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 = jM) :
              (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 = iM) :
              (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