# Zulip Chat Archive

## Stream: general

### 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):

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.

Last updated: Dec 20 2023 at 11:08 UTC