Breaking cycles in `analysis/specific_limits`

Stream: general

[Dylan MacKenzie (ecstatic-morse)]

Is it reasonable to add a dependency on analysis.complex.basic to analysis.specific_limits?

I tried it but it leads to and import cycle, since analysis.complex.basic currently depends on analysis.specific_limits via the following path:

[ "mathlib:analysis.complex.basic",
"mathlib:data.complex.is_R_or_C",
"mathlib:analysis.normed_space.star.basic",
"mathlib:analysis.normed.group.hom",
"mathlib:analysis.specific_limits" ]

This seems wrong. specific_limits feels like it should be a "leaf" in the dependency tree, but data.complex.is_R_or_C seems more fundamental. Do others agree?

[Dylan MacKenzie (ecstatic-morse)]

(I need the fact that \C is a uniform_space for the proof. Otherwise I would import data.complex.basic)

[Dylan MacKenzie (ecstatic-morse)]

Also, the result is about the limit of a product of a real series and a (bounded) complex series. I don't think it's generalizable beyond the complex numbers, but I don't really know. See #general > Proving Dirichlet's test.

[Mario Carneiro]

Well, specific_limits is... unspecific, so it's not a surprise that it is hazardous to dependency management. Probably there are both "leaf" type theorems in there and also basic theorems that are required for some constructions (for example, sum_i 1/x^i ~> 1/(1-x) is needed for things like the construction of the exponential function)

[Mario Carneiro]

we might just need more_specific_limits

[Mario Carneiro]

or come up with a better name

[Dylan MacKenzie (ecstatic-morse)]

One way to break the import cycle is by moving cauchy_series_of_le_geometric'' into a different module. It's the only thing from specific_limits used in normed.group.hom here.

[Dylan MacKenzie (ecstatic-morse)]

I could also just put my stuff in a different module. It's very_specific!

[Dylan MacKenzie (ecstatic-morse)]

data.complex.is_R_or_C also could be changed to not depend on analysis.normed_space.star.basic by moving the instance of cstar_ring elsewhere.

[Dylan MacKenzie (ecstatic-morse)]

I'm going to open a PR with that last idea. In a vacuum, it seems better to have dependencies going from data to analysis rather than vice versa. I know that's not the status quo.

[Dylan MacKenzie (ecstatic-morse)]

#12160

[Yury G. Kudryashov]

I think that we should split specific_limits into a few files. I'll look into this on Monday or Tuesday.

[Dylan MacKenzie (ecstatic-morse)]

My solution doesn't even fix the problem ,since there's a second dependency chain (just learned about import-graph --from ... --to ...):

"analysis.specific_limits"
"topology.metric_space.hausdorff_distance"
"analysis.normed_space.riesz_lemma"
"analysis.normed_space.operator_norm"
"analysis.normed_space.finite_dimension"
"data.complex.is_R_or_C"
"analysis.complex.basic"

[Dylan MacKenzie (ecstatic-morse)]

That one's harder to get rid of.

[Dylan MacKenzie (ecstatic-morse)]

I'll wait for things to get split up. I was told to put things in specific_limits during review, otherwise I wouldn't have tried this hard :stuck_out_tongue:. Presumably one of the submodules will be for results from complex analysis.