Proving Dirichlet's test

Stream: general

[Dylan MacKenzie (ecstatic-morse)]

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]

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)]

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)]

This discussion began because I wanted a version of cauchy_seq.const_mul that works on the reals (and briefly forgot that 0 has no multiplicative inverse, because I am dumb). Currently I have:

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.