Complex Analysis: Laplacian of modulus of a function

Stream: Is there code for X?

[Jad Abou Hawili]

Given $f(z),g(z) \in H(\Omega)$
where

$$|f(z)|^2 + |g(z)|^2 = 1$$

Determine $f,g$.

The solution goes as follows

$$\nabla^{2} |f(z)|^2 + \nabla^{2} |g(z)|^2 = \nabla^{2} 1$$ $$4|f'(z)|^2 + 4|g'(z)|^2 = 0$$ $$|f'(z)|^2 + |g'(z)|^2 = 0$$ $$|f'(z)|^2 = 0$$ $$f'(z)=0$$ $$f(z) = c$$

(similarly for g)

Im missing several pieces such as the laplacian, laplacian of modulus squared is 4 times the modulus of the derivative. Is this property in mathlib?

The plan is to start from this theorem and build to

$$|f(z)|^2 + |g(z)|^2 = |h(z)|^2$$

then to finally generalize with a sum on both sides, proof for above would also require the fact that if two holomorphic functions agree on a disk/neighborhood then they are equal.

I searched for the laplacian to no avail, i could try to define it on my own but would rather use what's available(if its available).

[Kevin Buzzard]

Can you formalize the question in Lean? I don't even know what $H(\Omega)$ is (and I'm not asking for an explanation, I'm just noting that by far the best way to ask a question here is to ask it in Lean).

[Jeremy Tan]

Kevin Buzzard said:

I don't even know what $H(\Omega)$ is

It must be the space of holomorphic functions over the complexes

[Kevin Buzzard]

In which case I think you're right, there is no Laplacian definition, although it wouldn't surprise me if we had all of the ingredients.

[Eric Wieser]

I have a definition of the laplacian (in the correct generality) locally somewhere...

[Jad Abou Hawili]

Kevin Buzzard said:

Can you formalize the question in Lean? I don't even know what $H(\Omega)$ is (and I'm not asking for an explanation, I'm just noting that by far the best way to ask a question here is to ask it in Lean).

Fair enough

import Mathlib.Data.Complex.Norm
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Topology.Defs.Basic


#check 2=2
variable {z: ℂ}
--variable {h : Norm ℂ}
-- modulus of z ,
#check norm
#check ‖z‖
def constant {c : ℂ} {f : ℂ → ℂ} := ∀ z, f z=c
example (f :  ℂ → ℂ) (g : ℂ → ℂ)
{diff_f : Differentiable ℂ f}
{diff_g : Differentiable ℂ g}
(h : ‖f z‖^2 + ‖g z‖^2  = 1) : ∃(c : ℂ), (∀ (z :ℂ), f z = c) := by

  sorry

[Jad Abou Hawili]

I used Differentiable $\mathbb{C}$ , this should mean holomorphic(correct me if im mistaken, this is the first time i formalize something like this)

[Jad Abou Hawili]

Jeremy Tan said:

Kevin Buzzard said:

I don't even know what $H(\Omega)$ is

It must be the space of holomorphic functions over the complexes

$\Omega$ is open , connected. $H(\Omega)$ means holomorphic over $\Omega$. Didn't mention this because what i really care about is the laplacian, although i guess i should have

[Jad Abou Hawili]

I just took $\mathbb{C}$ here , ill worry about $\Omega$ later.

[Jad Abou Hawili]

Kevin Buzzard said:

In which case I think you're right, there is no Laplacian definition, although it wouldn't surprise me if we had all of the ingredients.

well i wanted to try to use gradient but I couldn't even find the gradient as a vector of partial derivatives, which you would take the dot product of etc... Finding this or the laplacian(general enough to work on $\mathbb{C}$) would be satisfactory.

I'm also thinking of formalizing something simpler first concerning gradients to get the hang of things then do the initial problem.

[Jad Abou Hawili]

I could try and define all this but I'd rather use something already in mathlib(if its there)

[Jad Abou Hawili]

The todo lists partial derivatives, but undergrad lists that partial derivatives commute is done. This is getting confusing...

I dont see what this has to do with partial derivatives(something about line derivatives)

[Eric Wieser]

A previous discussion on the Laplacian: #Is there code for X? > Laplacian @ 💬

[Jad Abou Hawili]

Eric Wieser said:

A previous discussion on the Laplacian: #Is there code for X? > Laplacian @ 💬

Yes, i saw this but it didn't have

$$\nabla^{2} |f(z)|^2 = 4|f'(z)|^2$$

The proof of this involves partial derivatives where

z=x + iy
f(z) = u(x,y) + iv(x,y)
f'(z)=u_x + iv_x

then you take the modulus squared and do the laplacian.

Discussions involving partial derivatives were too technical for me to understand, and it didn't seem like there was anything ready i could use, which spawned this thread.

[Jad Abou Hawili]

I will attempt to play around with the code in that thread, and see if anything comes out of that.

[Kevin Buzzard]

My impression (watching from afar) is that we have all the machinery needed to do lots of differential operators, but very little in terms of concrete differential operators. See also

#mathlib4 > Stating Schrodinger's equation @ 💬

for more Laplacian-related chat.

[Jad Abou Hawili]

Yes, i saw these threads but couldn't really follow along with what was happening.

So i created this to check if anything came out of those discussions and was added to mathlib.

Guess i'll just have to get good, and go through them.