OAI/Geometry/UnitDistances/Levels.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.LevelStates.state line 11
  2. lemma OAI.PlanarUnitDistances.LevelStates.state_measurable line 19
  3. def OAI.PlanarUnitDistances.LevelStates.bit line 29
  4. lemma OAI.PlanarUnitDistances.LevelStates.bit_measurable line 33
  5. def OAI.PlanarUnitDistances.LevelStates.edgeError line 42
  6. lemma OAI.PlanarUnitDistances.LevelStates.edgeError_measurable line 47
  7. lemma OAI.PlanarUnitDistances.LevelStates.edgeError_bounds line 55
  8. def OAI.PlanarUnitDistances.LevelStates.meanError line 60
  9. lemma OAI.PlanarUnitDistances.LevelStates.meanError_measurable line 63
  10. lemma OAI.PlanarUnitDistances.LevelStates.meanError_bounds line 67
  11. lemma OAI.PlanarUnitDistances.LevelStates.edgeError_arch line 75
  12. lemma OAI.PlanarUnitDistances.LevelStates.edgeError_finite_ae line 84
  13. lemma OAI.PlanarUnitDistances.LevelStates.integral_meanError line 94
  14. theorem OAI.PlanarUnitDistances.LevelStates.exists_bounded_states line 110
  15. def OAI.PlanarUnitDistances.ThresholdProfiles.bit line 159
  16. lemma OAI.PlanarUnitDistances.ThresholdProfiles.bit_nonneg line 161
  17. lemma OAI.PlanarUnitDistances.ThresholdProfiles.bit_le_one line 162
  18. lemma OAI.PlanarUnitDistances.ThresholdProfiles.bit_measurable line 163
  19. lemma OAI.PlanarUnitDistances.ThresholdProfiles.bit_integrableOn line 166
  20. lemma OAI.PlanarUnitDistances.ThresholdProfiles.abs_bit_sub_eq line 173
  21. lemma OAI.PlanarUnitDistances.ThresholdProfiles.bit_sub_integral line 178
  22. lemma OAI.PlanarUnitDistances.ThresholdProfiles.bit_mismatch line 190
  23. def OAI.PlanarUnitDistances.ThresholdProfiles.frequency line 197
  24. def OAI.PlanarUnitDistances.ThresholdProfiles.minority line 199
  25. lemma OAI.PlanarUnitDistances.ThresholdProfiles.frequency_nonneg line 202
  26. lemma OAI.PlanarUnitDistances.ThresholdProfiles.frequency_le_one line 205
  27. lemma OAI.PlanarUnitDistances.ThresholdProfiles.frequency_measurable line 212
  28. lemma OAI.PlanarUnitDistances.ThresholdProfiles.minority_integrableOn line 217
  29. lemma OAI.PlanarUnitDistances.ThresholdProfiles.independent_mismatch line 229
  30. lemma OAI.PlanarUnitDistances.ThresholdProfiles.mismatch_le_twice_minority line 251
  31. lemma OAI.PlanarUnitDistances.ThresholdProfiles.pair_integrableOn line 259
  32. lemma OAI.PlanarUnitDistances.ThresholdProfiles.mismatch_integrableOn line 263
  33. lemma OAI.PlanarUnitDistances.ThresholdProfiles.integrated_mismatch line 268
  34. lemma OAI.PlanarUnitDistances.ThresholdProfiles.expected_distance_identity line 281
  35. lemma OAI.PlanarUnitDistances.ThresholdProfiles.expected_distance_le line 289
  36. lemma OAI.PlanarUnitDistances.ThresholdProfiles.minority_of_constant line 297
  37. lemma OAI.PlanarUnitDistances.ThresholdProfiles.finiteSupport_profile line 311
  38. lemma OAI.PlanarUnitDistances.ThresholdProfiles.finiteSupport_minorIntegral line 325
  39. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.archThreshold line 344
  40. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteThreshold line 346
  41. def OAI.PlanarUnitDistances.WeightedAbsoluteValues.profileScale line 349
  42. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteThreshold_support line 358
  43. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteProfile_integral_support line 363
  44. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.finiteProfile_pair_support line 371
  45. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.log_quotient_distance line 380
  46. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.profile_pair_height line 386
  47. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.weighted_height_profile_identity line 393
  48. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.expected_height_le_profileScale line 430
  49. lemma OAI.PlanarUnitDistances.WeightedAbsoluteValues.exists_normalizing_edge line 453
  50. def OAI.PlanarUnitDistances.LevelScale.weight line 487
  51. def OAI.PlanarUnitDistances.LevelScale.measure line 489
  52. instance OAI.PlanarUnitDistances.LevelScale.(instance at line 491) line 491
  53. def OAI.PlanarUnitDistances.LevelScale.cut line 493
  54. def OAI.PlanarUnitDistances.LevelScale.prob line 494
  55. def OAI.PlanarUnitDistances.LevelScale.minority line 496
  56. def OAI.PlanarUnitDistances.LevelScale.scale line 498
  57. lemma OAI.PlanarUnitDistances.LevelScale.prob_bounds line 501
  58. lemma OAI.PlanarUnitDistances.LevelScale.prob_measurable line 505
  59. lemma OAI.PlanarUnitDistances.LevelScale.minority_measurable line 508
  60. lemma OAI.PlanarUnitDistances.LevelScale.minority_bounds line 510
  61. lemma OAI.PlanarUnitDistances.LevelScale.scale_nonneg line 515
  62. lemma OAI.PlanarUnitDistances.LevelScale.scale_eq line 517
  63. lemma OAI.PlanarUnitDistances.LevelScale.pair_distance line 525
  64. theorem OAI.PlanarUnitDistances.LevelScale.expected_height_le_scale line 547
  65. lemma OAI.PlanarUnitDistances.LevelScale.exists_normalizing_edge line 583
  66. def OAI.PlanarUnitDistances.FiniteLaw.support line 601
  67. lemma OAI.PlanarUnitDistances.FiniteLaw.support_avg line 614
  68. lemma OAI.PlanarUnitDistances.LevelScale.scale_support line 631
  69. theorem OAI.PlanarUnitDistances.LevelScale.exists_normalizing_edge_support line 640
  70. lemma OAI.PlanarUnitDistances.LevelScale.expected_height_le_scale_support line 648
  71. lemma OAI.PlanarUnitDistances.NormalizedScale.avg_congr_support line 673
  72. theorem OAI.PlanarUnitDistances.NormalizedScale.coordinates line 682