OAI/Analysis/NodalLength/Divisors.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpNodal.Holomorphic.zeroWeight line 265
2. lemma OAI.SharpNodal.Holomorphic.zeroWeight_pos line 268
3. lemma OAI.SharpNodal.Holomorphic.zeroWeight_term_le line 273
4. lemma OAI.SharpNodal.Holomorphic.zeroWeight_radius line 278
5. lemma OAI.SharpNodal.Holomorphic.zeroWeight_local_comparison line 288
6. lemma OAI.SharpNodal.Holomorphic.blaschke_logDeriv_bound line 340
7. lemma OAI.SharpNodal.Holomorphic.factor_logDeriv_bound line 358
8. lemma OAI.SharpNodal.Holomorphic.local_divisor_sum_bound line 391
9. lemma OAI.SharpNodal.Holomorphic.exists_zeroWeight line 428
10. lemma OAI.SharpNodal.Holomorphic.small_variation line 477