OAI/NumberTheory/Catalan/Estimates/CauchyKernel.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.blaschkeFactor_imaginary_norm_pos line 21
  2. theorem OAI.InternalCatalan.blaschkeFactor_imaginary_lower line 28
  3. theorem OAI.InternalCatalan.finiteBlaschke_imaginary_lower line 39
  4. theorem OAI.InternalCatalan.finiteBlaschke_inner_quotient_le_one line 47
  5. theorem OAI.InternalCatalan.finiteBlaschke_outer_quotient_le_exp_two line 63
  6. theorem OAI.InternalCatalan.finiteBlaschke_imaginary_norm_abs line 78
  7. theorem OAI.InternalCatalan.finiteBlaschke_quotient_imaginary_norm_abs line 91
  8. theorem OAI.InternalCatalan.finiteBlaschke_diameter_quotient_le_exp_two line 100
  9. def OAI.InternalCatalan.blaschkeDensity line 125
  10. def OAI.InternalCatalan.blaschkeCauchyTransform line 128
  11. theorem OAI.InternalCatalan.imaginary_sub_ne_zero_of_re_ne_zero line 135
  12. theorem OAI.InternalCatalan.abs_re_le_norm_imaginary_sub line 142
  13. theorem OAI.InternalCatalan.continuous_blaschkeDensity_imaginary line 147
  14. theorem OAI.InternalCatalan.continuous_blaschkeCauchyKernel line 164
  15. theorem OAI.InternalCatalan.intervalIntegrable_blaschkeCauchyIntegrand line 172
  16. theorem OAI.InternalCatalan.blaschkeCauchyTransform_normalized line 185
  17. theorem OAI.InternalCatalan.blaschkeCauchyTransform_norm_le line 208
  18. theorem OAI.InternalCatalan.blaschkeCauchyTransform_far_axis_bound line 248
  19. def OAI.InternalCatalan.blaschkeCauchySegment line 265
  20. theorem OAI.InternalCatalan.isCompact_blaschkeCauchySegment line 269
  21. theorem OAI.InternalCatalan.imaginary_sub_ne_zero_of_not_mem_blaschkeCauchySegment line 273
  22. theorem OAI.InternalCatalan.exists_blaschkeCauchySegment_separation line 281
  23. theorem OAI.InternalCatalan.exists_blaschkeCauchySegment_uniform_separation line 293
  24. theorem OAI.InternalCatalan.continuousOn_blaschkeCauchyKernel_off_segment line 309
  25. theorem OAI.InternalCatalan.intervalIntegrable_blaschkeCauchyKernel_off_segment line 319
  26. theorem OAI.InternalCatalan.intervalIntegrable_blaschkeCauchyIntegrand_off_segment line 329
  27. theorem OAI.InternalCatalan.blaschkeCauchyKernel_hasDerivAt line 350
  28. theorem OAI.InternalCatalan.blaschkeCauchyKernel_derivative_norm_le line 363