[Merged by Bors] - feat: bounds on alternating convergent series #10120
Conversation
Parcly-Taxel
added
awaiting-review
|
|
||
| /-- Partial sums of an alternating antitone series with an even number of terms provide | ||
| lower bounds on the limit. -/ | ||
| theorem Antitone.alternating_series_le_tendsto (hfa : Antitone f) (k : ℕ) : |
There was a problem hiding this comment.
You should be able to reduce that to Monotone.tendsto_le_alternating_series applied to -f (and similarly for the next result).
Possibly the intermediate result in the have would make sense as a separate lemma (in all four versions, but with essentially only two proofs).
There was a problem hiding this comment.
I need an extra ContinuousNeg E assumption to go through that route. Indeed the theorems as their preconditions are set up now work even when E = Rat.
|
|
||
|
|
||
| variable {E : Type*} [OrderedRing E] [TopologicalSpace E] [OrderClosedTopology E] | ||
| {l : E} {f : ℕ → E} (hfl : Tendsto (fun n ↦ ∑ i in range n, (-1) ^ i * f i) atTop (𝓝 l)) |
There was a problem hiding this comment.
Prop assumptions like hfl should be mentioned in the theorems, not in the variable line: the reason is that otherwise the file is very hard to understand for the readers, as they don't know which assumptions are used.
sgouezel
added
awaiting-author
Parcly-Taxel
added
awaiting-review
leanprover-community-mathlib4-bot
added
ready-to-merge
|
Build failed (retrying...): |
|
Build failed (retrying...): |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Bounds.20on.20alternating.20convergent.20series/near/418770183