feat(Algebra/Order/BigOperators/Expect): add lemmas and strict variants (#33662)

### Summary

- Combine `le_expect_nonempty_of_subadditive` and `le_expect_of_subadditive` into a single lemma `le_expect_of_subadditive`.
  The extra assumptions `(hs : s.Nonempty)` and `(h_zero : m 0 = 0)` are unnecessary (since `m 0 = 0` follows from `h_div`).
  This requires a small downstream update to `Mathlib/Analysis/RCLike/Basic.lean` (`norm_expect_le`).

- Add strict-inequality variants:
  `expect_lt_expect`, `expect_lt`, `lt_expect`.

- Add existence lemmas:
  `exists_le_of_expect_le_expect`, `exists_le_of_le_expect`, `exists_le_of_expect_le`,
  and `exists_lt_of_expect_lt_expect`.

Author: Pjotr5

Mathlib/Algebra/Order/BigOperators/Expect.lean

@@ -110,10 +110,26 @@ end OrderedAddCommMonoid
 
 section OrderedCancelAddCommMonoid
 variable [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [Module ℚ≥0 α]
-  {s : Finset ι} {f : ι → α}
+  {a : α} {s : Finset ι} {f g : ι → α}
 section PosSMulStrictMono
 variable [PosSMulStrictMono ℚ≥0 α]
 
+lemma expect_lt_expect (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
+    𝔼 i ∈ s, f i < 𝔼 i ∈ s, g i := by
+  apply smul_lt_smul_of_pos_left (sum_lt_sum hle hlt)
+  rw [inv_pos, Nat.cast_pos, card_pos]
+  exact hlt.imp (fun _ => And.left)
+
+lemma expect_lt (hle : ∀ x ∈ s, f x ≤ a) (hlt : ∃ x ∈ s, f x < a) :
+    𝔼 i ∈ s, f i < a := by
+  rw [← expect_const (hlt.imp (fun _ => And.left)) a]
+  exact expect_lt_expect hle hlt
+
+lemma lt_expect (hle : ∀ x ∈ s, a ≤ f x) (hlt : ∃ x ∈ s, a < f x) :
+    a < 𝔼 i ∈ s, f i := by
+  rw [← expect_const (hlt.imp (fun _ => And.left)) a]
+  exact expect_lt_expect hle hlt
+
 lemma expect_pos (hf : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) : 0 < 𝔼 i ∈ s, f i :=
   smul_pos (inv_pos.2 <| mod_cast hs.card_pos) <| sum_pos hf hs
 
@@ -123,7 +139,11 @@ end OrderedCancelAddCommMonoid
 section LinearOrderedAddCommMonoid
 variable [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] [Module ℚ≥0 α]
   [PosSMulMono ℚ≥0 α] {s : Finset ι}
-  {f : ι → α} {a : α}
+  {f g : ι → α} {a : α}
+
+lemma exists_lt_of_expect_lt_expect (h : 𝔼 i ∈ s, g i < 𝔼 i ∈ s, f i) :
+    ∃ x ∈ s, g x < f x := by
+  contrapose! h; exact expect_le_expect h
 
 lemma exists_lt_of_lt_expect (hs : s.Nonempty) (h : a < 𝔼 i ∈ s, f i) : ∃ x ∈ s, a < f x := by
   contrapose! h; exact expect_le hs h
@@ -133,6 +153,24 @@ lemma exists_lt_of_expect_lt (hs : s.Nonempty) (h : 𝔼 i ∈ s, f i < a) : ∃
 
 end LinearOrderedAddCommMonoid
 
+section LinearOrderedCancelAddMonoid
+variable [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [Module ℚ≥0 α]
+  [PosSMulStrictMono ℚ≥0 α] {a : α} {s : Finset ι} {f g : ι → α}
+
+lemma exists_le_of_expect_le_expect (hs : s.Nonempty) (h : 𝔼 i ∈ s, g i ≤ 𝔼 i ∈ s, f i) :
+    ∃ x ∈ s, g x ≤ f x := by
+  obtain ⟨_, hx⟩ := hs
+  contrapose! h
+  exact expect_lt_expect (fun _ hx ↦ le_of_lt (h _ hx)) ⟨_, ⟨hx, h _ hx⟩⟩
+
+lemma exists_le_of_le_expect (hs : s.Nonempty) (h : a ≤ 𝔼 i ∈ s, f i) : ∃ x ∈ s, a ≤ f x :=
+  exists_le_of_expect_le_expect hs (by rwa [expect_const hs _])
+
+lemma exists_le_of_expect_le (hs : s.Nonempty) (h : 𝔼 i ∈ s, f i ≤ a) : ∃ x ∈ s, f x ≤ a :=
+  exists_le_of_expect_le_expect hs (by rwa [expect_const hs _])
+
+end LinearOrderedCancelAddMonoid
+
 section LinearOrderedAddCommGroup
 variable [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Module ℚ≥0 α] [PosSMulMono ℚ≥0 α]