Complex analysis

Stream: maths

[Yury G. Kudryashov]

I hope that #10000 will be merged in a few days. This means that we can start formalizing complex analysis. Let's coordinate here to avoid duplication of effort.

[Yury G. Kudryashov]

I have a version of the maximum modulus principle in #10978.

[Yury G. Kudryashov]

I see that @Chris Birkbeck is working on modular forms.

[Chris Birkbeck]

Yury G. Kudryashov said:

I hope that #10000 will be merged in a few days. This means that we can start formalizing complex analysis. Let's coordinate here to avoid duplication of effort.

Oh great! The bit that I got working using this was the "uniform limits of holomorphic functions are holomorphic" roughly following the method you described (i.e. commuting the limit and the integral and then using that C.I. define analytic functions). This is in #8979, but its a mess and I wouldn't be surprised if there are much more efficient ways of doing this.

[Chris Birkbeck]

My plan was to split this off into its own PR once #10000 was merged (not that its anywhere near PR ready, but it would be something to work from I guess) .

[Chris Birkbeck]

The next thing on the horizon for modular forms is probably q-expansions. But I wont start on this until I've turned more of this into PR's.

[Heather Macbeth]

Without volunteering to do anything much myself, let me propose that the generalization to several complex variables happen early, so that the development of complex analysis carries this generalization with it. For example, the maximum modulus principle and "uniform limits of holomorphic functions are holomorphic" hold in several complex variables too.

[Yury G. Kudryashov]

#10000 was merged a few minutes ago

[Kevin Buzzard]

Congratulations! How's your marking? ;-)

[Yury G. Kudryashov]

Done.

[Yury G. Kudryashov]

I have a mathematical question motivated by my formalization of the Cauchy integral formula.

docs#complex.has_fpower_series_on_ball_of_differentiable_off_countable shows that a function is analytic on an open disc provided that it is continuous on the corresponding closed disc and is differentiable at all but countably many points of the open disc. I know how to push assumptions to, e.g,, "bounded on a closed ball, continuous at the points of its boundary, and differentiable at all but countably many points of the open ball". This will take several days to formalize and will require a refactor of the Henstock integration code, so I don't want to do it unless I have a reason.

Is this form of the removable discontinuity theorem mathematically interesting? I don't have enough experience in this area to tell. Wikipedia and google say that people know how to remove larger (e.g., Hausdorff 1-dimensional measure zero) sets of singularities of a bounded function provided that this set of singularities is compact. Does anyone care about removing a dense countable set of singularities?

[Sebastien Gouezel]

I don't remember seeing or using anything like that. What comes up much more often is sets with zero analytic capacity, but this is for compact sets, not dense sets, as you mention.

[Yury G. Kudryashov]

Then I'll formalize something else.

[Yury G. Kudryashov]

I have some versions of the Schwarz lemma in branch#YK-schwarz, waiting for #12050