OAI/NumberTheory/Catalan/Estimates/BlaschkeEndpointGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.reciprocal_blaschkeFactor_endpoint_norm_le line 13
2. theorem OAI.InternalCatalan.blaschkeDensity_endpoint_norm_le_exp line 56
3. theorem OAI.InternalCatalan.blaschkeDensity_endpoint_norm_le_exp_twelve line 84
4. theorem OAI.InternalCatalan.blaschkeDensity_near_imaginary_units_norm_le line 101
5. theorem OAI.InternalCatalan.norm_ge_three_quarters_near_unit line 114
6. theorem OAI.InternalCatalan.blaschkeFactor_endpoint_norm_lower line 120