diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean index e413143..01003b1 100644 --- a/Nevanlinna/holomorphic_JensenFormula2.lean +++ b/Nevanlinna/holomorphic_JensenFormula2.lean @@ -7,9 +7,21 @@ import Mathlib.Analysis.Analytic.IsolatedZeros lemma xx {f : ℂ → ℂ} {S : Set ℂ} - {R : ℝ} - (h₁ : DifferentiableOn ℂ f (Metric.ball z₀ R)) : - ∃ o : ℂ → ℕ, ∃ F : ℂ → ℂ, ∀ z ∈ (Metric.ball z₀ R), (DifferentiableAt ℂ F z) ∧ (F z ≠ 0) ∧ (f z = F z * ∏ᶠ s ∈ (Metric.ball z₀ R), (z - s) ^ (o s)) := by + (h₁S : IsPreconnected S) + (h₂S : IsCompact S) + (hf : ∀ s ∈ S, AnalyticAt ℂ f s) : + ∃ o : ℂ → ℕ, ∃ F : ℂ → ℂ, ∀ z ∈ S, (AnalyticAt ℂ F z) ∧ (F z ≠ 0) ∧ (f z = F z * ∏ᶠ s ∈ S, (z - s) ^ (o s)) := by + + let o : ℂ → ℕ := by + intro z + if hz : z ∈ S then + let A := hf z hz + let B := A.order + + exact A.order + else + exact 0 + sorry