kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Compare commits

base: kebekus:348492cc9452129b494d521d60e7f7f64f613f46
Branches Tags
kebekus:main
kebekus:feature/analyticOn
..
compare: kebekus:71ad6aa67ec7afe25b43532c2493330f2e69ee97
Branches Tags
kebekus:main
kebekus:feature/analyticOn

No commits in common. "348492cc9452129b494d521d60e7f7f64f613f46" and "71ad6aa67ec7afe25b43532c2493330f2e69ee97" have entirely different histories.
348492cc94 ... 71ad6aa67e

2 changed files with 286 additions and 97 deletions
Show Stats Expand all files Collapse all files

2
Nevanlinna/cauchyRiemann.lean
View File

@ -44,7 +44,7 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
simp
theorem CauchyRiemann₄ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} : (Differentiable ℂ f)
theorem CauchyRiemann₄ {f : ℂ → ℂ} : (Differentiable ℂ f)
→ partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
intro h
unfold partialDeriv

381
Nevanlinna/complexHarmonic.lean
View File

@ -26,50 +26,20 @@ def Harmonic (f : ℂ → F) : Prop :=
(ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
Harmonic (f₁ + f₂) := by
constructor
· exact ContDiff.add h₁.1 h₂.1
· rw [laplace_add h₁.1 h₂.1]
simp
intro z
rw [h₁.2 z, h₂.2 z]
simp
theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic f) :
Harmonic (c • f) := by
constructor
· exact ContDiff.const_smul c h.1
· rw [laplace_smul h.1]
dsimp
intro z
rw [h.2 z]
simp
theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c ≠ 0) :
Harmonic f ↔ Harmonic (c • f) := by
constructor
· exact harmonic_smul_const_is_harmonic
· nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)]
exact fun a => harmonic_smul_const_is_harmonic a
theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) :
theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) :
Harmonic (l ∘ f) := by
constructor
· -- Continuous differentiability
apply ContDiff.comp
exact ContinuousLinearMap.contDiff l
exact h.1
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
· rw [laplace_compContLin]
simp
intro z
rw [h.2 z]
simp
exact ContDiff.restrict_scalars ℝ h.1
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} :
@ -79,7 +49,7 @@ theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ]
· have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl
rw [this]
exact harmonic_comp_CLM_is_harmonic
· have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
· have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
funext z
unfold Function.comp
simp
@ -108,17 +78,21 @@ theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
-- This lemma says that partial derivatives commute with complex scalar
-- multiplication. This is a consequence of partialDeriv_compContLin once we
-- note that complex scalar multiplication is continuous ℝ-linear.
have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → F₁, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
intro v s g hg
-- Present scalar multiplication as a continuous ℝ-linear map. This is
-- horrible, there must be better ways to do that.
let sMuls : F₁ →L[ℝ] F₁ :=
let sMuls : ℂ →L[ℝ] ℂ :=
{
toFun := fun x ↦ s • x
map_add' := by exact fun x y => DistribSMul.smul_add s x y
map_smul' := by exact fun m x => (smul_comm ((RingHom.id ℝ) m) s x).symm
cont := continuous_const_smul s
toFun := fun x ↦ s * x
map_add' := by
intro x y
ring
map_smul' := by
intro m x
simp
ring
}
-- Bring the goal into a form that is recognized by
@ -155,12 +129,6 @@ theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ
exact holomorphic_is_harmonic h
theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
Harmonic (Complex.conjCLE ∘ f) := by
apply harmonic_iff_comp_CLE_is_harmonic.1
exact holomorphic_is_harmonic h
theorem log_normSq_of_holomorphic_is_harmonic
{f : ℂ → ℂ}
(h₁ : Differentiable ℂ f)
@ -168,58 +136,151 @@ theorem log_normSq_of_holomorphic_is_harmonic
(h₃ : ∀ z, f z ∈ Complex.slitPlane) :
Harmonic (Real.log ∘ Complex.normSq ∘ f) := by
suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from
(harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f))
suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by
have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by
funext z
simp
rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
rw [Complex.normSq_eq_conj_mul_self]
rw [this]
exact hyp
-- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f)
-- THIS IS WHERE WE USE h₃
have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
unfold Function.comp
funext z
/- We start with a number of lemmas on regularity of all the functions involved -/
-- The norm square is real C²
have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
unfold Complex.normSq
simp
rw [Complex.log_mul_eq_add_log_iff]
conv =>
arg 3
intro x
rw [← Complex.reCLM_apply, ← Complex.imCLM_apply]
apply ContDiff.add
apply ContDiff.mul
apply ContinuousLinearMap.contDiff Complex.reCLM
apply ContinuousLinearMap.contDiff Complex.reCLM
apply ContDiff.mul
apply ContinuousLinearMap.contDiff Complex.imCLM
apply ContinuousLinearMap.contDiff Complex.imCLM
have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
rw [Complex.arg_conj]
have : ¬ Complex.arg (f z) = Real.pi := by
exact Complex.slitPlane_arg_ne_pi (h₃ z)
simp
tauto
rw [this]
-- f is real C²
have f_is_real_C2 : ContDiff ℝ 2 f :=
ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁)
-- Complex.log ∘ f is real C²
have log_f_is_holomorphic : Differentiable ℂ (Complex.log ∘ f) := by
intro z
apply DifferentiableAt.comp
exact Complex.differentiableAt_log (h₃ z)
exact h₁ z
-- Real.log |f|² is real C²
have t₄ : ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f) := by
rw [contDiff_iff_contDiffAt]
intro z
apply ContDiffAt.comp
apply Real.contDiffAt_log.mpr
simp
constructor
· exact Real.pi_pos
· exact Real.pi_nonneg
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
exact h₂ z
rw [this]
apply ContDiff.comp_contDiffAt z normSq_is_real_C2
exact ContDiff.contDiffAt f_is_real_C2
apply harmonic_add_harmonic_is_harmonic
have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
have t₂ : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
funext z
unfold Function.comp
rw [Complex.log_conj]
rfl
exact Complex.slitPlane_arg_ne_pi (h₃ z)
rw [this]
rw [← harmonic_iff_comp_CLE_is_harmonic]
repeat
apply holomorphic_is_harmonic
constructor
· -- logabs f is real C²
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]
have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
exact rfl
rw [this]
apply ContDiff.const_smul
exact t₄
· -- Laplace vanishes
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]
rw [laplace_smul]
simp
have : ∀ (z : ℂ), Complex.laplace (Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 ↔ Complex.laplace (Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 := by
intro z
rw [laplace_compContLin]
simp
-- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
exact t₄
conv =>
intro z
rw [this z]
have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by
unfold Function.comp
funext z
apply Complex.ofReal_log
exact Complex.normSq_nonneg (f z)
rw [this]
have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by
funext z
simp
exact Complex.normSq_eq_conj_mul_self
rw [this]
have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
unfold Function.comp
funext z
simp
rw [Complex.log_mul_eq_add_log_iff]
have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
rw [Complex.arg_conj]
have : ¬ Complex.arg (f z) = Real.pi := by
exact Complex.slitPlane_arg_ne_pi (h₃ z)
simp
tauto
rw [this]
simp
constructor
· exact Real.pi_pos
· exact Real.pi_nonneg
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
exact h₂ z
rw [this]
rw [laplace_add]
rw [t₂, laplace_compCLE]
intro z
apply DifferentiableAt.comp
exact Complex.differentiableAt_log (h₃ z)
exact h₁ z
simp
rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z]
simp
-- ContDiff ℝ 2 (Complex.log ∘ f)
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
-- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f)
rw [t₂]
apply ContDiff.comp
exact ContinuousLinearEquiv.contDiff Complex.conjCLE
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
-- ContDiff ℝ 2 (Complex.log ∘ f)
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
-- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
exact t₄
theorem logabs_of_holomorphic_is_harmonic
@ -229,18 +290,146 @@ theorem logabs_of_holomorphic_is_harmonic
(h₃ : ∀ z, f z ∈ Complex.slitPlane) :
Harmonic (fun z ↦ Real.log ‖f z‖) := by
-- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
/- We start with a number of lemmas on regularity of all the functions involved -/
-- The norm square is real C²
have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
unfold Complex.normSq
simp
conv =>
arg 3
intro x
rw [← Complex.reCLM_apply, ← Complex.imCLM_apply]
apply ContDiff.add
apply ContDiff.mul
apply ContinuousLinearMap.contDiff Complex.reCLM
apply ContinuousLinearMap.contDiff Complex.reCLM
apply ContDiff.mul
apply ContinuousLinearMap.contDiff Complex.imCLM
apply ContinuousLinearMap.contDiff Complex.imCLM
-- f is real C²
have f_is_real_C2 : ContDiff ℝ 2 f :=
ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁)
-- Complex.log ∘ f is real C²
have log_f_is_holomorphic : Differentiable ℂ (Complex.log ∘ f) := by
intro z
apply DifferentiableAt.comp
exact Complex.differentiableAt_log (h₃ z)
exact h₁ z
-- Real.log |f|² is real C²
have t₄ : ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f) := by
rw [contDiff_iff_contDiffAt]
intro z
apply ContDiffAt.comp
apply Real.contDiffAt_log.mpr
simp
exact h₂ z
apply ContDiff.comp_contDiffAt z normSq_is_real_C2
exact ContDiff.contDiffAt f_is_real_C2
have t₂ : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ 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]
unfold Function.comp
rw [Complex.log_conj]
rfl
exact Complex.slitPlane_arg_ne_pi (h₃ z)
-- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1
constructor
· -- logabs f is real C²
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]
exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃
have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
exact rfl
rw [this]
apply ContDiff.const_smul
exact t₄
· -- Laplace vanishes
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]
rw [laplace_smul]
simp
have : ∀ (z : ℂ), Complex.laplace (Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 ↔ Complex.laplace (Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 := by
intro z
rw [laplace_compContLin]
simp
-- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
exact t₄
conv =>
intro z
rw [this z]
have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by
unfold Function.comp
funext z
apply Complex.ofReal_log
exact Complex.normSq_nonneg (f z)
rw [this]
have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by
funext z
simp
exact Complex.normSq_eq_conj_mul_self
rw [this]
have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
unfold Function.comp
funext z
simp
rw [Complex.log_mul_eq_add_log_iff]
have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
rw [Complex.arg_conj]
have : ¬ Complex.arg (f z) = Real.pi := by
exact Complex.slitPlane_arg_ne_pi (h₃ z)
simp
tauto
rw [this]
simp
constructor
· exact Real.pi_pos
· exact Real.pi_nonneg
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
exact h₂ z
rw [this]
rw [laplace_add]
rw [t₂, laplace_compCLE]
intro z
simp
rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z]
simp
-- ContDiff ℝ 2 (Complex.log ∘ f)
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
-- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f)
rw [t₂]
apply ContDiff.comp
exact ContinuousLinearEquiv.contDiff Complex.conjCLE
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
-- ContDiff ℝ 2 (Complex.log ∘ f)
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
-- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
exact t₄