OAI/Analysis/Mahler/Lens.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SymmetricMahler.SignedUnitRepresentation.ofFintype line 18
  2. lemma OAI.SymmetricMahler.SignedUnitRepresentation.ofFintype_cost line 36
  3. lemma OAI.SymmetricMahler.lifted_cost_eq line 46
  4. lemma OAI.SymmetricMahler.lens_face_interval line 56
  5. theorem OAI.SymmetricMahler.optimal_signed_of_common_lens line 70
  6. lemma OAI.SymmetricMahler.unconditional_stripMassBound line 169
  7. lemma OAI.SymmetricMahler.stripMap_volume_lower line 184
  8. lemma OAI.SymmetricMahler.nonempty_inter_of_small_deficit line 211
  9. lemma OAI.SymmetricMahler.eventually_nonempty_inter_of_saturation line 225
  10. lemma OAI.SymmetricMahler.exists_nearby_image_of_saturation line 237
  11. lemma OAI.SymmetricMahler.exists_sequence_of_saturation line 253
  12. lemma OAI.SymmetricMahler.subset_dilate_of_one_le line 273
  13. lemma OAI.SymmetricMahler.persistent_open_test_of_body_product line 282
  14. lemma OAI.SymmetricMahler.volume_body_product_dilate line 300
  15. lemma OAI.SymmetricMahler.tendsto_volume_body_product_dilate line 306
  16. theorem OAI.SymmetricMahler.equality_strip_images_dense line 322
  17. lemma OAI.MahlerConformal.summable_odd_square_inv line 377
  18. lemma OAI.MahlerConformal.term_two_bound_closed line 381
  19. lemma OAI.MahlerConformal.summable_series_two_closed line 386
  20. lemma OAI.MahlerConformal.continuousOn_F_closed line 390
  21. lemma OAI.MahlerConformal.closure_Omega_eq line 398
  22. lemma OAI.MahlerConformal.continuous_boundary_F line 406
  23. lemma OAI.MahlerConformal.tendsto_F_polar_boundary line 413
  24. lemma OAI.MahlerConformal.boundary_F_one line 423
  25. lemma OAI.MahlerConformal.integral_B_boundary line 431
  26. lemma OAI.MahlerConformal.Q_boundary line 451
  27. def OAI.MahlerConformal.lensWidth line 462
  28. lemma OAI.MahlerConformal.continuous_lensWidth line 464
  29. lemma OAI.MahlerConformal.lensWidth_one line 467
  30. lemma OAI.MahlerConformal.lensWidth_neg_one line 469
  31. lemma OAI.MahlerConformal.lensWidth_even line 474
  32. lemma OAI.MahlerConformal.boundary_upper_real line 478
  33. def OAI.MahlerConformal.boundaryDerivative line 486
  34. lemma OAI.MahlerConformal.cayley_im_of_ne line 490
  35. lemma OAI.MahlerConformal.continuousAt_boundaryDerivative line 497
  36. lemma OAI.MahlerConformal.hasFDerivWithinAt_F_closed line 509
  37. lemma OAI.MahlerConformal.hasDerivAt_boundary_F line 525
  38. lemma OAI.MahlerConformal.hasDerivAt_boundary_S line 546
  39. lemma OAI.MahlerConformal.cayley_polar_boundary line 553
  40. lemma OAI.MahlerConformal.norm_cayley_polar_boundary line 589
  41. lemma OAI.MahlerConformal.concaveOn_boundary_S line 596
  42. lemma OAI.MahlerConformal.width_angle_mem line 619
  43. lemma OAI.MahlerConformal.concaveOn_lensWidth line 625
  44. lemma OAI.MahlerConformal.lensWidth_nonneg line 638
  45. lemma OAI.MahlerConformal.boundary_width_upper line 648
  46. lemma OAI.MahlerConformal.boundary_width line 667
  47. lemma OAI.MahlerConformal.isCompact_closure_Omega line 683
  48. lemma OAI.MahlerConformal.closure_Omega_real line 687
  49. lemma OAI.MahlerConformal.closure_Omega_im_le line 697
  50. lemma OAI.MahlerConformal.closure_Omega_conj line 730
  51. lemma OAI.MahlerConformal.closure_Omega_width_bound line 737
  52. def OAI.MahlerEndpoint.logCot line 752
  53. lemma OAI.MahlerEndpoint.logCot_scaled_div_log line 754
  54. lemma OAI.MahlerEndpoint.logCot_scaled_ratio line 778
  55. lemma OAI.MahlerEndpoint.profile_ratio line 790
  56. lemma OAI.MahlerEndpoint.concave_ratio_antitone line 822
  57. lemma OAI.MahlerEndpoint.uniform_profile_ratio line 836
  58. lemma OAI.MahlerConformal.lensWidth_zero_pos line 895
  59. lemma OAI.MahlerConformal.lensWidth_endpoint_pos line 909
  60. lemma OAI.MahlerConformal.concaveOn_endpoint_profile line 918
  61. lemma OAI.MahlerConformal.hasDerivAt_endpoint_profile line 928
  62. lemma OAI.MahlerConformal.lensWidth_endpoint_scaling line 946