From 4ca5f6d4d23535a8d54997031d62c3c53bee497b Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 29 Jul 2024 15:50:51 +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/holomorphic.examples.lean | 170 ++++++++++++++++++++++++++ Nevanlinna/holomorphic.primitive.lean | 6 +- Nevanlinna/partialDeriv.lean | 6 +- 3 files changed, 179 insertions(+), 3 deletions(-) create mode 100644 Nevanlinna/holomorphic.examples.lean diff --git a/Nevanlinna/holomorphic.examples.lean b/Nevanlinna/holomorphic.examples.lean new file mode 100644 index 0000000..9dd4bbf --- /dev/null +++ b/Nevanlinna/holomorphic.examples.lean @@ -0,0 +1,170 @@ +import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv +import Nevanlinna.complexHarmonic +import Nevanlinna.complexHarmonic +import Nevanlinna.holomorphicAt + + +theorem CauchyRiemann₆ + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] + {f : E → F} + {z : E} : + (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ ∀ e, partialDeriv ℝ (Complex.I • e) f z = Complex.I • partialDeriv ℝ e f z := by + constructor + + · -- Direction "→" + intro h + constructor + · exact DifferentiableAt.restrictScalars ℝ h + · unfold partialDeriv + conv => + intro e + left + rw [DifferentiableAt.fderiv_restrictScalars ℝ h] + simp + rw [← mul_one Complex.I] + rw [← smul_eq_mul] + conv => + intro e + right + right + rw [DifferentiableAt.fderiv_restrictScalars ℝ h] + simp + + · -- Direction "←" + intro ⟨h₁, h₂⟩ + apply (differentiableAt_iff_restrictScalars ℝ h₁).2 + + use { + toFun := fderiv ℝ f z + map_add' := fun x y => ContinuousLinearMap.map_add (fderiv ℝ f z) x y + map_smul' := by + simp + intro m x + have : m = m.re + m.im • Complex.I := by simp + rw [this, add_smul, add_smul, ContinuousLinearMap.map_add] + congr + simp + rw [smul_assoc, smul_assoc, ContinuousLinearMap.map_smul (fderiv ℝ f z) m.2] + congr + exact h₂ x + } + rfl + + +theorem CauchyRiemann₇ + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] + {f : ℂ → F} + {z : ℂ} : + (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by + constructor + · intro hf + constructor + · exact (CauchyRiemann₆.1 hf).1 + · let A := (CauchyRiemann₆.1 hf).2 1 + simp at A + exact A + · intro ⟨h₁, h₂⟩ + apply CauchyRiemann₆.2 + constructor + · exact h₁ + · intro e + have : Complex.I • e = e • Complex.I := by + rw [smul_eq_mul, smul_eq_mul] + exact CommMonoid.mul_comm Complex.I e + rw [this] + have : e = e.re + e.im • Complex.I := by simp + rw [this, add_smul, partialDeriv_add₁, partialDeriv_add₁] + simp + rw [← smul_eq_mul] + have : partialDeriv ℝ ((e.re : ℝ) • Complex.I) f = partialDeriv ℝ ((e.re : ℂ) • Complex.I) f := by rfl + rw [← this, partialDeriv_smul₁ ℝ] + have : (e.re : ℂ) = (e.re : ℝ) • (1 : ℂ) := by simp + rw [this, partialDeriv_smul₁ ℝ] + have : partialDeriv ℝ ((e.im : ℂ) * Complex.I) f = partialDeriv ℝ ((e.im : ℝ) • Complex.I) f := by rfl + rw [this, partialDeriv_smul₁ ℝ] + simp + rw [h₂] + rw [smul_comm] + congr + rw [mul_assoc] + simp + nth_rw 2 [smul_comm] + rw [← smul_assoc] + simp + have : - (e.im : ℂ) = (-e.im : ℝ) • (1 : ℂ) := by simp + rw [this, partialDeriv_smul₁ ℝ] + simp + + + +/- + +A harmonic, real-valued function on ℂ is the real part of a suitable holomorphic function. + +-/ + +theorem harmonic_is_realOfHolomorphic + {f : ℂ → ℝ} + (hf : ∀ z, HarmonicAt f z) : + ∃ F : ℂ → ℂ, ∀ z, (HolomorphicAt F z ∧ ((F z).re = f z)) := by + + let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f) + let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f) + + let g : ℂ → ℂ := f_1 - Complex.I • f_I + + have reg₀ : Differentiable ℝ g := by + let smulICLM : ℂ ≃L[ℝ] ℂ := + { + toFun := fun x ↦ Complex.I • x + map_add' := fun x y => DistribSMul.smul_add Complex.I x y + map_smul' := fun m x => (smul_comm ((RingHom.id ℝ) m) Complex.I x).symm + invFun := fun x ↦ (Complex.I)⁻¹ • x + left_inv := by + intro x + simp + rw [← mul_assoc, mul_comm] + simp + right_inv := by + intro x + simp + rw [← mul_assoc] + simp + continuous_toFun := continuous_const_smul Complex.I + continuous_invFun := continuous_const_smul (Complex.I)⁻¹ + } + + apply Differentiable.sub + apply Differentiable.comp + exact ContinuousLinearMap.differentiable Complex.ofRealCLM + intro z + sorry + apply Differentiable.comp + sorry + sorry + + + have reg₁ : Differentiable ℂ g := by + intro z + apply CauchyRiemann₇.2 + constructor + · exact reg₀ z + · dsimp [g] + have : f_1 - Complex.I • f_I = f_1 + (- Complex.I • f_I) := by + rw [sub_eq_add_neg] + simp + rw [this, partialDeriv_add₂, partialDeriv_add₂] + simp + dsimp [f_1, f_I] + + sorry + sorry + sorry + sorry + sorry + + + + + sorry diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean index d7e3921..c2a67be 100644 --- a/Nevanlinna/holomorphic.primitive.lean +++ b/Nevanlinna/holomorphic.primitive.lean @@ -25,6 +25,7 @@ theorem partialDeriv_compContLinAt rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h] simp + theorem partialDeriv_compCLE {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] @@ -46,6 +47,7 @@ theorem partialDeriv_compCLE rw [ContinuousLinearEquiv.comp_differentiableAt_iff] exact hyp + theorem partialDeriv_smul'₂ {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] @@ -82,6 +84,7 @@ theorem partialDeriv_smul'₂ rw [partialDeriv_compCLE] tauto + theorem CauchyRiemann₄ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} : @@ -104,6 +107,7 @@ theorem CauchyRiemann₄ funext w simp + theorem MeasureTheory.integral2_divergence₃ {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f g : ℝ × ℝ → E) @@ -231,7 +235,6 @@ theorem integral_divergence₅ exact B - noncomputable def primitive {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] : ℂ → (ℂ → E) → (ℂ → E) := by @@ -303,7 +306,6 @@ theorem primitive_fderivAtBasepointZero apply Continuous.add continuity fun_prop - have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by apply Continuous.intervalIntegrable diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index 020aca4..520b6a4 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -38,7 +38,11 @@ theorem partialDeriv_eventuallyEq exact fun v => rfl -theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by +theorem partialDeriv_smul₁ + {f : E → F} + {a : 𝕜} + {v : E} : + partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by unfold partialDeriv conv => left