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).
• 𝔼 x, f x 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).

def «term_/ℚ_» : Lean.TrailingParserDescr

Equations

• «term_/ℚ_» = Lean.ParserDescr.trailingNode `term_/ℚ_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /ℚ ") (Lean.ParserDescr.cat `term 0))

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

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

Equations

• Finset.expect s f = (↑s.card)⁻¹ • Finset.sum s f

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).
• 𝔼 x, f x 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} {α : Type u_3} [AddCommMonoid α] [Module ℚ≥0 α] {f : ι → α} [Fintype ι] : (Finset.expect Finset.univ fun (x : ι) => f x) = (↑(Fintype.card ι))⁻¹ • Finset.sum Finset.univ fun (x : ι) => f x

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Finset.expectWith_congr {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f : ι → α} {g : ι → α} (p : ι → Prop) [DecidablePred p] (h : ∀ x ∈ s, p x → f x = g x) : (Finset.expect (Finset.filter (fun (i : ι) => p i) s) fun (i : ι) => f i) = Finset.expect (Finset.filter (fun (i : ι) => p i) s) fun (i : ι) => g i

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

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

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

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

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

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

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

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

See also Finset.expect_boole.

@[simp]

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

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

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

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

theorem Finset.expect_equiv {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f : ι → α} {t : Finset κ} {g : κ → α} (e : ι ≃ κ) (hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : (Finset.expect s fun (i : ι) => f i) = Finset.expect t 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} {α : Type u_3} [AddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {t : Finset κ} (f : ι → κ → α) : (Finset.expect (s ×ˢ t) fun (x : ι × κ) => f x.1 x.2) = Finset.expect s fun (x : ι) => Finset.expect t fun (y : κ) => f x y

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

def Finset.balance {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [Module ℚ≥0 α] [Fintype ι] (f : ι → α) : ι → α

Equations

• Finset.balance f = f - Function.const ι (Finset.expect Finset.univ fun (y : ι) => f y)

theorem Finset.balance_apply {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [Module ℚ≥0 α] [Fintype ι] (f : ι → α) (x : ι) : Finset.balance f x = f x - Finset.expect Finset.univ fun (y : ι) => f y

@[simp]

theorem Finset.balance_zero {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [Module ℚ≥0 α] [Fintype ι] : Finset.balance 0 = 0

@[simp]

theorem Finset.balance_add {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [Module ℚ≥0 α] [Fintype ι] (f : ι → α) (g : ι → α) : Finset.balance (f + g) = Finset.balance f + Finset.balance g

@[simp]

theorem Finset.balance_sub {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [Module ℚ≥0 α] [Fintype ι] (f : ι → α) (g : ι → α) : Finset.balance (f - g) = Finset.balance f - Finset.balance g

@[simp]

theorem Finset.balance_neg {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [Module ℚ≥0 α] [Fintype ι] (f : ι → α) : Finset.balance (-f) = -Finset.balance f

@[simp]

theorem Finset.sum_balance {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [Module ℚ≥0 α] [Fintype ι] (f : ι → α) : (Finset.sum Finset.univ fun (x : ι) => Finset.balance f x) = 0

@[simp]

theorem Finset.expect_balance {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [Module ℚ≥0 α] [Fintype ι] (f : ι → α) : (Finset.expect Finset.univ fun (x : ι) => Finset.balance f x) = 0

@[simp]

theorem Finset.balance_idem {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [Module ℚ≥0 α] [Fintype ι] (f : ι → α) : Finset.balance (Finset.balance f) = Finset.balance f

@[simp]

theorem Finset.map_balance {ι : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommGroup α] [Module ℚ≥0 α] [Field β] [Module ℚ≥0 β] [Fintype ι] {F : Type u_5} [FunLike F α β] [LinearMapClass F ℚ≥0 α β] (g : F) (f : ι → α) (a : ι) : g (Finset.balance f a) = Finset.balance (⇑g ∘ f) a

@[simp]

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

@[simp]

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

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

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

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

theorem Finset.expect_pow {ι : Type u_1} {α : Type u_3} [CommSemiring α] [Module ℚ≥0 α] [IsScalarTower ℚ≥0 α α] [SMulCommClass ℚ≥0 α α] (s : Finset ι) (f : ι → α) (n : ℕ) : (Finset.expect s fun (i : ι) => f i) ^ n = Finset.expect (s^^n) fun (p : Fin n → ι) => Finset.prod Finset.univ fun (i : Fin n) => f (p i)

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

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

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

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

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

Order

theorem Finset.expect_eq_zero_iff_of_nonneg {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) (hf : ∀ i ∈ s, 0 ≤ f i) : (Finset.expect s fun (i : ι) => f i) = 0 ↔ ∀ i ∈ s, f i = 0

theorem Finset.expect_eq_zero_iff_of_nonpos {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) (hf : ∀ i ∈ s, f i ≤ 0) : (Finset.expect s fun (i : ι) => f i) = 0 ↔ ∀ i ∈ s, f i = 0

theorem Finset.expect_le_expect {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f : ι → α} {g : ι → α} [PosSMulMono ℚ≥0 α] (hfg : ∀ i ∈ s, f i ≤ g i) : (Finset.expect s fun (i : ι) => f i) ≤ Finset.expect s fun (i : ι) => g i

theorem GCongr.expect_le_expect {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f : ι → α} {g : ι → α} [PosSMulMono ℚ≥0 α] (h : ∀ i ∈ s, f i ≤ g i) : Finset.expect s f ≤ Finset.expect s g

This is a (beta-reduced) version of the standard lemma Finset.expect_le_expect, convenient for the gcongr tactic.

theorem Finset.expect_le {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} [PosSMulMono ℚ≥0 α] (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, f x ≤ a) : (Finset.expect s fun (i : ι) => f i) ≤ a

theorem Finset.le_expect {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} [PosSMulMono ℚ≥0 α] (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, a ≤ f x) : a ≤ Finset.expect s fun (i : ι) => f i

theorem Finset.expect_nonneg {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f : ι → α} [PosSMulMono ℚ≥0 α] (hf : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ Finset.expect s fun (i : ι) => f i

theorem Finset.le_expect_of_subadditive {ι : Type u_1} {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid α] [Module ℚ≥0 α] [OrderedAddCommMonoid β] [Module ℚ≥0 β] [PosSMulMono ℚ≥0 β] (m : α → β) (h_zero : m 0 = 0) (h_add : ∀ (a b : α), m (a + b) ≤ m a + m b) (h_div : ∀ (a : α) (n : ℕ), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a) (s : Finset ι) (f : ι → α) : m (Finset.expect s fun (i : ι) => f i) ≤ Finset.expect s fun (i : ι) => m (f i)

If m is a subadditive function (m (x + y) ≤ m x + m y, f 1 = 1), and f i, i ∈ s, is a finite family of elements, then m (𝔼 i in s, f i) ≤ 𝔼 i in s, m (f i).

theorem Finset.expect_pos {ι : Type u_1} {α : Type u_3} [OrderedCancelAddCommMonoid α] [Module ℚ≥0 α] {s : Finset ι} {f : ι → α} [PosSMulStrictMono ℚ≥0 α] (hf : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) : 0 < Finset.expect s fun (i : ι) => f i

theorem Finset.abs_expect_le_expect_abs {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [Module ℚ≥0 α] [PosSMulMono ℚ≥0 α] (s : Finset ι) (f : ι → α) : |Finset.expect s fun (i : ι) => f i| ≤ Finset.expect s fun (i : ι) => |f i|

@[simp]

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

theorem Fintype.expect_bijective {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid α] [Module ℚ≥0 α] (e : ι → κ) (he : Function.Bijective e) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : (Finset.expect Finset.univ fun (i : ι) => f i) = Finset.expect Finset.univ 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} {α : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid α] [Module ℚ≥0 α] (e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : (Finset.expect Finset.univ fun (i : ι) => f i) = Finset.expect Finset.univ 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.

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Fintype.expect_eq_zero_iff_of_nonneg {ι : Type u_1} {α : Type u_3} [Fintype ι] [OrderedAddCommMonoid α] [Module ℚ≥0 α] {f : ι → α} [Nonempty ι] (hf : 0 ≤ f) : (Finset.expect Finset.univ fun (i : ι) => f i) = 0 ↔ f = 0

theorem Fintype.expect_eq_zero_iff_of_nonpos {ι : Type u_1} {α : Type u_3} [Fintype ι] [OrderedAddCommMonoid α] [Module ℚ≥0 α] {f : ι → α} [Nonempty ι] (hf : f ≤ 0) : (Finset.expect Finset.univ fun (i : ι) => f i) = 0 ↔ f = 0

@[simp]

theorem RCLike.coe_balance {ι : Type u_1} {α : Type u_3} [RCLike α] [Fintype ι] (f : ι → ℝ) (a : ι) : ↑(Finset.balance f a) = Finset.balance (RCLike.ofReal ∘ f) a

@[simp]

theorem RCLike.coe_comp_balance {ι : Type u_1} {α : Type u_3} [RCLike α] [Fintype ι] (f : ι → ℝ) : RCLike.ofReal ∘ Finset.balance f = Finset.balance (RCLike.ofReal ∘ f)

instance instPosSMulMonoNNRatToSMulToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldInstNNRatLinearOrderedSemifieldInstMulActionNNRatToMonoidToMonoidWithZeroToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringInstNNRatLinearOrderedSemifieldToPreorderToPartialOrderToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToZeroToLinearOrderedCommMonoidWithZeroInstNNRatLinearOrderedCommGroupWithZero {α : Type u_3} [Preorder α] [MulAction ℚ α] [PosSMulMono ℚ α] : PosSMulMono ℚ≥0 α

Equations

• ⋯ = ⋯

instance LinearOrderedSemifield.toPosSMulStrictMono {α : Type u_3} [LinearOrderedSemifield α] : PosSMulStrictMono ℚ≥0 α

Equations

• ⋯ = ⋯

def Mathlib.Meta.Positivity.evalFinsetExpect : Mathlib.Meta.Positivity.PositivityExt