diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean index 5e30048..b3a912e 100644 --- a/Nevanlinna/firstMain.lean +++ b/Nevanlinna/firstMain.lean @@ -227,4 +227,6 @@ theorem Nevanlinna_firstMain₂ (h₁f : MeromorphicOn f ⊤) : |(h₁f.T_infty r) - ((h₁f.sub (MeromorphicOn.const a)).T_infty r)| ≤ logpos ‖a‖ + log 2 := by + -- See Lang, p. 168 + sorry