Hartogs's theorem

Stream: maths

[Junyan Xu]

Yeah, I meant the title of this topic (which you can edit) :)

[Geoffrey Irving]

^ Fixed, in both title and repo. :)

[Geoffrey Irving]

@Reid Barton: To clarify for onlookers, I proved https://en.wikipedia.org/wiki/Hartogs%27s_theorem_on_separate_holomorphicity, not Hartogs's extension theorem.

[Geoffrey Irving]

@Eric Wieser: Ah, alas, I'm on a slightly older version of mathlib that doesn't have continuous_multilinear_map.of_subsingleton. I'll havre to upgrade: last time I tried I went through the complex.abs refactor and got loads of timeouts, and I rolled it back.

[Eric Wieser]

continuous_multilinear_map.of_subsingleton doesn't exist yet, it's in the PR I opened!

[Geoffrey Irving]

^ Aha, I have to upgrade even more then. :)

[Anatole Dedecker]

Eric Wieser said:

I don't see conj_clm anywhere, but suspect we have it

docs#starₗᵢ should work for that

[Eric Wieser]

Do we have the version for continuous but not normed spaces?

[Anatole Dedecker]

I don’t think so, although we have docs#star_continuous_map

[Geoffrey Irving]

The Hartogs' proof is now ported to Lean 4: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Mandelbrot.20-.20Lean.204.20version/near/396156117