OAI/Geometry/UnitDistances/Profiles.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.LocalProfiles.rareBit line 11
  2. def OAI.PlanarUnitDistances.LocalProfiles.exceptional line 12
  3. def OAI.PlanarUnitDistances.LocalProfiles.X line 14
  4. def OAI.PlanarUnitDistances.LocalProfiles.signed line 17
  5. def OAI.PlanarUnitDistances.LocalProfiles.jfirst line 19
  6. def OAI.PlanarUnitDistances.LocalProfiles.jsecond line 21
  7. def OAI.PlanarUnitDistances.LocalProfiles.jpoints line 23
  8. def OAI.PlanarUnitDistances.LocalProfiles.ifirst line 25
  9. def OAI.PlanarUnitDistances.LocalProfiles.isecond line 27
  10. def OAI.PlanarUnitDistances.LocalProfiles.bits line 29
  11. def OAI.PlanarUnitDistances.LocalProfiles.error1 line 32
  12. def OAI.PlanarUnitDistances.LocalProfiles.error2 line 35
  13. lemma OAI.PlanarUnitDistances.LocalProfiles.X_nonneg line 38
  14. lemma OAI.PlanarUnitDistances.LocalProfiles.error1_nonneg line 41
  15. lemma OAI.PlanarUnitDistances.LocalProfiles.error2_nonneg line 44
  16. lemma OAI.PlanarUnitDistances.LocalProfiles.residual line 48
  17. lemma OAI.PlanarUnitDistances.LocalProfiles.size line 66
  18. def OAI.PlanarUnitDistances.WedgeSummary.JW line 82
  19. lemma OAI.PlanarUnitDistances.WedgeSummary.first_joint line 84
  20. lemma OAI.PlanarUnitDistances.WedgeSummary.second_joint line 89
  21. lemma OAI.PlanarUnitDistances.WedgeSummary.point_joint line 94
  22. lemma OAI.PlanarUnitDistances.WedgeSummary.first_error line 98
  23. lemma OAI.PlanarUnitDistances.WedgeSummary.second_error line 103
  24. lemma OAI.PlanarUnitDistances.WedgeSummary.X_average line 109
  25. lemma OAI.PlanarUnitDistances.WedgeSummary.err1_at line 119
  26. lemma OAI.PlanarUnitDistances.WedgeSummary.err2_at line 139
  27. lemma OAI.PlanarUnitDistances.WedgeSummary.cut_error line 150
  28. theorem OAI.PlanarUnitDistances.WedgeSummary.residual_budget line 160
  29. theorem OAI.PlanarUnitDistances.WedgeSummary.size_budget line 171
  30. lemma OAI.PlanarUnitDistances.ThresholdProfiles.bit_integral line 186
  31. lemma OAI.PlanarUnitDistances.ThresholdProfiles.signed_bit_sub_integral line 204
  32. structure OAI.PlanarUnitDistances.ActualProfiles.Input line 220
  33. def OAI.PlanarUnitDistances.ActualProfiles.Input.book line 237
  34. def OAI.PlanarUnitDistances.ActualProfiles.Input.snap line 239
  35. def OAI.PlanarUnitDistances.ActualProfiles.Input.threshold line 241
  36. def OAI.PlanarUnitDistances.ActualProfiles.Input.profile line 243
  37. def OAI.PlanarUnitDistances.ActualProfiles.Input.heightAt line 245
  38. def OAI.PlanarUnitDistances.ActualProfiles.Input.errorAt line 247
  39. lemma OAI.PlanarUnitDistances.ActualProfiles.Input.integral line 251
  40. lemma OAI.PlanarUnitDistances.ActualProfiles.Input.piece line 254
  41. lemma OAI.PlanarUnitDistances.ActualProfiles.Input.bits_eq line 258
  42. lemma OAI.PlanarUnitDistances.ActualProfiles.Input.height_nonneg line 266
  43. lemma OAI.PlanarUnitDistances.ActualProfiles.Input.error_nonneg line 268
  44. theorem OAI.PlanarUnitDistances.ActualProfiles.Input.residual line 275
  45. theorem OAI.PlanarUnitDistances.ActualProfiles.Input.size line 303
  46. lemma OAI.PlanarUnitDistances.SamplingDecay.limit line 333
  47. def OAI.PlanarUnitDistances.BudgetParameters.vanishing line 361
  48. lemma OAI.PlanarUnitDistances.BudgetParameters.vanishing_pos line 362
  49. lemma OAI.PlanarUnitDistances.BudgetParameters.vanishing_limit line 363
  50. structure OAI.PlanarUnitDistances.BudgetParameters.Params line 366
  51. def OAI.PlanarUnitDistances.BudgetParameters.Params.zeta line 382
  52. lemma OAI.PlanarUnitDistances.BudgetParameters.Params.zeta_pos line 383
  53. lemma OAI.PlanarUnitDistances.BudgetParameters.Params.k_zeta line 387
  54. def OAI.PlanarUnitDistances.BudgetParameters.joint line 392
  55. def OAI.PlanarUnitDistances.BudgetParameters.leading line 394
  56. def OAI.PlanarUnitDistances.BudgetParameters.wedge line 399
  57. theorem OAI.PlanarUnitDistances.BudgetParameters.exists_small line 402
  58. def OAI.PlanarUnitDistances.IncidenceBook.capacity line 467
  59. def OAI.PlanarUnitDistances.IncidenceBook.length line 468
  60. lemma OAI.PlanarUnitDistances.IncidenceBook.capacity_pos line 469
  61. lemma OAI.PlanarUnitDistances.IncidenceBook.length_pos line 470
  62. structure OAI.PlanarUnitDistances.IncidenceBook.Realization line 471
  63. def OAI.PlanarUnitDistances.IncidenceBook.labelFintype line 483
  64. def OAI.PlanarUnitDistances.IncidenceBook.snapshotFintype line 485
  65. def OAI.PlanarUnitDistances.IncidenceBook.Realization.good line 487
  66. def OAI.PlanarUnitDistances.IncidenceBook.Realization.input line 491
  67. def OAI.PlanarUnitDistances.IncidenceBook.Realization.book line 506
  68. def OAI.PlanarUnitDistances.IncidenceBook.Realization.fractional line 509
  69. def OAI.PlanarUnitDistances.IncidenceBook.Realization.scale_eq line 511
  70. def OAI.PlanarUnitDistances.IncidenceBook.Realization.mistake_bound line 513
  71. def OAI.PlanarUnitDistances.IncidenceBook.Realization.history_bound line 515
  72. def OAI.PlanarUnitDistances.IncidenceBook.Realization.stable line 517
  73. def OAI.PlanarUnitDistances.IncidenceBook.Realization.rare line 519
  74. def OAI.PlanarUnitDistances.IncidenceBook.Realization.common_bound line 522
  75. def OAI.PlanarUnitDistances.IncidenceBook.Realization.bad_bound line 523
  76. def OAI.PlanarUnitDistances.IncidenceBook.Realization.height_bound line 524
  77. def OAI.PlanarUnitDistances.IncidenceBook.Realization.joint_bound line 525
  78. def OAI.PlanarUnitDistances.IncidenceBook.Realization.wedge_bound line 527
  79. def OAI.PlanarUnitDistances.IncidenceBook.Realization.prediction_bound line 529
  80. def OAI.PlanarUnitDistances.IncidenceBook.Realization.Valid line 531
  81. theorem OAI.PlanarUnitDistances.IncidenceBook.constants line 535
  82. def OAI.PlanarUnitDistances.BookEnvelope.height line 578
  83. def OAI.PlanarUnitDistances.BookEnvelope.j line 579
  84. def OAI.PlanarUnitDistances.BookEnvelope.pred line 580
  85. def OAI.PlanarUnitDistances.BookEnvelope.star line 581
  86. def OAI.PlanarUnitDistances.BookEnvelope.prediction line 582
  87. def OAI.PlanarUnitDistances.BookEnvelope.common line 583
  88. def OAI.PlanarUnitDistances.BookEnvelope.center line 586
  89. def OAI.PlanarUnitDistances.BookEnvelope.point line 587
  90. def OAI.PlanarUnitDistances.BookEnvelope.sc line 588
  91. def OAI.PlanarUnitDistances.BookEnvelope.total line 589
  92. theorem OAI.PlanarUnitDistances.BookEnvelope.total_limit line 592
  93. lemma OAI.PlanarUnitDistances.BookEnvelope.sampling_nonneg line 628
  94. theorem OAI.PlanarUnitDistances.BookEnvelope.bounds line 637
  95. theorem OAI.PlanarUnitDistances.CoercivityAll.all line 705