From d6e8f57019841d8e750d928247e12f191d76885e Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 31 May 2024 16:06:42 +0200 Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/complexHarmonic.lean | 47 ++++++--------- Nevanlinna/laplace.lean | 7 +-- Nevanlinna/partialDeriv.lean | 103 ++++++++++++++++++++++++++------ 3 files changed, 105 insertions(+), 52 deletions(-) diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index ba399ec..7e6b12c 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -269,36 +269,26 @@ theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpe unfold Complex.laplace intro z hz simp - have : DifferentiableAt ℂ f z := by + have : ∀ z ∈ s, partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by sorry - let ZZ := h z hz - rw [CauchyRiemann₅ 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 Complex.I] + rw [partialDeriv_smul'₂] - -- 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] @@ -399,7 +389,6 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn exact h₁ z - theorem log_normSq_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h₁ : Differentiable ℂ f) diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index e4b56fb..5a9b1ac 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -94,7 +94,7 @@ theorem laplace_add_ContDiffOn rw [add_comm] -theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by +theorem laplace_smul {f : ℂ → F} : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by intro v unfold Complex.laplace rw [partialDeriv_smul₂] @@ -103,11 +103,6 @@ theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Compl rw [partialDeriv_smul₂] simp - exact (partialDeriv_contDiff ℝ h Complex.I).differentiable le_rfl - exact h.differentiable one_le_two - exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl - exact h.differentiable one_le_two - theorem laplace_compContLin {f : ℂ → F} {l : F →L[ℝ] G} (h : ContDiff ℝ 2 f) : Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index 4312e5e..501b1b7 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -30,16 +30,30 @@ theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v rw [map_add] -theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by +theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by unfold partialDeriv - + funext w have : a • f = fun y ↦ a • f y := by rfl rw [this] - - conv => - left - intro w - rw [fderiv_const_smul (h w)] + by_cases ha : a = 0 + · rw [ha] + simp + · by_cases hf : DifferentiableAt 𝕜 f w + · rw [fderiv_const_smul hf] + simp + · have : ¬DifferentiableAt 𝕜 (fun y => a • f y) w := by + by_contra contra + let ZZ := DifferentiableAt.const_smul contra a⁻¹ + have : (fun y => a⁻¹ • a • f y) = f := by + funext i + rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha] + simp + rw [this] at ZZ + exact hf ZZ + simp + rw [fderiv_zero_of_not_differentiableAt hf] + rw [fderiv_zero_of_not_differentiableAt this] + simp theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by @@ -59,8 +73,7 @@ theorem partialDeriv_add₂_differentiableAt {v : E} {x : E} (h₁ : DifferentiableAt 𝕜 f₁ x) - (h₂ : DifferentiableAt 𝕜 f₂ x) - : + (h₂ : DifferentiableAt 𝕜 f₂ x) : partialDeriv 𝕜 v (f₁ + f₂) x = (partialDeriv 𝕜 v f₁) x + (partialDeriv 𝕜 v f₂) x := by unfold partialDeriv @@ -88,6 +101,23 @@ theorem partialDeriv_compContLinAt {f : E → F} {l : F →L[𝕜] G} {v : E} {x simp +theorem partialDeriv_compCLE {f : E → F} {l : F ≃L[𝕜] G} {v : E} : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by + funext x + by_cases hyp : DifferentiableAt 𝕜 f x + · let lCLM : F →L[𝕜] G := l + suffices shyp : partialDeriv 𝕜 v (lCLM ∘ f) x = (lCLM ∘ partialDeriv 𝕜 v f) x from by tauto + apply partialDeriv_compContLinAt + exact hyp + · unfold partialDeriv + rw [fderiv_zero_of_not_differentiableAt] + simp + rw [fderiv_zero_of_not_differentiableAt] + simp + exact hyp + rw [ContinuousLinearEquiv.comp_differentiableAt_iff] + exact hyp + + theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff 𝕜 (n + 1) f) : ∀ v : E, ContDiff 𝕜 n (partialDeriv 𝕜 v f) := by unfold partialDeriv intro v @@ -155,15 +185,54 @@ theorem partialDeriv_eventuallyEq' {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[ section restrictScalars -variable (𝕜 : Type*) [NontriviallyNormedField 𝕜] -variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] -variable [IsScalarTower 𝕜 𝕜' E] -variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] -variable [IsScalarTower 𝕜 𝕜' F] ---variable {f : E → F} +theorem partialDeriv_smul'₂ + (𝕜 : Type*) [NontriviallyNormedField 𝕜] + {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] + {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] + [IsScalarTower 𝕜 𝕜' F] + {f : E → F} {a : 𝕜'} {v : E} : + partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by -theorem partialDeriv_restrictScalars {f : E → F} {v : E} : + funext w + by_cases ha : a = 0 + · unfold partialDeriv + have : a • f = fun y ↦ a • f y := by rfl + rw [this, ha] + simp + · -- Now a is not zero. We present scalar multiplication with a as a continuous linear equivalence. + let smulCLM : F ≃L[𝕜] F := + { + toFun := fun x ↦ a • x + map_add' := fun x y => DistribSMul.smul_add a x y + map_smul' := fun m x => (smul_comm ((RingHom.id 𝕜) m) a x).symm + invFun := fun x ↦ a⁻¹ • x + left_inv := by + intro x + simp + rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha, one_smul] + right_inv := by + intro x + simp + rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul] + continuous_toFun := continuous_const_smul a + continuous_invFun := continuous_const_smul a⁻¹ + } + + have : a • f = smulCLM ∘ f := by tauto + rw [this] + rw [partialDeriv_compCLE] + tauto + + +theorem partialDeriv_restrictScalars + (𝕜 : Type*) [NontriviallyNormedField 𝕜] + {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] + {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] + [IsScalarTower 𝕜 𝕜' E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] + [IsScalarTower 𝕜 𝕜' F] + {f : E → F} {v : E} : Differentiable 𝕜' f → partialDeriv 𝕜 v f = partialDeriv 𝕜' v f := by intro hf unfold partialDeriv