feat(Algebra/Order/BigOperators/Expect): add lemmas and strict variants#33662
feat(Algebra/Order/BigOperators/Expect): add lemmas and strict variants#33662Pjotr5 wants to merge 8 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
new-contributor
PR summary 68e18bf8edImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
b-mehta
left a comment
b-mehta
left a comment
There was a problem hiding this comment.
I've left a few preliminary comments, will come back for a more detailed review once those are addressed
| -- TODO: Contribute back better docstring to `le_prod_of_submultiplicative` | ||
| /-- If `m` is a subadditive function (`m (x + y) ≤ m x + m y`, `m 0 = 0`) preserved under division | ||
| /-- If `m` is a subadditive function (`m (x + y) ≤ m x + m y`) preserved under division | ||
| by a natural, then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`. -/ | ||
| lemma le_expect_of_subadditive (h_zero : m 0 = 0) (h_add : ∀ a b, m (a + b) ≤ m a + m b) | ||
| lemma le_expect_of_subadditive (h_add : ∀ a b, m (a + b) ≤ m a + m b) | ||
| (h_div : ∀ (n : ℕ) a, m (a /ℚ n) = m a /ℚ n) : m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i) := | ||
| le_expect_of_subadditive_on_pred (p := fun _ ↦ True) h_zero (by simpa) (by simp) (by simpa) | ||
| (by simp) | ||
| le_expect_of_subadditive_on_pred (p := fun _ ↦ True) (by convert h_div 0 0 <;> simp) | ||
| (by simpa) (by simp) (by simpa) (by simp) |
There was a problem hiding this comment.
Nice catch, although I wonder if this actually means h_div should be stated for n != 0 in le_expect_nonempty_of_subadditive. @YaelDillies I guess you wrote these?
There was a problem hiding this comment.
Implemented the style updates. Regarding h_div: I agree it feels a bit artificial to derive m 0 = 0 from h_div 0 0.
There was a problem hiding this comment.
@Pjotr5 note you can also click on "apply suggestion" on github. This is much easier and automatically resolves the comment.
| 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 |
There was a problem hiding this comment.
| 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 | |
| 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 |
This is what mathlib's style guidelines say, and be sure to make this change below too.
|
|
||
| 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] |
There was a problem hiding this comment.
| rw [←expect_const (hlt.imp (fun _ => And.left)) a] | |
| rw [← expect_const (hlt.imp (fun _ => And.left)) a] |
|
Oh, and sorry for the delay on this one, I think you got an unlucky sequence of assignments! Thanks for your contribution though! |
7 participants
Summary
Combine
le_expect_nonempty_of_subadditiveandle_expect_of_subadditiveinto a single lemmale_expect_of_subadditive.The extra assumptions
(hs : s.Nonempty)and(h_zero : m 0 = 0)are unnecessary (sincem 0 = 0follows fromh_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.