done for today

This commit is contained in:
Stefan Kebekus 2024-05-31 10:21:27 +02:00
parent a7b0790675
commit 7a1359308e
3 changed files with 124 additions and 22 deletions

View File

@ -62,3 +62,21 @@ theorem CauchyRiemann₄ {F : Type*} [NormedAddCommGroup F] [NormedSpace F]
right
intro w
rw [DifferentiableAt.fderiv_restrictScalars (h w)]
theorem CauchyRiemann₅ {F : Type*} [NormedAddCommGroup F] [NormedSpace F] {f : → F} {z : } : (DifferentiableAt f z)
→ partialDeriv Complex.I f z = Complex.I • partialDeriv 1 f z := by
intro h
unfold partialDeriv
conv =>
left
rw [DifferentiableAt.fderiv_restrictScalars h]
simp
rw [← mul_one Complex.I]
rw [← smul_eq_mul]
rw [ContinuousLinearMap.map_smul_of_tower (fderiv f z) Complex.I 1]
conv =>
right
right
rw [DifferentiableAt.fderiv_restrictScalars h]

View File

@ -53,13 +53,13 @@ theorem HarmonicOn_congr {f₁ f₂ : → F} {s : Set } (hs : IsOpen s) (
rw [eq_comm]
exact hf₁₂ x hx
· intro z hz
have : f₁ =ᶠ[nhds z] f₂ := by
have : f₁ =ᶠ[nhds z] f₂ := by
unfold Filter.EventuallyEq
unfold Filter.Eventually
simp
refine mem_nhds_iff.mpr ?_
use s
constructor
constructor
· exact hf₁₂
· constructor
· exact hs
@ -72,13 +72,13 @@ theorem HarmonicOn_congr {f₁ f₂ : → F} {s : Set } (hs : IsOpen s) (
intro x hx
exact hf₁₂ x hx
· intro z hz
have : f₁ =ᶠ[nhds z] f₂ := by
have : f₁ =ᶠ[nhds z] f₂ := by
unfold Filter.EventuallyEq
unfold Filter.Eventually
simp
refine mem_nhds_iff.mpr ?_
use s
constructor
constructor
· exact hf₁₂
· constructor
· exact hs
@ -102,10 +102,9 @@ theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : → F} {s : Set
HarmonicOn (f₁ + f₂) s := by
constructor
· exact ContDiffOn.add h₁.1 h₂.1
· rw [laplace_add h₁.1 h₂.1]
simp
intro z
rw [h₁.2 z, h₂.2 z]
· intro z hz
rw [laplace_add_ContDiffOn hs h₁.1 h₂.1 z hz]
rw [h₁.2 z hz, h₂.2 z hz]
simp
@ -177,6 +176,21 @@ theorem harmonic_iff_comp_CLE_is_harmonic {f : → F₁} {l : F₁ ≃L[]
exact harmonic_comp_CLM_is_harmonic
theorem harmonicOn_iff_comp_CLE_is_harmonicOn {f : → F₁} {s : Set } {l : F₁ ≃L[] G₁} (hs : IsOpen s) :
HarmonicOn f s ↔ HarmonicOn (l ∘ f) s := by
constructor
· have : l ∘ f = (l : F₁ →L[] G₁) ∘ f := by rfl
rw [this]
exact harmonicOn_comp_CLM_is_harmonicOn hs
· have : f = (l.symm : G₁ →L[] F₁) ∘ l ∘ f := by
funext z
unfold Function.comp
simp
nth_rewrite 2 [this]
exact harmonicOn_comp_CLM_is_harmonicOn hs
theorem holomorphic_is_harmonic {f : → F₁} (h : Differentiable f) :
Harmonic f := by
@ -233,6 +247,71 @@ theorem holomorphic_is_harmonic {f : → F₁} (h : Differentiable f) :
exact fI_is_real_differentiable
theorem holomorphicOn_is_harmonicOn {f : → F₁} {s : Set } (hs : IsOpen s) (h : DifferentiableOn f s) :
HarmonicOn f s := by
-- f is real C²
have f_is_real_C2 : ContDiffOn 2 f s :=
ContDiffOn.restrict_scalars (DifferentiableOn.contDiffOn h hs)
have fI_is_real_differentiable : DifferentiableOn (partialDeriv 1 f) s := by
intro z hz
apply DifferentiableAt.differentiableWithinAt
let ZZ := (f_is_real_C2 z hz).contDiffAt (IsOpen.mem_nhds hs hz)
let AA := partialDeriv_contDiffAt ZZ 1
exact AA.differentiableAt (by rfl)
constructor
· -- f is two times real continuously differentiable
exact f_is_real_C2
· -- Laplace of f is zero
unfold Complex.laplace
intro z hz
simp
have : DifferentiableAt f z := by
sorry
let ZZ := h z hz
rw [CauchyRiemann₅ this]
-- 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
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₁ :=
{
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
}
-- Bring the goal into a form that is recognized by
-- partialDeriv_compContLin.
have : s • g = sMuls ∘ g := by rfl
rw [this]
rw [partialDeriv_compContLin hg]
rfl
rw [this]
rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
rw [CauchyRiemann₄ h]
rw [this]
rw [← smul_assoc]
simp
-- Subgoals coming from the application of 'this'
-- Differentiable (Real.partialDeriv 1 f)
exact fI_is_real_differentiable
-- Differentiable (Real.partialDeriv 1 f)
exact fI_is_real_differentiable
theorem re_of_holomorphic_is_harmonic {f : } (h : Differentiable f) :
Harmonic (Complex.reCLM ∘ f) := by
apply harmonic_comp_CLM_is_harmonic
@ -294,26 +373,31 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
· exact Real.pi_nonneg
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
exact h₂ z hz
rw [HarmonicOn_congr hs this]
simp
apply harmonic_add_harmonic_is_harmonic
have : Complex.log ∘ ⇑(starRingEnd ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
funext z
apply harmonicOn_add_harmonicOn_is_harmonicOn
exact hs
have : (fun x => Complex.log ((starRingEnd ) (f x))) = (Complex.log ∘ ⇑(starRingEnd ) ∘ f) := by
rfl
rw [this]
have : ∀ z ∈ s, (Complex.log ∘ ⇑(starRingEnd ) ∘ f) z = (Complex.conjCLE ∘ Complex.log ∘ f) z := by
intro z hz
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]
exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
rw [HarmonicOn_congr hs this]
rw [← harmonicOn_iff_comp_CLE_is_harmonicOn]
apply holomorphicOn_is_harmonicOn
intro z
apply DifferentiableAt.comp
exact Complex.differentiableAt_log (h₃ z)
exact h₁ z
repeat
apply holomorphic_is_harmonic
intro z
apply DifferentiableAt.comp
exact Complex.differentiableAt_log (h₃ z)
exact h₁ z
theorem log_normSq_of_holomorphic_is_harmonic

View File

@ -84,7 +84,7 @@ theorem laplace_add_ContDiffOn
rw [partialDeriv_add₂_differentiableAt t₃ t₄]
-- I am super confused at this point because the tactic 'ring' does not work.
-- I do not understand why.
-- I do not understand why. So, I need to do things by hand.
rw [add_assoc]
rw [add_assoc]
rw [add_right_inj (partialDeriv 1 (partialDeriv 1 f₁) x)]