diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index e45212b..8ce9bcd 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -4,12 +4,12 @@ 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.Analysis.RCLike.Basic import Mathlib.Topology.Algebra.InfiniteSum.Module import Mathlib.Topology.Instances.RealVectorSpace import Nevanlinna.cauchyRiemann @@ -254,13 +254,6 @@ theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpe 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 @@ -269,8 +262,6 @@ theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpe unfold Complex.laplace intro z hz simp - have : ∀ z ∈ s, partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by - sorry have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by unfold Filter.EventuallyEq unfold Filter.Eventually @@ -289,17 +280,33 @@ theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpe rw [partialDeriv_eventuallyEq ℝ this Complex.I] rw [partialDeriv_smul'₂] - rw [partialDeriv_comm f_is_real_C2 Complex.I 1] - rw [CauchyRiemann₄ h] + simp + rw [partialDeriv_commOn hs f_is_real_C2 Complex.I 1 z hz] + + have : Complex.I • partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z = Complex.I • (partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z) := by + rfl rw [this] + have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by + unfold Filter.EventuallyEq + unfold Filter.Eventually + simp + refine mem_nhds_iff.mpr ?_ + use s + constructor + · intro x hx + simp + apply CauchyRiemann₅ + apply DifferentiableOn.differentiableAt h + exact IsOpen.mem_nhds hs hx + · constructor + · exact hs + · exact hz + rw [partialDeriv_eventuallyEq ℝ this 1] + rw [partialDeriv_smul'₂] + simp 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) : @@ -367,11 +374,13 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn rw [HarmonicOn_congr hs this] simp - apply harmonicOn_add_harmonicOn_is_harmonicOn - exact hs + apply harmonicOn_add_harmonicOn_is_harmonicOn hs + have : (fun x => Complex.log ((starRingEnd ℂ) (f x))) = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) := by rfl rw [this] + + -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s have : ∀ z ∈ s, (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) z = (Complex.conjCLE ∘ Complex.log ∘ f) z := by intro z hz unfold Function.comp @@ -383,9 +392,24 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn rw [← harmonicOn_iff_comp_CLE_is_harmonicOn] apply holomorphicOn_is_harmonicOn - intro z + exact hs + + intro z hz + apply DifferentiableAt.differentiableWithinAt apply DifferentiableAt.comp - exact Complex.differentiableAt_log (h₃ z) + + + + exact Complex.differentiableAt_log (h₃ z hz) + apply DifferentiableOn.differentiableAt h₁ -- (h₁ z hz) + exact IsOpen.mem_nhds hs hz + exact hs + + -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s + apply holomorphicOn_is_harmonicOn hs + apply? + + exact h₁ z diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index 501b1b7..b2a1b8a 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -1,6 +1,8 @@ import Mathlib.Analysis.Calculus.FDeriv.Basic import Mathlib.Analysis.Calculus.FDeriv.Symmetric import Mathlib.Analysis.Calculus.ContDiff.Basic +import Mathlib.Topology.Basic +import Mathlib.Topology.Defs.Filter variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] @@ -168,6 +170,23 @@ lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff 𝕜 2 f) (z a b : E) : · simp +lemma partialDeriv_fderivOn + {s : Set E} + {f : E → F} + (hs : IsOpen s) + (hf : ContDiffOn 𝕜 2 f s) (a b : E) : + ∀ z ∈ s, fderiv 𝕜 (fderiv 𝕜 f) z b a = partialDeriv 𝕜 b (partialDeriv 𝕜 a f) z := by + + intro z hz + unfold partialDeriv + rw [fderiv_clm_apply] + · simp + · convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz) + apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞) + exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 hf).2 + · 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] @@ -268,3 +287,42 @@ theorem partialDeriv_comm rw [← partialDeriv_fderiv ℝ h z v₂ v₁] rw [derivSymm] rw [partialDeriv_fderiv ℝ h z v₁ v₂] + + +theorem partialDeriv_commOn + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] + {s : Set E} + {f : E → F} + (hs : IsOpen s) + (h : ContDiffOn ℝ 2 f s) : + ∀ v₁ v₂ : E, ∀ z ∈ s, partialDeriv ℝ v₁ (partialDeriv ℝ v₂ f) z = partialDeriv ℝ v₂ (partialDeriv ℝ v₁ f) z := by + + intro v₁ v₂ z hz + + have derivSymm : + (fderiv ℝ (fun w => fderiv ℝ f w) z) v₁ v₂ = (fderiv ℝ (fun w => fderiv ℝ f w) z) v₂ v₁ := by + + let f' := fderiv ℝ f + have h₀ : ∀ y ∈ s, HasFDerivAt f (f' y) y := by + intro y hy + apply DifferentiableAt.hasFDerivAt + apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hy) + apply h.differentiableOn one_le_two + + let f'' := (fderiv ℝ f' z) + have h₁ : HasFDerivAt f' f'' z := by + apply DifferentiableAt.hasFDerivAt + apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz) + apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞) + exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 h).2 + + have h₀' : ∀ᶠ (y : E) in nhds z, HasFDerivAt f (f' y) y := by + apply eventually_nhds_iff.mpr + use s + + exact second_derivative_symmetric_of_eventually h₀' h₁ v₁ v₂ + + rw [← partialDeriv_fderivOn ℝ hs h v₂ v₁ z hz] + rw [derivSymm] + rw [← partialDeriv_fderivOn ℝ hs h v₁ v₂ z hz]