Order properties of the average over a finset #
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)
:
(s.expect fun (i : ι) => f i) ≤ s.expect 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)
:
s.expect f ≤ s.expect 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 ι}
{f : ι → α}
[PosSMulMono ℚ≥0 α]
{a : α}
(hs : s.Nonempty)
(h : ∀ x ∈ s, f x ≤ a)
:
(s.expect fun (i : ι) => f i) ≤ a
theorem
Finset.le_expect
{ι : Type u_1}
{α : Type u_3}
[OrderedAddCommMonoid α]
[Module ℚ≥0 α]
{s : Finset ι}
{f : ι → α}
[PosSMulMono ℚ≥0 α]
{a : α}
(hs : s.Nonempty)
(h : ∀ x ∈ s, a ≤ f x)
:
a ≤ s.expect 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 ≤ s.expect fun (i : ι) => f i
theorem
Finset.le_expect_nonempty_of_subadditive_on_pred
{ι : Type u_1}
{M : Type u_6}
{N : Type u_7}
[AddCommMonoid M]
[Module ℚ≥0 M]
[OrderedAddCommMonoid N]
[Module ℚ≥0 N]
[PosSMulMono ℚ≥0 N]
{m : M → N}
{p : M → Prop}
{f : ι → M}
{s : Finset ι}
(h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b)
(hp_add : ∀ (a b : M), p a → p b → p (a + b))
(h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a)
(hs_nonempty : s.Nonempty)
(hs : ∀ i ∈ s, p (f i))
:
m (s.expect fun (i : ι) => f i) ≤ s.expect fun (i : ι) => m (f i)
Let {a | p a} be an additive subsemigroup of an additive commutative monoid M. If m is a
subadditive function (m (a + b) ≤ m a + m b) preserved under division by a natural, f is a
function valued in that subsemigroup and s is a nonempty set, then
m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i).
theorem
Finset.le_expect_nonempty_of_subadditive
{ι : Type u_1}
{M : Type u_6}
{N : Type u_7}
[AddCommMonoid M]
[Module ℚ≥0 M]
[OrderedAddCommMonoid N]
[Module ℚ≥0 N]
[PosSMulMono ℚ≥0 N]
{f : ι → M}
{s : Finset ι}
(m : M → N)
(h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b)
(h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a)
(hs : s.Nonempty)
:
m (s.expect fun (i : ι) => f i) ≤ s.expect fun (i : ι) => m (f i)
If m : M → N is a subadditive function (m (a + b) ≤ m a + m b) and s is a nonempty set,
then m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i).
theorem
Finset.le_expect_of_subadditive_on_pred
{ι : Type u_1}
{M : Type u_6}
{N : Type u_7}
[AddCommMonoid M]
[Module ℚ≥0 M]
[OrderedAddCommMonoid N]
[Module ℚ≥0 N]
[PosSMulMono ℚ≥0 N]
{m : M → N}
{p : M → Prop}
{f : ι → M}
{s : Finset ι}
(h_zero : m 0 = 0)
(h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b)
(hp_add : ∀ (a b : M), p a → p b → p (a + b))
(h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a)
(hs : ∀ i ∈ s, p (f i))
:
m (s.expect fun (i : ι) => f i) ≤ s.expect fun (i : ι) => m (f i)
Let {a | p a} be a subsemigroup of a commutative monoid M. If m is a subadditive function
(m (x + y) ≤ m x + m y, m 0 = 0) preserved under division by a natural and f is a function
valued in that subsemigroup, then m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i).
theorem
Finset.le_expect_of_subadditive
{ι : Type u_1}
{M : Type u_6}
{N : Type u_7}
[AddCommMonoid M]
[Module ℚ≥0 M]
[OrderedAddCommMonoid N]
[Module ℚ≥0 N]
[PosSMulMono ℚ≥0 N]
{m : M → N}
{f : ι → M}
{s : Finset ι}
(h_zero : m 0 = 0)
(h_add : ∀ (a b : M), m (a + b) ≤ m a + m b)
(h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a)
:
m (s.expect fun (i : ι) => f i) ≤ s.expect fun (i : ι) => m (f i)
If m is a subadditive function (m (x + y) ≤ m x + m y, m 0 = 0) preserved under division
by a natural, then m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ 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 < s.expect fun (i : ι) => f i
theorem
Finset.exists_lt_of_lt_expect
{ι : Type u_1}
{α : Type u_3}
[LinearOrderedAddCommMonoid α]
[Module ℚ≥0 α]
[PosSMulMono ℚ≥0 α]
{s : Finset ι}
{f : ι → α}
{a : α}
(hs : s.Nonempty)
(h : a < s.expect fun (i : ι) => f i)
:
∃ x ∈ s, a < f x
theorem
Finset.exists_lt_of_expect_lt
{ι : Type u_1}
{α : Type u_3}
[LinearOrderedAddCommMonoid α]
[Module ℚ≥0 α]
[PosSMulMono ℚ≥0 α]
{s : Finset ι}
{f : ι → α}
{a : α}
(hs : s.Nonempty)
(h : (s.expect fun (i : ι) => f i) < a)
:
∃ x ∈ s, f x < a
theorem
Finset.abs_expect_le
{ι : Type u_1}
{α : Type u_3}
[LinearOrderedAddCommGroup α]
[Module ℚ≥0 α]
[PosSMulMono ℚ≥0 α]
(s : Finset ι)
(f : ι → α)
:
|s.expect fun (i : ι) => f i| ≤ s.expect fun (i : ι) => |f i|
theorem
Finset.expect_mul_sq_le_sq_mul_sq
{ι : Type u_1}
{R : Type u_5}
[LinearOrderedCommSemiring R]
[ExistsAddOfLE R]
[Module ℚ≥0 R]
[PosSMulMono ℚ≥0 R]
(s : Finset ι)
(f : ι → R)
(g : ι → R)
:
Cauchy-Schwarz inequality in terms of Finset.expect.
Positivity extension for Finset.expect.