How many of these topology lemmas are new?

Stream: mathlib4

[Geoffrey Irving]

https://github.com/girving/ray/blob/main/Ray/Misc/Topology.lean contains assorted basic topology lemmas, depending only on mathlib (ignore the dependence on my bound tactic, which is easily removable). I've stripped several that already occurred in mathlib that I'd missed while learning Lean (https://github.com/girving/ray/commit/cfa5fd491e98e174d1ba8ca52b68b726e83f0935), but probably there are a few others already there that I missed.

Would someone be up for doing a quick scan and pointing out other lemmas in this file that already exist? I'm planning to PR these next if they look reasonable, scattered across various topology files, though a bit of cleanup is required (removing dependence on bound, generalizing lemmas as necessary, etc.).

Also feel free to tell me if I skip this "request for scan" step and do the PR directly, though I do expect that means the PR will contain several things that already exist in mathlib.

[Vincent Beffara]

ContinuousOn.bounded is like docs#IsCompact.exists_isMaxOn or docs#IsCompact.exists_forall_ge

[Yaël Dillies]

I would be happy to do a scan but that probably won't happen before sunday.

[Anatole Dedecker]

I’m available to do a scan, but it would indeed be easier if you open a draft PR (no need to put everything in the right file for now) so that I can easily comment

[Yury G. Kudryashov]

Do you want me to replace some of these lemmas by mathlib versions? If yes, would you give me write permission or should I make pull requests?

[Yury G. Kudryashov]

One candidate for removal (not from this file): the atInf filter. It's the same as docs#Bornology.cobounded (if you assume Normed(Add)Group). In the case of a proper set, it's also cocompact. If Mathlib is missing some API about cobounded, then we should add missing lemmas instead of a new definition.

[Geoffrey Irving]

@Yury G. Kudryashov That would certainly be amazing if you're offering, and I'd love to take you up on it if so. Though I think in practice most of the work is going through the remainder of the repo and fixing all the instances. I gave you access, but it may be less work for you either to just point out redundant bits (atInf I did know about, but haven't gotten to removing it) or sending a PR that changes the local file but doesn't fix all the downstream uses. In any of these cases, thank you!

I think there may also be refactoring tricks in Lean + VSCode that I don't know how to use, so if (1) you use these in typical refactoring workflows and (2) there's some documentation of them I'd love to see it. For example, I had Filter.Eventually.self because I hadn't noticed Filter.Eventually.self_of_nhds, but renamed it via perl rather than VSCode.

[Geoffrey Irving]

@Yury G. Kudryashov Let me know if you want to take a pass first, and if not I'll make the super-draft PR for @Anatole Dedecker tomorrow.

[Yury G. Kudryashov]

I'll try to make a first pass later tonight. If I fail (I'm at home with 2 kids, and my wife is away for a week, so can't be sure), then I won't have time till tomorrow evening.

[Yury G. Kudryashov]

Do you intentionally avoid using defeq in lemmas like subset_setOf (it's just Iff.rfl)?

[Yury G. Kudryashov]

I golfed some proofs, often to 1-liners.

[Yury G. Kudryashov]

So that you may decide for yourself whether you want to delete your versions or not.

[Yury G. Kudryashov]

#7913

[Yaël Dillies]

Yury G. Kudryashov said:

I'll try to make a first pass later tonight. If I fail (I'm at home with 2 kids, and my wife is away for a week, so can't be sure), then I won't have time till tomorrow evening.

With appropriate training, that's four more eyes to review Geoffrey's code :grinning_face_with_smiling_eyes:

[Yury G. Kudryashov]

The kids are 5yo and 11yo.

[Kevin Buzzard]

I tried my little nephew on the natural number game but then realised they couldn't type rfl because they didn't know where any of the letters were on the keyboard :-/

[Geoffrey Irving]

@Yury G. Kudryashov That non-use isn’t intentional: some of those lemmas were written quite a while ago before I understood Lean well. Incidentally, that particular lemma is for use in simp, since sometimes applying other simp lemmas results in explicit setOf occurrences; not sure if that’s a separate mistake on my part.

[Yury G. Kudryashov]

Do you have any plans for Hartogs with more than 2 variables?

[Geoffrey Irving]

Yes, will prove that near when I upstream it. I think it follows by currying if we write down the Banach space of holomorphic functions on a set, as my 2 variable version is for any separable Banach space output already. But I haven’t fully checked this.

[Yury G. Kudryashov]

I thought about using docs#torusIntegral and write the series explicitly but I constantly get distracted.

[Geoffrey Irving]

Yeah, I think you’re currently proving Osgood in a lot more generality than me, in which case most of my Osgood.lean would disappear (but Hartogs.lean is still useful).

[Yury G. Kudryashov]

I opened more Mathlib PRs.

[Yury G. Kudryashov]

About Hartogs, I want to prove a version that implies that a compact singularity in dimension ≥2 is removable.

[Geoffrey Irving]

Wow, thank you so much for all the PRs! :heart:

I unfortunately don't know how related that theorem of Hartogs is to the separate holomorphicity one: they're both by Hartogs, but I haven't read the proof of the noncompact singularity theorem.

My guess is that that the best thing for me to do on the upstreaming route is reduce bound to gcongr (https://github.com/girving/ray/blob/main/Ray/Tactic/Bound.lean), since most of my non-topology analysis stuff depends on bound. Does that seem right? The other thing I could try to upstream next is AnalyticManifold, since none of that depends on bound.

[Yury G. Kudryashov]

I'm going to be busy with another project for a week, then I'll have to quickly grade a midterm. About compact singularity theorem (for simplicity, in dimension 2). Consider $f\colon\mathbb C^2\to E$ that is holomorphic in the bidisc of radius 2 outside of the bidisc of radius 1. Let us show that f (a, b) is equal to the iterated Cauchy integral over $S^1\times S^1$ whenever 1 < max |a| |b| < 2. WLOG, 1 < |a| < 2, |b| < 2. We apply Cauchy integral formula for f(a, ⋅) first, then we apply Cauchy integral formula to f(⋅, y) to find each f(a, y), |y|=2 that appears in the first integral. Note that we never used differentiability of f in the bidisc of radius 1. Finally, we know that f is equal to the Cauchy integral on the difference of two bidiscs but this Cauchy integral is analytic everywhere in the larger bidisc.