OAI/NumberTheory/Catalan/Analysis/BlaschkeDensityLogDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.reciprocalFactor_hasDerivAt line 10
2. theorem OAI.InternalCatalan.reciprocalFactor_logDeriv line 20
3. theorem OAI.InternalCatalan.blaschkeDensity_logDeriv line 28
4. theorem OAI.InternalCatalan.blaschkeDensity_endpoint_ne_zero line 60
5. theorem OAI.InternalCatalan.blaschkeDensity_endpoint_logDeriv_norm_le line 74
6. theorem OAI.InternalCatalan.blaschkeDensity_endpoint_deriv_norm_le line 119