diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean index 36ce469..30261aa 100644 --- a/Nevanlinna/complexHarmonic.examples.lean +++ b/Nevanlinna/complexHarmonic.examples.lean @@ -138,10 +138,27 @@ theorem log_normSq_of_holomorphicAt_is_harmonicAt apply hx.2 rw [HarmonicAt_eventuallyEq this] + apply harmonicAt_add_harmonicAt_is_harmonicAt + · + sorry + · 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 + + sorry + assumption + + + sorry diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 8acc506..cdd9e9c 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -1,20 +1,4 @@ -import Mathlib.Analysis.Complex.Basic -import Mathlib.Analysis.Complex.TaylorSeries -import Mathlib.Analysis.Calculus.LineDeriv.Basic -import Mathlib.Analysis.Calculus.ContDiff.Defs -import Mathlib.Analysis.Calculus.FDeriv.Basic -import Mathlib.Analysis.Calculus.FDeriv.Symmetric -import Mathlib.Analysis.RCLike.Basic -import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv -import Mathlib.Data.Complex.Module -import Mathlib.Data.Complex.Order -import Mathlib.Data.Complex.Exponential -import Mathlib.Data.Fin.Tuple.Basic -import Mathlib.Topology.Algebra.InfiniteSum.Module -import Mathlib.Topology.Instances.RealVectorSpace -import Nevanlinna.cauchyRiemann import Nevanlinna.laplace -import Nevanlinna.partialDeriv variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁] @@ -162,11 +146,10 @@ theorem harmonicAt_add_harmonicAt_is_harmonicAt HarmonicAt (f₁ + f₂) x := by constructor · exact ContDiffAt.add h₁.1 h₂.1 - · rw [laplace_add_ContDiffAt] - intro z hz - rw [laplace_add_ContDiffOn hs h₁.1 h₂.1 z hz] - rw [h₁.2 z hz, h₂.2 z hz] + · apply Filter.EventuallyEq.trans (laplace_add_ContDiffAt' h₁.1 h₂.1) + apply Filter.EventuallyEq.trans (Filter.EventuallyEq.add h₁.2 h₂.2) simp + rfl theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic f) : diff --git a/Nevanlinna/holomorphic.lean b/Nevanlinna/holomorphic.lean index 7b71167..782c0e2 100644 --- a/Nevanlinna/holomorphic.lean +++ b/Nevanlinna/holomorphic.lean @@ -19,6 +19,7 @@ import Nevanlinna.complexHarmonic variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] +variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace G] def HolomorphicAt (f : E → F) (x : E) : Prop := ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z @@ -59,7 +60,7 @@ theorem HolomorphicAt_differentiableAt theorem HolomorphicAt_isOpen (f : E → F) : IsOpen { x : E | HolomorphicAt f x } := by - + rw [← subset_interior_iff_isOpen] intro x hx simp at hx @@ -78,6 +79,31 @@ theorem HolomorphicAt_isOpen · exact h₂s +theorem HolomorphicAt_comp + {g : E → F} + {f : F → G} + {z : E} + (hf : HolomorphicAt f (g z)) + (hg : HolomorphicAt g z) : + HolomorphicAt (f ∘ g) z := by + obtain ⟨UE, h₁UE, h₂UE⟩ := hg + obtain ⟨UF, h₁UF, h₂UF⟩ := hf + use UE ∩ g⁻¹' UF + constructor + · simp + constructor + · assumption + · apply ContinuousAt.preimage_mem_nhds + apply (h₂UE z (mem_of_mem_nhds h₁UE)).continuousAt + assumption + · intro x hx + apply DifferentiableAt.comp + apply h₂UF + exact hx.2 + apply h₂UE + exact hx.1 + + theorem HolomorphicAt_contDiffAt {f : ℂ → F} {z : ℂ} diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index 64711c5..42f6025 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -1,19 +1,4 @@ -import Mathlib.Data.Fin.Tuple.Basic import Mathlib.Analysis.Complex.Basic -import Mathlib.Analysis.Complex.TaylorSeries -import Mathlib.Analysis.Calculus.LineDeriv.Basic -import Mathlib.Analysis.Calculus.ContDiff.Defs -import Mathlib.Analysis.Calculus.FDeriv.Basic -import Mathlib.Analysis.Calculus.FDeriv.Symmetric -import Mathlib.Data.Complex.Module -import Mathlib.Data.Complex.Order -import Mathlib.Data.Complex.Exponential -import Mathlib.Analysis.RCLike.Basic -import Mathlib.Order.Filter.Basic -import Mathlib.Topology.Algebra.InfiniteSum.Module -import Mathlib.Topology.Basic -import Mathlib.Topology.Instances.RealVectorSpace -import Nevanlinna.cauchyRiemann import Nevanlinna.partialDeriv variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] @@ -169,6 +154,7 @@ theorem laplace_add_ContDiffAt apply fun v ↦ (partialDeriv_contDiffAt ℝ h₁ v).differentiableAt le_rfl apply fun v ↦ (partialDeriv_contDiffAt ℝ h₂ v).differentiableAt le_rfl + theorem laplace_add_ContDiffAt' {f₁ f₂ : ℂ → F} {x : ℂ} @@ -177,49 +163,43 @@ theorem laplace_add_ContDiffAt' Δ (f₁ + f₂) =ᶠ[nhds x] (Δ f₁) + (Δ f₂):= by unfold Complex.laplace - have : partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁) + - (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₂)) = - (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂)) + - (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₂))) := by - group - rw [this] - apply Filter.EventuallyEq.add - suffices hyp : partialDeriv ℝ 1 (partialDeriv ℝ 1 (f₁ + f₂)) =ᶠ[nhds x] partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) + partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂) from by - have : (fun x => partialDeriv ℝ 1 (partialDeriv ℝ 1 (f₁ + f₂)) x) = partialDeriv ℝ 1 (partialDeriv ℝ 1 (f₁ + f₂)) := by - rfl - rw [this] - have : (fun x => (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) + partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂)) x) = (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁)) + (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂)) := by - rfl - rwa [this] - - simp - - have h₁₁ : ContDiffAt ℝ 1 f₁ x := h₁.of_le one_le_two - have h₂₁ : ContDiffAt ℝ 1 f₂ x := h₂.of_le one_le_two - let A : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by - exact partialDeriv_add₂_contDiffAt ℝ h₁₁ h₂₁ - let B : partialDeriv ℝ 1 (partialDeriv ℝ 1 (f₁ + f₂)) =ᶠ[nhds x] (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁)) + (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂)) := by - sorry - - sorry - repeat - rw [partialDeriv_eventuallyEq ℝ (partialDeriv_add₂_contDiffAt ℝ h₁₁ h₂₁)] - rw [partialDeriv_add₂_differentiableAt] - - -- I am super confused at this point because the tactic 'ring' does not work. - -- I do not understand why. So, I need to do things by hand. rw [add_assoc] + nth_rw 5 [add_comm] rw [add_assoc] - rw [add_right_inj (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) x)] - rw [add_comm] - rw [add_assoc] - rw [add_right_inj (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁) x)] - rw [add_comm] + rw [← add_assoc] + + have dualPDeriv : ∀ v : ℂ, partialDeriv ℝ v (partialDeriv ℝ v (f₁ + f₂)) =ᶠ[nhds x] + partialDeriv ℝ v (partialDeriv ℝ v f₁) + partialDeriv ℝ v (partialDeriv ℝ v f₂) := by + + intro v + have h₁₁ : ContDiffAt ℝ 1 f₁ x := h₁.of_le one_le_two + have h₂₁ : ContDiffAt ℝ 1 f₂ x := h₂.of_le one_le_two + + have t₁ : partialDeriv ℝ v (partialDeriv ℝ v (f₁ + f₂)) =ᶠ[nhds x] partialDeriv ℝ v (partialDeriv ℝ v f₁ + partialDeriv ℝ v f₂) := by + exact partialDeriv_eventuallyEq' ℝ (partialDeriv_add₂_contDiffAt ℝ h₁₁ h₂₁) v + + have t₂ : partialDeriv ℝ v (partialDeriv ℝ v f₁ + partialDeriv ℝ v f₂) =ᶠ[nhds x] (partialDeriv ℝ v (partialDeriv ℝ v f₁)) + (partialDeriv ℝ v (partialDeriv ℝ v f₂)) := by + apply partialDeriv_add₂_contDiffAt ℝ + apply partialDeriv_contDiffAt + exact h₁ + apply partialDeriv_contDiffAt + exact h₂ + + apply Filter.EventuallyEq.trans t₁ t₂ + + have eventuallyEq_add + {a₁ a₂ b₁ b₂ : ℂ → F} + (h : a₁ =ᶠ[nhds x] b₁) + (h' : a₂ =ᶠ[nhds x] b₂) : (a₁ + a₂) =ᶠ[nhds x] (b₁ + b₂) := by + have {c₁ c₂ : ℂ → F} : (fun x => c₁ x + c₂ x) = c₁ + c₂ := by rfl + rw [← this, ← this] + exact Filter.EventuallyEq.add h h' + apply eventuallyEq_add + · exact dualPDeriv 1 + · nth_rw 2 [add_comm] + exact dualPDeriv Complex.I - repeat - apply fun v ↦ (partialDeriv_contDiffAt ℝ h₁ v).differentiableAt le_rfl - apply fun v ↦ (partialDeriv_contDiffAt ℝ h₂ v).differentiableAt le_rfl theorem laplace_smul {f : ℂ → F} : ∀ v : ℝ, Δ (v • f) = v • (Δ f) := by intro v diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index 18a1480..d0395b8 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -28,6 +28,16 @@ theorem partialDeriv_eventuallyEq' simp +theorem partialDeriv_eventuallyEq + {f₁ f₂ : E → F} + {x : E} + (h : f₁ =ᶠ[nhds x] f₂) : + ∀ v : E, partialDeriv 𝕜 v f₁ x = partialDeriv 𝕜 v f₂ x := by + unfold partialDeriv + rw [Filter.EventuallyEq.fderiv_eq h] + exact fun v => rfl + + theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by unfold partialDeriv conv => @@ -177,7 +187,12 @@ theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff 𝕜 (n + 1) exact contDiff_const -theorem partialDeriv_contDiffAt {n : ℕ} {f : E → F} {x : E} (h : ContDiffAt 𝕜 (n + 1) f x) : ∀ v : E, ContDiffAt 𝕜 n (partialDeriv 𝕜 v f) x := by +theorem partialDeriv_contDiffAt + {n : ℕ} + {f : E → F} + {x : E} + (h : ContDiffAt 𝕜 (n + 1) f x) : + ∀ v : E, ContDiffAt 𝕜 n (partialDeriv 𝕜 v f) x := by unfold partialDeriv intro v @@ -253,12 +268,6 @@ lemma partialDeriv_fderivAt exact differentiableAt_const a -theorem partialDeriv_eventuallyEq {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) : ∀ v : E, partialDeriv 𝕜 v f₁ x = partialDeriv 𝕜 v f₂ x := by - unfold partialDeriv - rw [Filter.EventuallyEq.fderiv_eq h] - exact fun v => rfl - - section restrictScalars theorem partialDeriv_smul'₂