OAI/Analysis/HotSpots/Riemann.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Complex.exists_injective_not_dense_image_deriv_ne_zero line 44
  2. lemma OAI.Complex.exists_mapsTo_unitBall_injOn_deriv_ne_zero line 113
  3. def OAI.StrictHotSpots.Riemann.extend line 147
  4. lemma OAI.StrictHotSpots.Riemann.extend_coe line 151
  5. lemma OAI.StrictHotSpots.Riemann.extend_eq line 154
  6. lemma OAI.StrictHotSpots.Riemann.extend_continuousOn line 157
  7. def OAI.StrictHotSpots.Riemann.holomorphicBall line 162
  8. lemma OAI.StrictHotSpots.Riemann.tendsto_extend line 165
  9. lemma OAI.StrictHotSpots.Riemann.holomorphicBall_isClosed line 172
  10. lemma OAI.StrictHotSpots.Riemann.holomorphicBall_dist_bound line 185
  11. lemma OAI.StrictHotSpots.Riemann.holomorphicBall_equicontinuous line 202
  12. lemma OAI.StrictHotSpots.Riemann.holomorphicBall_isCompact line 216
  13. lemma OAI.StrictHotSpots.Riemann.deriv_tendsto line 231
  14. lemma OAI.StrictHotSpots.Riemann.hurwitz_locally_zero line 248
  15. lemma OAI.StrictHotSpots.Riemann.hurwitz_injective line 302
  16. def OAI.StrictHotSpots.Riemann.normalizedMaps line 330
  17. lemma OAI.StrictHotSpots.Riemann.normalizedMaps_isClosed line 333
  18. lemma OAI.StrictHotSpots.Riemann.normalizedMaps_isCompact line 367
  19. lemma OAI.StrictHotSpots.Riemann.deriv_continuousOn line 372
  20. lemma OAI.StrictHotSpots.Riemann.exists_extremal line 379
  21. lemma OAI.StrictHotSpots.Riemann.extend_eventuallyEq line 388
  22. lemma OAI.StrictHotSpots.Riemann.normalized_initial line 395
  23. lemma OAI.StrictHotSpots.Riemann.exists_nonzero_extremal line 424
  24. lemma OAI.StrictHotSpots.Riemann.normalized_norm_lt line 432
  25. def OAI.StrictHotSpots.Riemann.mobius line 456
  26. lemma OAI.StrictHotSpots.Riemann.mobius_denom_ne line 458
  27. lemma OAI.StrictHotSpots.Riemann.mobius_norm_identity line 468
  28. lemma OAI.StrictHotSpots.Riemann.norm_mobius_lt line 474
  29. lemma OAI.StrictHotSpots.Riemann.mobius_self line 483
  30. lemma OAI.StrictHotSpots.Riemann.mobius_zero line 484
  31. lemma OAI.StrictHotSpots.Riemann.mobius_injOn line 486
  32. lemma OAI.StrictHotSpots.Riemann.hasDerivAt_mobius line 495
  33. lemma OAI.StrictHotSpots.Riemann.hasDerivAt_mobius_zero line 505
  34. lemma OAI.StrictHotSpots.Riemann.norm_mobius_self_deriv line 509
  35. lemma OAI.StrictHotSpots.Riemann.norm_mobius_zero_deriv line 517
  36. lemma OAI.StrictHotSpots.Riemann.hasDerivAt_continuous_square_root line 523
  37. lemma OAI.StrictHotSpots.Riemann.root_improvement_inequality line 540
  38. lemma OAI.StrictHotSpots.Riemann.exists_root_improvement line 554
  39. lemma OAI.StrictHotSpots.Riemann.exists_normalized_bijective line 613
  40. lemma OAI.StrictHotSpots.Riemann.analytic_inverse_openPartialHomeomorph line 659
  41. lemma OAI.StrictHotSpots.Riemann.exists_biholomorphic_inverse line 696
  42. theorem OAI.StrictHotSpots.Riemann.exists_disk_biholomorphism line 729
  43. lemma OAI.StrictHotSpots.Conformal.conjugate_contDiffOn line 771
  44. lemma OAI.StrictHotSpots.Conformal.conjugate_hasFDerivAt line 779
  45. theorem OAI.StrictHotSpots.Conformal.exists_interior_chart line 789
  46. lemma OAI.StrictHotSpots.Conformal.chartMeasure_univ line 868
  47. lemma OAI.StrictHotSpots.Conformal.chartMeasure_finite line 874
  48. def OAI.StrictHotSpots.Conformal.potentialMeasure line 879
  49. lemma OAI.StrictHotSpots.Conformal.potentialMeasure_density line 882
  50. lemma OAI.StrictHotSpots.Conformal.potentialMeasure_integral line 890
  51. lemma OAI.StrictHotSpots.Conformal.potentialMeasure_map line 895
  52. lemma OAI.StrictHotSpots.Conformal.potentialMeasure_finite line 900
  53. lemma OAI.StrictHotSpots.Conformal.scale_gap line 905
  54. theorem OAI.StrictHotSpots.Conformal.potentialMeasure_subcritical line 913
  55. theorem OAI.StrictHotSpots.Conformal.exists_actual_subcritical_potential line 930
  56. lemma OAI.StrictHotSpots.Riemann.mobius_neg_zero line 979
  57. theorem OAI.StrictHotSpots.Riemann.schwarz_mobius_ball line 982
  58. theorem OAI.StrictHotSpots.Riemann.schwarz_pick_deriv line 1004
  59. lemma OAI.StrictHotSpots.Riemann.mobius_deficit_identity line 1046
  60. lemma OAI.StrictHotSpots.Riemann.mobius_boundary_deficit line 1056
  61. theorem OAI.StrictHotSpots.Riemann.disk_distance_from_interior_ball line 1086