[Merged by Bors] - fix(topology/algebra/infinite_sum): remove hard-coding of ℕ and ℝ #6096
Conversation
It may be possible to make these assumptions stricter, but they're weak enough to still cover the original use case.
eric-wieser
added
the
awaiting-review
| @@ -689,6 +703,9 @@ variables {f g : β → α} {a a₁ a₂ : α} | |||
| lemma has_sum_le (h : ∀b, f b ≤ g b) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ := | |||
| le_of_tendsto_of_tendsto' hf hg $ assume s, sum_le_sum $ assume b _, h b | |||
|
|
|||
| @[mono] lemma has_sum_mono (hf : has_sum f a₁) (hg : has_sum g a₂) (h : f ≤ g) : a₁ ≤ a₂ := | |||
There was a problem hiding this comment.
Can you explain what this brings compared to has_sum_le? Same thing for tsum_mono below.
There was a problem hiding this comment.
Consistency with finset.sum_mono, primarily. Also, tsum_strict_mono is elegible for tagging with @[mono], while tsum_lt_tusm is not.
There was a problem hiding this comment.
Then I'd say remove has_sum_le. We don't need two statements saying exactly the same thing modulo a permutation of the arguments, unless there is a very good reason to do so. And maybe rename this one to has_sum.mono, for use with dot notation as @bryangingechen suggests?
There was a problem hiding this comment.
This isn't just an argument permutation, one is stated as ∀b, f b ≤ g b while the other is f ≤ g
There was a problem hiding this comment.
As for dot notation, hf.mono hg h reads a little oddly to me as it doesn't really have the same pattern as hf.add hg, but I'll let you decide.
There was a problem hiding this comment.
Yes, it's defeq for ≤, but not defeq for <. I think we should keep the API for ≤ and < the same as each other for discoverability - but I wouldn't object to dropping the quantified versions of the lemmas entirely.
sgouezel
added
awaiting-author
| @@ -689,6 +703,9 @@ variables {f g : β → α} {a a₁ a₂ : α} | |||
| lemma has_sum_le (h : ∀b, f b ≤ g b) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ := | |||
| le_of_tendsto_of_tendsto' hf hg $ assume s, sum_le_sum $ assume b _, h b | |||
|
|
|||
| @[mono] lemma has_sum_mono (hf : has_sum f a₁) (hg : has_sum g a₂) (h : f ≤ g) : a₁ ≤ a₂ := | |||
There was a problem hiding this comment.
This for a later PR, but it looks like some more of the lemmas in this section could be renamed to let us take advantage of dot notation.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
| lemma has_sum.update (hf : has_sum f a₁) (b : β) [decidable_eq β] (a : α) : | ||
| has_sum (update f b a) (a - f b + a₁) := | ||
| begin | ||
| convert ((has_sum_ite_eq b _).add hf), |
There was a problem hiding this comment.
Probably function.update_apply can help with golfing here.
There was a problem hiding this comment.
I get stuck on a goal ite (b' = b) a (f b') = ite (b' = b) (a - f b + f b') (f b'), which isn't really any easier to resolve than the way I currently tackle the original goal.
eric-wieser
added
awaiting-review
|
ok, let's merge it like that and change names later if needed. |
github-actions
bot
added
ready-to-merge
) It may be possible to make these assumptions stricter, but they're weak enough to still cover the original use case. Hopefully that can be handled by @alexjbest's upcoming linter to relax assumptions.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
) It may be possible to make these assumptions stricter, but they're weak enough to still cover the original use case. Hopefully that can be handled by @alexjbest's upcoming linter to relax assumptions.
It may be possible to make these assumptions stricter, but they're weak enough to still cover the original use case.
Hopefully that can be handled by @alexjbest's upcoming linter to relax assumptions.
This PR is follow-up to @adomani's #6017