[Merged by Bors] - feat(Algebra/BigOperators/Order): prod_lt_prod #7844
Conversation
FLDutchmann
added
awaiting-review
| variable [StrictOrderedCommSemiring R] [Nontrivial R] {f : ι → R} {s : Finset ι} | ||
| variable [StrictOrderedCommSemiring R] {f : ι → R} {s : Finset ι} |
There was a problem hiding this comment.
Nontrivial is implied by StrictOrderedCommSemiring
|
|
||
| -- This is also true for an ordered commutative multiplicative monoid with zero | ||
| theorem prod_pos (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i in s, f i := | ||
| prod_induction f (fun x ↦ 0 < x) (fun _ _ ha hb ↦ mul_pos ha hb) zero_lt_one h0 | ||
| #align finset.prod_pos Finset.prod_pos | ||
|
|
||
| theorem prod_lt_prod {t : Finset ℕ} {f g : ℕ → R} (hf : ∀ i ∈ t, 0 < f i) | ||
| (hfg : ∀ i ∈ t, f i ≤ g i) (hlt : ∃ i ∈ t, f i < g i) : | ||
| ∏ i in t, f i < ∏ i in t, g i := by |
There was a problem hiding this comment.
I think this lemma could be a bit more useful as an iff: ∏ i in t, f i < ∏ i in t, g i ↔ ∃ i ∈ t, f i < g i
There was a problem hiding this comment.
I could see this being nicer, but surely we'd want to be consistent with Finset.prod_lt_prod'. In my mind we could either
- Leave it as is
- change
prod_lt_prod'too and fix any breakage - also add this variant as
prod_lt_prod_iff(andprod_lt_prod_iff') - let the two be inconsistent.
In my mind 1 or 3 seem preferable but I'd love to know what others think.
|
|
||
| theorem prod_lt_prod_of_nonempty {t : Finset ℕ} {f g : ℕ → R} (hf : ∀ i ∈ t, 0 < f i) | ||
| (hfg : ∀ i ∈ t, f i < g i) (h_ne : t.Nonempty) : | ||
| ∏ i in t, f i < ∏ i in t, g i := by |
There was a problem hiding this comment.
maybe ∏ i in t, f i < ∏ i in t, g i ↔ t.Nonempty
|
I'm fine with both options 1 and 3. Let's merge this now, and feel free to open a new PR doing 3. bors merge |
github-actions
bot
added
ready-to-merge
Add a product variant of [mul_lt_mul](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Ring/Defs.html#mul_lt_mul), following the pattern of [Finset.prod_lt_prod'](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Order.html#Finset.prod_lt_prod'). This fills in a gap between [Finset.prod_le_prod](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Order.html#Finset.prod_le_prod), [Finset.prod_le_prod'](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Order.html#Finset.prod_le_prod') and [Finset.prod_lt_prod'](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Order.html#Finset.prod_lt_prod').
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Add a product variant of mul_lt_mul, following the pattern of Finset.prod_lt_prod'. This fills in a gap between Finset.prod_le_prod, Finset.prod_le_prod' and Finset.prod_lt_prod'.