From 9579da6e3938fa0f19b0775a74ba6f5fe90a3fee Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 8 May 2024 15:59:56 +0200 Subject: [PATCH] Define partial over arbitrary fields --- Nevanlinna/cauchyRiemann.lean | 4 +-- Nevanlinna/complexHarmonic.lean | 16 +++++----- Nevanlinna/partialDeriv.lean | 56 ++++++++++++++++++--------------- 3 files changed, 40 insertions(+), 36 deletions(-) diff --git a/Nevanlinna/cauchyRiemann.lean b/Nevanlinna/cauchyRiemann.lean index 08cca7d..1272109 100644 --- a/Nevanlinna/cauchyRiemann.lean +++ b/Nevanlinna/cauchyRiemann.lean @@ -45,9 +45,9 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z) theorem CauchyRiemann₄ {f : ℂ → ℂ} : (Differentiable ℂ f) - → Real.partialDeriv Complex.I f = Complex.I • Real.partialDeriv 1 f := by + → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by intro h - unfold Real.partialDeriv + unfold partialDeriv conv => left diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 568d2c6..8c19276 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -17,10 +17,10 @@ import Nevanlinna.partialDeriv noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by intro f - let fx := Real.partialDeriv 1 f - let fxx := Real.partialDeriv 1 fx - let fy := Real.partialDeriv Complex.I f - let fyy := Real.partialDeriv Complex.I fy + let fx := partialDeriv ℝ 1 f + let fxx := partialDeriv ℝ 1 fx + let fy := partialDeriv ℝ Complex.I f + let fyy := partialDeriv ℝ Complex.I fy exact fxx + fyy @@ -35,8 +35,8 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : have f_is_real_C2 : ContDiff ℝ 2 f := ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) - have fI_is_real_differentiable : Differentiable ℝ (Real.partialDeriv 1 f) := by - exact (partialDeriv_contDiff f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞) + have fI_is_real_differentiable : Differentiable ℝ (partialDeriv ℝ 1 f) := by + exact (partialDeriv_contDiff ℝ f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞) constructor · -- f is two times real continuously differentiable @@ -49,7 +49,7 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : -- 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 : ℂ → ℂ, Differentiable ℝ g → Real.partialDeriv v (s • g) = s • (Real.partialDeriv v g) := by + have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, 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 @@ -71,7 +71,7 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : have : s • g = sMuls ∘ g := by rfl rw [this] - rw [partialDeriv_compContLin hg] + rw [partialDeriv_compContLin ℝ hg] rfl rw [this] diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index 79d11eb..ebed05b 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -10,31 +10,33 @@ import Mathlib.Analysis.Calculus.FDeriv.Linear import Mathlib.Analysis.Calculus.FDeriv.Symmetric variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] -variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] - -noncomputable def Real.partialDeriv : E → (E → F) → (E → F) := - fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v)) +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] +variable (𝕜) -theorem partialDeriv_smul₁ {f : E → F} {a : ℝ} {v : E} : Real.partialDeriv (a • v) f = a • Real.partialDeriv v f := by - unfold Real.partialDeriv +noncomputable def partialDeriv : E → (E → F) → (E → F) := + fun v ↦ (fun f ↦ (fun w ↦ fderiv 𝕜 f w v)) + + +theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by + unfold partialDeriv conv => left intro w rw [map_smul] -theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : Real.partialDeriv (v₁ + v₂) f = (Real.partialDeriv v₁ f) + (Real.partialDeriv v₂ f) := by - unfold Real.partialDeriv +theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v₁ + v₂) f = (partialDeriv 𝕜 v₁ f) + (partialDeriv 𝕜 v₂ f) := by + unfold partialDeriv conv => left intro w rw [map_add] -theorem partialDeriv_smul₂ {f : E → F} {a : ℝ} {v : E} (h : Differentiable ℝ f) : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by - unfold Real.partialDeriv +theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by + unfold partialDeriv have : a • f = fun y ↦ a • f y := by rfl rw [this] @@ -45,8 +47,8 @@ theorem partialDeriv_smul₂ {f : E → F} {a : ℝ} {v : E} (h : Differentiable rw [fderiv_const_smul (h w)] -theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable ℝ f₁) (h₂ : Differentiable ℝ f₂) : Real.partialDeriv v (f₁ + f₂) = (Real.partialDeriv v f₁) + (Real.partialDeriv v f₂) := by - unfold Real.partialDeriv +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 + unfold partialDeriv have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl rw [this] @@ -57,8 +59,8 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable rw [fderiv_add (h₁ w) (h₂ w)] -theorem partialDeriv_compContLin {f : E → F} {l : F →L[ℝ] F} {v : E} (h : Differentiable ℝ f) : Real.partialDeriv v (l ∘ f) = l ∘ Real.partialDeriv v f := by - unfold Real.partialDeriv +theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] F} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by + unfold partialDeriv conv => left @@ -69,14 +71,14 @@ theorem partialDeriv_compContLin {f : E → F} {l : F →L[ℝ] F} {v : E} (h : rfl -theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff ℝ (n + 1) f) : ∀ v : E, ContDiff ℝ n (Real.partialDeriv v f) := by - unfold Real.partialDeriv +theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff 𝕜 (n + 1) f) : ∀ v : E, ContDiff 𝕜 n (partialDeriv 𝕜 v f) := by + unfold partialDeriv intro v let A := (contDiff_succ_iff_fderiv.1 h).right simp at A - have : (fun w => (fderiv ℝ f w) v) = (fun f => f v) ∘ (fun w => (fderiv ℝ f w)) := by + have : (fun w => (fderiv 𝕜 f w) v) = (fun f => f v) ∘ (fun w => (fderiv 𝕜 f w)) := by rfl rw [this] @@ -87,18 +89,21 @@ theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff ℝ (n + 1) exact contDiff_const -lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff ℝ 2 f) (z a b : E) : - fderiv ℝ (fderiv ℝ f) z b a = Real.partialDeriv b (Real.partialDeriv a f) z := by +lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff 𝕜 2 f) (z a b : E) : + fderiv 𝕜 (fderiv 𝕜 f) z b a = partialDeriv 𝕜 b (partialDeriv 𝕜 a f) z := by - unfold Real.partialDeriv + unfold partialDeriv rw [fderiv_clm_apply] · simp · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z · simp -theorem partialDeriv_comm {f : E → F} (h : ContDiff ℝ 2 f) : - ∀ v₁ v₂ : E, Real.partialDeriv v₁ (Real.partialDeriv v₂ f) = Real.partialDeriv v₂ (Real.partialDeriv v₁ f) := by +theorem partialDeriv_comm + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] + {f : E → F} (h : ContDiff ℝ 2 f) : + ∀ v₁ v₂ : E, partialDeriv ℝ v₁ (partialDeriv ℝ v₂ f) = partialDeriv ℝ v₂ (partialDeriv ℝ v₁ f) := by intro v₁ v₂ funext z @@ -118,7 +123,6 @@ theorem partialDeriv_comm {f : E → F} (h : ContDiff ℝ 2 f) : apply second_derivative_symmetric h₀ h₁ v₁ v₂ - - rw [← partialDeriv_fderiv h z v₂ v₁] + rw [← partialDeriv_fderiv ℝ h z v₂ v₁] rw [derivSymm] - rw [partialDeriv_fderiv h z v₁ v₂] + rw [partialDeriv_fderiv ℝ h z v₁ v₂]