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

Update holomorphic_JensenFormula2.lean

This commit is contained in:
Stefan Kebekus 2024-08-22 14:52:52 +02:00
parent b818aa5c13
commit 42a6c439a9
1 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Nevanlinna/holomorphic_JensenFormula2.lean
View File

@ -8,6 +8,14 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
open Real open Real
noncomputable def Zeroset
{f : ℂ → ℂ}
{s : Set ℂ}
(hf : ∀ z ∈ s, HolomorphicAt f z) :
Set ℂ := by
exact f⁻¹' {0} ∩ s
noncomputable def ZeroFinset noncomputable def ZeroFinset
{f : ℂ → ℂ} {f : ℂ → ℂ}
(h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
@ -272,7 +280,9 @@ theorem jensen_case_R_eq_one
simp_rw [← Complex.norm_eq_abs] at this simp_rw [← Complex.norm_eq_abs] at this
rw [t₁] at this rw [t₁] at this
--let Z₁ := (ZeroFinset h₁f h₂f) ∩ (Metric.ball 0 1)
let Z₂ := { x : ZeroFinset h₁f h₂f | ‖x.1‖ = 1 }
sorry sorry