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 12:40:32 +02:00
parent 3e924d5b4a
commit e5b9559f69
1 changed files with 7 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
Nevanlinna/holomorphic_examples.lean
View File

@ -252,15 +252,16 @@ theorem harmonic_is_realOfHolomorphic
constructor constructor
· -- ∀ (z : ℂ), HolomorphicAt F z · -- ∀ (z : ℂ), HolomorphicAt F z
intro z intro x hx
apply HolomorphicAt_iff.2 apply HolomorphicAt_iff.2
use Set.univ use Metric.ball z R
constructor constructor
· exact isOpen_const · exact Metric.isOpen_ball
· constructor · constructor
· simp · assumption
· intro w _ · intro w hw
exact regF w apply (regF w hw).differentiableAt
apply IsOpen.mem_nhds Metric.isOpen_ball hw
· -- (F z).re = f z · -- (F z).re = f z
have A := reg₂f.differentiable one_le_two have A := reg₂f.differentiable one_le_two
have B : Differentiable ℝ (Complex.reCLM ∘ F) := by have B : Differentiable ℝ (Complex.reCLM ∘ F) := by