diff --git a/Nevanlinna/cauchyRiemann.lean b/Nevanlinna/cauchyRiemann.lean index 883749d..243ad35 100644 --- a/Nevanlinna/cauchyRiemann.lean +++ b/Nevanlinna/cauchyRiemann.lean @@ -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] diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 12f91c5..ba399ec 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -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 diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index 811806d..e4b56fb 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -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)]