Antiholomorphic functions

Stream: maths

[Yury G. Kudryashov]

Should we generalize (parts of) the HasFDerivAt machinery to allow semilinear maps, so that we can talk about derivatives of antiholomorphic functions?

[Sébastien Gouëzel]

You can already talk about derivatives of antiholomorphic functions, by looking at the real derivative. To me that's the standard way to do things, and it's the way it's done in textbooks. Is that blocking you somewhere?

[Yury G. Kudryashov]

The question is motivated by @David Loeffler 's #34402 but the PR review isn't blocked on this decision.

[Yury G. Kudryashov]

The PR talks about these derivatives using HasFDerivAt over reals, and I thought that having HasFDerivAt with $\sigma$ may be a more natural way to do it.

[Yury G. Kudryashov]

But probably you're right, and we should continue using real derivatives until we're forced to change this (not sure if it will ever happen).

[David Loeffler]

In the PR #34402, it is the real deriv we ultimately need anyway, since the aim is to evaluate the Jacobian in the change-of-variables formula.

[David Loeffler]

(Similar things have come up before in modular forms stuff, see e.g. HasFDerivAt.star_star.)