theorem Finset.expect_lt_expect {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [Module ℚ≥0 M] [PosSMulStrictMono ℚ≥0 M] {s : Finset ι} {f g : ι → M} (hfg : ∀ i ∈ s, f i ≤ g i) (hfg' : ∃ i ∈ s, f i < g i) : (s.expect fun (i : ι) => f i) < s.expect fun (i : ι) => g i

theorem Finset.expect_pos' {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [Module ℚ≥0 M] [PosSMulStrictMono ℚ≥0 M] {s : Finset ι} {f : ι → M} (h : ∀ i ∈ s, 0 ≤ f i) (hs : ∃ i ∈ s, 0 < f i) : 0 < s.expect fun (i : ι) => f i