OAI/Analysis/IntegralMeans/Distortion.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.polar_symm_eq_circleMap line 21
  2. lemma OAI.Brennan.circleAverage_eq_integral_neg_pi line 28
  3. lemma OAI.Brennan.integral_ball_polar line 35
  4. lemma OAI.Brennan.ball_closedBall_ae_eq line 95
  5. lemma OAI.Brennan.integral_ball_holomorphic line 103
  6. lemma OAI.Brennan.integral_closedBall_holomorphic line 137
  7. lemma OAI.Brennan.holomorphic_sq_submean line 147
  8. lemma OAI.Brennan.meromorphic_univalent_coefficient line 176
  9. lemma OAI.Brennan.nonconstant_germ_of_injOn line 202
  10. lemma OAI.Brennan.univalent_inverse_continuousAt line 214
  11. lemma OAI.Brennan.univalent_deriv_ne_zero line 229
  12. lemma OAI.Brennan.differentiableAt_of_continuous_root line 288
  13. lemma OAI.Brennan.exists_holomorphic_sqrt_disk line 306
  14. lemma OAI.Brennan.dslope_factor line 337
  15. lemma OAI.Brennan.sq_mem_disk line 341
  16. lemma OAI.Brennan.exists_odd_transform line 345
  17. lemma OAI.Brennan.schlicht_second_deriv_bound line 454
  18. def OAI.Brennan.diskAutomorphism line 467
  19. lemma OAI.Brennan.diskAutomorphism_den_ne_zero line 469
  20. lemma OAI.Brennan.diskAutomorphism_normSq_identity line 481
  21. lemma OAI.Brennan.diskAutomorphism_mem line 487
  22. lemma OAI.Brennan.diskAutomorphism_deriv line 500
  23. lemma OAI.Brennan.diskAutomorphism_injOn line 512
  24. lemma OAI.Brennan.diskAutomorphism_zero line 525
  25. lemma OAI.Brennan.diskAutomorphism_differentiableOn line 527
  26. lemma OAI.Brennan.diskAutomorphism_second_deriv line 531
  27. def OAI.Brennan.diskKoebe line 547
  28. lemma OAI.Brennan.disk_coeff_ne_zero line 550
  29. lemma OAI.Brennan.diskKoebe_univalent line 555
  30. lemma OAI.Brennan.diskKoebe_deriv line 565
  31. lemma OAI.Brennan.diskKoebe_schlicht line 574
  32. lemma OAI.Brennan.diskKoebe_second_deriv line 583
  33. def OAI.Brennan.omittedTransform line 614
  34. lemma OAI.Brennan.omittedTransform_univalent line 616
  35. lemma OAI.Brennan.omittedTransform_deriv line 629
  36. lemma OAI.Brennan.omittedTransform_schlicht line 637
  37. lemma OAI.Brennan.omittedTransform_second_deriv line 646
  38. lemma OAI.Brennan.schlicht_preSchwarzian_bound line 665
  39. lemma OAI.Brennan.schlicht_quarter line 671
  40. lemma OAI.Brennan.hasDerivAt_log_norm_real line 690
  41. lemma OAI.Brennan.logarithmic_distortion line 705
  42. lemma OAI.Brennan.radialDistortion_of_preSchwarzian line 762
  43. lemma OAI.Brennan.schlicht_deriv_bounds line 827
  44. lemma OAI.Brennan.schlicht_deriv_compact_bound line 843
  45. lemma OAI.Brennan.schlicht_lipschitz_bound line 852
  46. lemma OAI.Brennan.schlicht_local_bound line 865
  47. def OAI.Brennan.ballNormalize line 873
  48. lemma OAI.Brennan.affine_disk_maps_ball line 876
  49. lemma OAI.Brennan.ballNormalize_deriv line 884
  50. lemma OAI.Brennan.ballNormalize_schlicht line 897
  51. lemma OAI.Brennan.univalent_ball_quarter line 915
  52. lemma OAI.Brennan.schlicht_separation line 934
  53. lemma OAI.Brennan.schlicht_lower_growth line 947
  54. lemma OAI.Brennan.schlicht_uniform_separation line 957