Topic: Proving Dirichlet's test
Dylan MacKenzie (ecstatic-morse) (Feb 14 2022 at 22:21):
For some additional context, I've already finished Dirichlet's test in ℂ. I would have put it in
analysis/specific_limits.lean, but trying to import
analysis.complex.basic results in an import cycle. Also, I think I'll have to make it generic over
is_R_or_C to remove the casts from the statement of the alternating series test anyways.
I could state it using
∃ x, tendsto ... instead. Perhaps you're saying it would be easier to prove this way? I chose
cauchy_seq because the alternating series test and Dirichlet's test don't give any information about what the limit actually is, so I assumed you would have to through some analogue of
summable_iff_cauchy_seq_finset for conditionally convergent sums. Is this where I went awry?
Kevin Buzzard (Feb 14 2022 at 22:22):
I think Patrick is asking where you are seeing what you call Dirichlet's test on the UG todo list. Searching for Dirichlet on the UG web page gives nothing. Naming of results is not consistent between different countries.
Dylan MacKenzie (ecstatic-morse) (Feb 14 2022 at 22:26):
Dylan MacKenzie (ecstatic-morse) said:
It's a general form of the alternating series test, which can also be proved in a nicer way. Unlike the alternating series test, it might actually be useful down the line, since its used to prove convergence of Dirichlet series
@Kevin Buzzard I addressed that here. I found the proof for Dirichlet's test was a bit nicer than proving the alternating series test directly. It generated some useful intermediate results, like summation by parts. It's possible that I've made the wrong choice, of course.
Dylan MacKenzie (ecstatic-morse) (Feb 14 2022 at 22:45):
private lemma cauchy_seq.real_const_mul (hf : cauchy_seq f) : cauchy_seq (λ n, x * f n) := uniform_continuous.comp_cauchy_seq real.uniform_continuous_mul_const hf
Heather Macbeth and Patrick Massot suggested that I work around the problem by avoiding
cauchy_seq entirely. This would be a bit of a bummer since I've already finished the proof, but if it leads to something shorter then it's fine.
Last updated: Aug 03 2023 at 10:10 UTC