Compare commits

..

3 Commits

Author SHA1 Message Date
Stefan Kebekus dd207b19a2 working… 2024-07-30 16:45:26 +02:00
Stefan Kebekus 8d100b2333 working… 2024-07-30 15:11:57 +02:00
Stefan Kebekus 1d27eeb66b Working. 2024-07-30 14:11:39 +02:00
2 changed files with 116 additions and 18 deletions

View File

@ -1,4 +1,3 @@
import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
import Nevanlinna.complexHarmonic import Nevanlinna.complexHarmonic
import Nevanlinna.holomorphicAt import Nevanlinna.holomorphicAt
import Nevanlinna.holomorphic_primitive import Nevanlinna.holomorphic_primitive
@ -107,7 +106,7 @@ A harmonic, real-valued function on is the real part of a suitable holomorph
theorem harmonic_is_realOfHolomorphic theorem harmonic_is_realOfHolomorphic
{f : } {f : }
(hf : ∀ z, HarmonicAt f z) : (hf : ∀ z, HarmonicAt f z) :
∃ F : , ∀ z, (HolomorphicAt F z ∧ ((F z).re = f z)) := by ∃ F : , ∀ z, HolomorphicAt F z ∧ (Complex.reCLM ∘ F = f) := by
let f_1 : := Complex.ofRealCLM ∘ (partialDeriv 1 f) let f_1 : := Complex.ofRealCLM ∘ (partialDeriv 1 f)
let f_I : := Complex.ofRealCLM ∘ (partialDeriv Complex.I f) let f_I : := Complex.ofRealCLM ∘ (partialDeriv Complex.I f)
@ -194,20 +193,64 @@ theorem harmonic_is_realOfHolomorphic
apply Differentiable.const_smul apply Differentiable.const_smul
exact reg₁f_I.differentiable le_rfl exact reg₁f_I.differentiable le_rfl
let F := primitive 0 g let F := fun z ↦ (primitive 0 g) z + f 0
have regF : Differentiable F := by
apply Differentiable.add
apply primitive_differentiable reg₁
simp
have pF'' : ∀ x, (fderiv F x) = ContinuousLinearMap.lsmul (g x) := by
intro x
rw [DifferentiableAt.fderiv_restrictScalars (regF x)]
dsimp [F]
rw [fderiv_add_const]
rw [primitive_fderiv']
exact rfl
exact reg₁
use F use F
intro z intro z
constructor constructor
· -- HolomorphicAt F z · -- HolomorphicAt F z
apply HolomorphicAt_iff.2 apply HolomorphicAt_iff.2
use {z : | true} use Set.univ
constructor constructor
· exact isOpen_const · exact isOpen_const
· constructor · constructor
· simp · simp
· intro w hw · intro w _
let A : HasDerivAt (primitive 0 g) (g w) w := primitive_fderiv g reg₁ exact regF w
apply A.differentiableAt
· -- (F z).re = f z · -- (F z).re = f z
have A := reg₂f.differentiable one_le_two
have B : Differentiable (Complex.reCLM ∘ F) := by
apply Differentiable.comp
exact ContinuousLinearMap.differentiable Complex.reCLM
exact Differentiable.restrictScalars regF
have C : (F 0).re = f 0 := by
dsimp [F]
rw [primitive_zeroAtBasepoint]
simp
apply eq_of_fderiv_eq B A _ 0 C
intro x
rw [fderiv.comp]
simp
apply ContinuousLinearMap.ext
intro w
simp
rw [pF'']
dsimp [g, f_1, f_I, partialDeriv]
simp
have : w = w.re • 1 + w.im • Complex.I := by simp
nth_rw 3 [this]
rw [(fderiv f x).map_add]
rw [(fderiv f x).map_smul, (fderiv f x).map_smul]
rw [smul_eq_mul, smul_eq_mul]
ring
-- DifferentiableAt (⇑Complex.reCLM) (F x)
fun_prop
-- DifferentiableAt F x
exact regF.restrictScalars x
sorry

View File

@ -485,11 +485,11 @@ theorem primitive_translation
simp simp
theorem primitive_fderivAtBasepoint theorem primitive_hasDerivAtBasepoint
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{z₀ : } {f : → E}
(f : → E) (hf : Continuous f)
(hf : Continuous f) : (z₀ : ) :
HasDerivAt (primitive z₀ f) (f z₀) z₀ := by HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
let g := f ∘ fun z ↦ z + z₀ let g := f ∘ fun z ↦ z + z₀
@ -597,15 +597,70 @@ theorem primitive_additivity
abel abel
theorem primitive_fderiv theorem primitive_hasDerivAt
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{z₀ z : } {f : → E}
(f : → E) (hf : Differentiable f)
(hf : Differentiable f) : (z₀ z : ) :
HasDerivAt (primitive z₀ f) (f z) z := by HasDerivAt (primitive z₀ f) (f z) z := by
rw [primitive_additivity f hf z₀ z] rw [primitive_additivity f hf z₀ z]
rw [← add_zero (f z)] rw [← add_zero (f z)]
apply HasDerivAt.add apply HasDerivAt.add
apply primitive_fderivAtBasepoint apply primitive_hasDerivAtBasepoint
exact hf.continuous exact hf.continuous
apply hasDerivAt_const apply hasDerivAt_const
theorem primitive_differentiable
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ : ) :
Differentiable (primitive z₀ f) := by
intro z
exact (primitive_hasDerivAt hf z₀ z).differentiableAt
theorem primitive_hasFderivAt
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ : ) :
∀ z, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ).flip (f z)) z := by
intro z
rw [hasFDerivAt_iff_hasDerivAt]
simp
exact primitive_hasDerivAt hf z₀ z
theorem primitive_hasFderivAt'
{f : }
(hf : Differentiable f)
(z₀ : ) :
∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul (f z)) z := by
intro z
rw [hasFDerivAt_iff_hasDerivAt]
simp
exact primitive_hasDerivAt hf z₀ z
theorem primitive_fderiv
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ : ) :
∀ z, (fderiv (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ).flip (f z) := by
intro z
apply HasFDerivAt.fderiv
exact primitive_hasFderivAt hf z₀ z
theorem primitive_fderiv'
{f : }
(hf : Differentiable f)
(z₀ : ) :
∀ z, (fderiv (primitive z₀ f) z) = ContinuousLinearMap.lsmul (f z) := by
intro z
apply HasFDerivAt.fderiv
exact primitive_hasFderivAt' hf z₀ z