kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update holomorphic_examples.lean

This commit is contained in:
Stefan Kebekus 2024-08-08 13:30:59 +02:00
parent e5b9559f69
commit 6a12258093
1 changed files with 37 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
Nevanlinna/holomorphic_examples.lean
View File

@ -112,7 +112,7 @@ theorem harmonic_is_realOfHolomorphic
{R : ℝ} {R : ℝ}
(hR : 0 < R) (hR : 0 < R)
(hf : ∀ x ∈ Metric.ball z R, HarmonicAt f x) : (hf : ∀ x ∈ Metric.ball z R, HarmonicAt f x) :
∃ F : ℂ → ℂ, (∀ z ∈ Metric.ball z R, HolomorphicAt F z) ∧ (Set.EqOn (Complex.reCLM ∘ F) f (Metric.ball z R)) := by ∃ F : ℂ → ℂ, (∀ x ∈ Metric.ball z R, HolomorphicAt F x) ∧ (Set.EqOn (Complex.reCLM ∘ F) f (Metric.ball z R)) := 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)
@ -251,7 +251,7 @@ theorem harmonic_is_realOfHolomorphic
use F use F
constructor constructor
· -- ∀ (z : ℂ), HolomorphicAt F z · -- ∀ x ∈ Metric.ball z R, HolomorphicAt F x
intro x hx intro x hx
apply HolomorphicAt_iff.2 apply HolomorphicAt_iff.2
use Metric.ball z R use Metric.ball z R
@ -262,20 +262,21 @@ theorem harmonic_is_realOfHolomorphic
· intro w hw · intro w hw
apply (regF w hw).differentiableAt apply (regF w hw).differentiableAt
apply IsOpen.mem_nhds Metric.isOpen_ball hw apply IsOpen.mem_nhds Metric.isOpen_ball hw
· -- (F z).re = f z · -- Set.EqOn (⇑Complex.reCLM ∘ F) f (Metric.ball z R)
have A := reg₂f.differentiable one_le_two have : DifferentiableOn ℝ (Complex.reCLM ∘ F) (Metric.ball z R) := by
have B : Differentiable ℝ (Complex.reCLM ∘ F) := by apply DifferentiableOn.comp
apply Differentiable.comp apply Differentiable.differentiableOn
exact ContinuousLinearMap.differentiable Complex.reCLM apply ContinuousLinearMap.differentiable Complex.reCLM
exact Differentiable.restrictScalars ℝ regF apply regF.restrictScalars ℝ
have C : (F 0).re = f 0 := by exact Set.mapsTo'.mpr fun ⦃a⦄ _ => hR
dsimp [F] have hz : z ∈ Metric.ball z R := by exact Metric.mem_ball_self hR
rw [primitive_zeroAtBasepoint] apply Convex.eqOn_of_fderivWithin_eq _ this _ _ _ hz _
simp exact convex_ball z R
apply reg₂f.differentiableOn one_le_two
apply IsOpen.uniqueDiffOn Metric.isOpen_ball
apply eq_of_fderiv_eq B A _ 0 C intro x hx
rw [fderivWithin_eq_fderiv, fderivWithin_eq_fderiv]
intro x
rw [fderiv.comp] rw [fderiv.comp]
simp simp
apply ContinuousLinearMap.ext apply ContinuousLinearMap.ext
@ -290,7 +291,24 @@ theorem harmonic_is_realOfHolomorphic
rw [(fderiv ℝ f x).map_smul, (fderiv ℝ f x).map_smul] rw [(fderiv ℝ f x).map_smul, (fderiv ℝ f x).map_smul]
rw [smul_eq_mul, smul_eq_mul] rw [smul_eq_mul, smul_eq_mul]
ring ring
-- DifferentiableAt ℝ (⇑Complex.reCLM) (F x)
fun_prop assumption
-- DifferentiableAt ℝ F x exact ContinuousLinearMap.differentiableAt Complex.reCLM
exact regF.restrictScalars ℝ x apply (regF.restrictScalars ℝ x hx).differentiableAt
apply IsOpen.mem_nhds Metric.isOpen_ball hx
apply IsOpen.uniqueDiffOn Metric.isOpen_ball
assumption
apply (reg₂f.differentiableOn one_le_two).differentiableAt
apply IsOpen.mem_nhds Metric.isOpen_ball hx
apply IsOpen.uniqueDiffOn Metric.isOpen_ball
assumption
-- DifferentiableAt ℝ (⇑Complex.reCLM ∘ F) x
apply DifferentiableAt.comp
apply Differentiable.differentiableAt
exact ContinuousLinearMap.differentiable Complex.reCLM
apply (regF.restrictScalars ℝ x hx).differentiableAt
apply IsOpen.mem_nhds Metric.isOpen_ball hx
--
dsimp [F]
rw [primitive_zeroAtBasepoint]
simp