Alternative proofs of Liouville's theorem on conformal maps

Stream: maths

[Yourong Zang]

Hello, @Heather Macbeth suggested here that formalizing Liouville's theorem on C^4 conformal maps between Euclidean spaces is doable at the current stage. One elementary proof due to Nevanlinna with this regularity condition does seem approachable, as most of the tools it uses are available in mathlib. However, the proof also relies heavily on solving the differential equations derived from an equation about the inner product of differentials applied on pairs of orthogonal vectors (and also the transcendence of log and arctan functions).

I was wondering if there is a route/argument one can take to bypass the differential equations, or if there exists a more general/abstract linear algebra statement on the differentials of conformal maps that can be used to prove this theorem. Due to my limited understanding of the general picture, I failed to locate any relevant materials or possible solutions. I would be extremely grateful for any input. Thanks in advance.

[Heather Macbeth]

@Yourong Zang I believe you can follow the "standard" proof which works with partial derivatives, just working a little more abstractly with the Frechet derivative and some linear algebra. For example, chapter 3 of the book Inversion theory and conformal mapping, by David Blair.

To be a little more explicit -- I just went through one of the lemmas, annotating how you would change the proof from partial derivatives and a fixed orthonormal basis of $\mathbb{R}^n$ to the Frechet derivative and a real inner product space (no fixed basis). See attached. Blair-lemma-5.1.pdf

I hope this serves as a useful model for the rest of the proof, but feel free to message me with other questions.

[Yourong Zang]

Heather Macbeth said:

Yourong Zang I believe you can follow the "standard" proof which works with partial derivatives, just working a little more abstractly with the Frechet derivative and some linear algebra. For example, chapter 3 of the book Inversion theory and conformal mapping, by David Blair.

To be a little more explicit -- I just went through one of the lemmas, annotating how you would change the proof from partial derivatives and a fixed orthonormal basis of $\mathbb{R}^n$ to the Frechet derivative and a real inner product space (no fixed basis). See attached. Blair-lemma-5.1.pdf

I hope this serves as a useful model for the rest of the proof, but feel free to message me with other questions.

I am extremely grateful for your reply, patience, and the detailed modification. I will definitely try my best on this proof.