nevanlinna/Nevanlinna/harmonicAt_examples.lean

212 lines
6.8 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
import Nevanlinna.complexHarmonic
import Nevanlinna.holomorphicAt
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F] [CompleteSpace F]
theorem holomorphicAt_is_harmonicAt
{f : → F}
{z : }
(hf : HolomorphicAt f z) :
HarmonicAt f z := by
let t := {x | HolomorphicAt f x}
have ht : IsOpen t := HolomorphicAt_isOpen f
have hz : z ∈ t := by exact hf
constructor
· -- ContDiffAt 2 f z
exact hf.contDiffAt
· -- Δ f =ᶠ[nhds z] 0
apply Filter.eventuallyEq_iff_exists_mem.2
use t
constructor
· exact IsOpen.mem_nhds ht hz
· intro w hw
unfold Complex.laplace
simp
rw [partialDeriv_eventuallyEq hw.CauchyRiemannAt Complex.I]
rw [partialDeriv_smul'₂]
simp
rw [partialDeriv_commAt hw.contDiffAt Complex.I 1]
rw [partialDeriv_eventuallyEq hw.CauchyRiemannAt 1]
rw [partialDeriv_smul'₂]
simp
rw [← smul_assoc]
simp
theorem re_of_holomorphicAt_is_harmonicAr
{f : }
{z : }
(h : HolomorphicAt f z) :
HarmonicAt (Complex.reCLM ∘ f) z := by
apply harmonicAt_comp_CLM_is_harmonicAt
exact holomorphicAt_is_harmonicAt h
theorem im_of_holomorphicAt_is_harmonicAt
{f : }
{z : }
(h : HolomorphicAt f z) :
HarmonicAt (Complex.imCLM ∘ f) z := by
apply harmonicAt_comp_CLM_is_harmonicAt
exact holomorphicAt_is_harmonicAt h
theorem antiholomorphicAt_is_harmonicAt
{f : }
{z : }
(h : HolomorphicAt f z) :
HarmonicAt (Complex.conjCLE ∘ f) z := by
apply harmonicAt_iff_comp_CLE_is_harmonicAt.1
exact holomorphicAt_is_harmonicAt h
theorem log_normSq_of_holomorphicAt_is_harmonicAt
{f : }
{z : }
(h₁f : HolomorphicAt f z)
(h₂f : f z ≠ 0) :
HarmonicAt (Real.log ∘ Complex.normSq ∘ f) z := by
-- For later use
have slitPlaneLemma {z : } (hz : z ≠ 0) : z ∈ Complex.slitPlane -z ∈ Complex.slitPlane := by
rw [Complex.mem_slitPlane_iff, Complex.mem_slitPlane_iff]
simp at hz
rw [Complex.ext_iff] at hz
push_neg at hz
simp at hz
simp
by_contra contra
push_neg at contra
exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2
-- First prove the theorem for functions with image in the slitPlane
have lem₁ : ∀ g : , (HolomorphicAt g z) → (g z ≠ 0) → (g z ∈ Complex.slitPlane) → HarmonicAt (Real.log ∘ Complex.normSq ∘ g) z := by
intro g h₁g h₂g h₃g
-- Rewrite the log |g|² as Complex.log (g * gc)
suffices hyp : HarmonicAt (Complex.log ∘ ((Complex.conjCLE ∘ g) * g)) z from by
have : Real.log ∘ Complex.normSq ∘ g = Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g := by
funext x
simp
rw [this]
have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g = Complex.log ∘ ((Complex.conjCLE ∘ g) * g) := by
funext x
simp
rw [Complex.ofReal_log]
rw [Complex.normSq_eq_conj_mul_self]
exact Complex.normSq_nonneg (g x)
rw [← this] at hyp
apply harmonicAt_comp_CLM_is_harmonicAt hyp
-- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
-- This uses the assumption that g z is in Complex.slitPlane
have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.log ∘ Complex.conjCLE ∘ g + Complex.log ∘ g) := by
apply Filter.eventuallyEq_iff_exists_mem.2
use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
constructor
· apply ContinuousAt.preimage_mem_nhds
· exact h₁g.differentiableAt.continuousAt
· apply IsOpen.mem_nhds
apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
constructor
· exact h₃g
· exact h₂g
· intro x hx
simp
rw [Complex.log_mul_eq_add_log_iff _ hx.2]
rw [Complex.arg_conj]
simp [Complex.slitPlane_arg_ne_pi hx.1]
constructor
· exact Real.pi_pos
· exact Real.pi_nonneg
simp
apply hx.2
-- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
-- This uses the assumption that g z is in Complex.slitPlane
have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.conjCLE ∘ Complex.log ∘ g + Complex.log ∘ g) := by
apply Filter.eventuallyEq_iff_exists_mem.2
use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
constructor
· apply ContinuousAt.preimage_mem_nhds
· exact h₁g.differentiableAt.continuousAt
· apply IsOpen.mem_nhds
apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
constructor
· exact h₃g
· exact h₂g
· intro x hx
simp
rw [← Complex.log_conj]
rw [Complex.log_mul_eq_add_log_iff _ hx.2]
rw [Complex.arg_conj]
simp [Complex.slitPlane_arg_ne_pi hx.1]
constructor
· exact Real.pi_pos
· exact Real.pi_nonneg
simp
apply hx.2
apply Complex.slitPlane_arg_ne_pi hx.1
rw [HarmonicAt_eventuallyEq this]
apply harmonicAt_add_harmonicAt_is_harmonicAt
· rw [← harmonicAt_iff_comp_CLE_is_harmonicAt]
apply holomorphicAt_is_harmonicAt
apply HolomorphicAt_comp
use Complex.slitPlane
constructor
· apply IsOpen.mem_nhds
exact Complex.isOpen_slitPlane
assumption
· exact fun z a => Complex.differentiableAt_log a
exact h₁g
· apply holomorphicAt_is_harmonicAt
apply HolomorphicAt_comp
use Complex.slitPlane
constructor
· apply IsOpen.mem_nhds
exact Complex.isOpen_slitPlane
assumption
· exact fun z a => Complex.differentiableAt_log a
exact h₁g
by_cases h₃f : f z ∈ Complex.slitPlane
· exact lem₁ f h₁f h₂f h₃f
· have : Complex.normSq ∘ f = Complex.normSq ∘ (-f) := by funext; simp
rw [this]
apply lem₁ (-f)
· exact HolomorphicAt_neg h₁f
· simpa
· exact (slitPlaneLemma h₂f).resolve_left h₃f
theorem logabs_of_holomorphicAt_is_harmonic
{f : }
{z : }
(h₁f : HolomorphicAt f z)
(h₂f : f z ≠ 0) :
HarmonicAt (fun w ↦ Real.log ‖f w‖) z := by
-- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
have : (fun z ↦ Real.log ‖f z‖) = (2 : )⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
funext z
simp
unfold Complex.abs
simp
rw [Real.log_sqrt]
rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
exact Complex.normSq_nonneg (f z)
rw [this]
-- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
apply (harmonicAt_iff_smul_const_is_harmonicAt (inv_ne_zero two_ne_zero)).1
exact log_normSq_of_holomorphicAt_is_harmonicAt h₁f h₂f