OAI/Algebra/Drinfeld/Boundary.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.loop_x line 13
  2. theorem OAI.RealDeligneDrinfeld.BraidInsertionSum.loop_y line 21
  3. theorem OAI.RealDeligneDrinfeld.KZLogDifference.difference line 38
  4. theorem OAI.RealDeligneDrinfeld.KZLogDifference.exponential line 54
  5. lemma OAI.DeligneDrinfeld.PoleEstimate.continuousOn_inv line 73
  6. lemma OAI.DeligneDrinfeld.PoleEstimate.integral_inv_sq line 76
  7. lemma OAI.DeligneDrinfeld.PoleEstimate.integral_inv_sq_le line 88
  8. lemma OAI.DeligneDrinfeld.PoleEstimate.integral_inv_le line 93
  9. lemma OAI.DeligneDrinfeld.PoleEstimate.abs_inv_add_sub_inv_le line 99
  10. lemma OAI.DeligneDrinfeld.PoleEstimate.abs_inv_sub_sub_inv_le line 112
  11. lemma OAI.DeligneDrinfeld.PoleEstimate.integral_abs_inv_add_sub_inv_le line 129
  12. lemma OAI.DeligneDrinfeld.PoleEstimate.integral_abs_inv_sub_sub_inv_le line 142
  13. theorem OAI.DeligneDrinfeld.PoleEstimate.integralNorm_add_le line 162
  14. lemma OAI.DeligneDrinfeld.PoleEstimate.scalar_right_inv_continuous line 170
  15. lemma OAI.DeligneDrinfeld.PoleEstimate.integral_right_inv_abs line 175
  16. theorem OAI.DeligneDrinfeld.PoleEstimate.bulkForm_mass line 190
  17. def OAI.DeligneDrinfeld.PoleEstimate.shiftedBulk line 214
  18. lemma OAI.DeligneDrinfeld.PoleEstimate.right_shift_abs line 217
  19. lemma OAI.DeligneDrinfeld.PoleEstimate.integral_right_shift line 221
  20. lemma OAI.DeligneDrinfeld.PoleEstimate.shiftedBulk_continuous line 227
  21. lemma OAI.DeligneDrinfeld.PoleEstimate.shiftedBulk_error_mass line 241
  22. def OAI.DeligneDrinfeld.FourCollar.form line 278
  23. def OAI.DeligneDrinfeld.FourCollar.cx line 282
  24. def OAI.DeligneDrinfeld.FourCollar.cy line 284
  25. def OAI.DeligneDrinfeld.FourCollar.vx line 286
  26. def OAI.DeligneDrinfeld.FourCollar.vy line 288
  27. def OAI.DeligneDrinfeld.FourCollar.residue line 291
  28. def OAI.DeligneDrinfeld.FourCollar.remainder line 294
  29. theorem OAI.DeligneDrinfeld.FourCollar.coordinates_derivative line 302
  30. theorem OAI.DeligneDrinfeld.FourCollar.scalar_nonzero line 321
  31. theorem OAI.DeligneDrinfeld.FourCollar.chamber line 328
  32. theorem OAI.DeligneDrinfeld.FourCollar.form_collar line 345
  33. theorem OAI.DeligneDrinfeld.FourCollar.remainder_continuous line 380
  34. theorem OAI.DeligneDrinfeld.FourCollar.residue_mem line 411
  35. theorem OAI.DeligneDrinfeld.FourCollar.remainder_mem line 419
  36. def OAI.DeligneDrinfeld.FourCollar.normalized line 432
  37. theorem OAI.DeligneDrinfeld.FourCollar.normalized_derivative line 437
  38. theorem OAI.DeligneDrinfeld.FourCollar.normalized_limit line 445
  39. theorem OAI.DeligneDrinfeld.FourCollar.normalized_isUnit line 451
  40. def OAI.DeligneDrinfeld.BCBoundary.endpoint line 464
  41. theorem OAI.DeligneDrinfeld.BCBoundary.interval_bounds line 466
  42. theorem OAI.DeligneDrinfeld.BCBoundary.form_eq line 472
  43. theorem OAI.DeligneDrinfeld.BCBoundary.error_bound line 478
  44. theorem OAI.DeligneDrinfeld.BCBoundary.bulk_bound line 495
  45. def OAI.DeligneDrinfeld.BCBoundary.mass line 506
  46. theorem OAI.DeligneDrinfeld.BCBoundary.mass_subpower line 510
  47. theorem OAI.DeligneDrinfeld.BCBoundary.perturbation line 515
  48. theorem OAI.DeligneDrinfeld.BCBoundary.shared_residue_cancel line 546
  49. theorem OAI.DeligneDrinfeld.BCBoundary.gap_tendsto line 564
  50. theorem OAI.DeligneDrinfeld.BCBoundary.bulk_limit line 572
  51. theorem OAI.DeligneDrinfeld.BCBoundary.limit line 587
  52. def OAI.DeligneDrinfeld.KZRectangle.edges line 611
  53. def OAI.DeligneDrinfeld.KZRectangle.dif line 612
  54. def OAI.DeligneDrinfeld.KZRectangle.chords line 614
  55. theorem OAI.DeligneDrinfeld.KZRectangle.form_eq line 618
  56. theorem OAI.DeligneDrinfeld.KZRectangle.form_commute line 628
  57. theorem OAI.DeligneDrinfeld.KZRectangle.dif_ne_zero line 638
  58. theorem OAI.DeligneDrinfeld.KZRectangle.transport_derivative line 644
  59. theorem OAI.DeligneDrinfeld.KZRectangle.transport_homotopy line 688
  60. def OAI.DeligneDrinfeld.StraightKZ.segment line 747
  61. def OAI.DeligneDrinfeld.StraightKZ.velocity line 749
  62. theorem OAI.DeligneDrinfeld.StraightKZ.segment_zero line 751
  63. theorem OAI.DeligneDrinfeld.StraightKZ.segment_one line 753
  64. theorem OAI.DeligneDrinfeld.StraightKZ.segment_strictMono line 756
  65. theorem OAI.DeligneDrinfeld.StraightKZ.segment_derivative line 770
  66. def OAI.DeligneDrinfeld.StraightKZ.connection line 777
  67. def OAI.DeligneDrinfeld.StraightKZ.fundamental line 780
  68. lemma OAI.DeligneDrinfeld.StraightKZ.connection_mem line 783
  69. lemma OAI.DeligneDrinfeld.StraightKZ.zero_connection line 788
  70. theorem OAI.DeligneDrinfeld.StraightKZ.fundamental_isUnit line 796
  71. theorem OAI.DeligneDrinfeld.StraightKZ.fundamental_derivative line 801