OAI/Analysis/NodalLength/HolomorphicLength.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Holomorphic.zero_free_logDeriv_bound_wide line 284
2. lemma OAI.SharpNodal.Holomorphic.blaschke_logDeriv_bound_wide line 339
3. lemma OAI.SharpNodal.Holomorphic.factor_logDeriv_bound_wide line 357
4. lemma OAI.SharpNodal.Holomorphic.exists_zeroWeight_wide line 390
5. lemma OAI.SharpNodal.Profiles.holomorphic_gradient_local_length_wide line 436
6. lemma OAI.SharpNodal.Profiles.nodal_length_of_weight_wide line 518
7. lemma OAI.SharpNodal.Profiles.nodal_length_holomorphic_comparison_wide line 578