OAI/Analysis/NodalLength/NodalGraphs.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpNodal.Holomorphic.blaschke line 257
2. lemma OAI.SharpNodal.Holomorphic.blaschke_eq_inv line 259
3. lemma OAI.SharpNodal.Holomorphic.blaschke_denom_ne line 263
4. lemma OAI.SharpNodal.Holomorphic.blaschke_analytic line 274
5. lemma OAI.SharpNodal.Holomorphic.blaschke_norm_sphere line 280
6. lemma OAI.SharpNodal.Holomorphic.blaschke_norm_le line 284
7. lemma OAI.SharpNodal.Holomorphic.blaschke_ne_zero line 301
8. lemma OAI.SharpNodal.Holomorphic.blaschke_logDeriv line 306
9. lemma OAI.SharpNodal.Holomorphic.codiscrete_analytic_eq line 319
10. lemma OAI.SharpNodal.Holomorphic.analytic_max_ball line 338
11. lemma OAI.SharpNodal.Holomorphic.finite_blaschke_factorization line 347
12. lemma OAI.SharpNodal.Holomorphic.exists_holomorphic_log line 427
13. lemma OAI.SharpNodal.Holomorphic.zero_free_logDeriv_bound line 448
14. lemma OAI.SharpNodal.Profiles.plane_norm_le_abs line 510
15. lemma OAI.SharpNodal.Profiles.plane_map_expansion line 516
16. lemma OAI.SharpNodal.Profiles.nodal_graph_distance line 521
17. lemma OAI.SharpNodal.Profiles.nodal_graph_length line 545