OAI/Geometry/UnitDistances/Wedges.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.FiniteLaw.dependent line 11
  2. def OAI.PlanarUnitDistances.FiniteLaw.mix line 16
  3. def OAI.PlanarUnitDistances.FiniteLaw.tensor line 24
  4. lemma OAI.PlanarUnitDistances.FiniteLaw.dependent_avg line 32
  5. lemma OAI.PlanarUnitDistances.FiniteLaw.mix_avg line 35
  6. lemma OAI.PlanarUnitDistances.FiniteLaw.tensor_event line 39
  7. lemma OAI.PlanarUnitDistances.FiniteLaw.tensor_coordinate line 53
  8. lemma OAI.PlanarUnitDistances.FiniteLaw.tensor_union_le line 67
  9. lemma OAI.PlanarUnitDistances.FiniteLaw.tensor_dependent line 72
  10. lemma OAI.PlanarUnitDistances.FiniteLaw.independent_push line 89
  11. lemma OAI.PlanarUnitDistances.FiniteLaw.law_ext line 103
  12. lemma OAI.PlanarUnitDistances.FiniteLaw.push_dependent_fst line 110
  13. lemma OAI.PlanarUnitDistances.FiniteLaw.push_dependent_snd line 118
  14. lemma OAI.PlanarUnitDistances.FiniteLaw.tensor_mixture line 126
  15. def OAI.PlanarUnitDistances.WedgeLaw.law line 142
  16. lemma OAI.PlanarUnitDistances.WedgeLaw.average line 145
  17. lemma OAI.PlanarUnitDistances.WedgeLaw.first line 149
  18. lemma OAI.PlanarUnitDistances.WedgeLaw.second line 159
  19. lemma OAI.PlanarUnitDistances.WedgeLaw.first_point line 169
  20. lemma OAI.PlanarUnitDistances.WedgeLaw.second_point line 174
  21. lemma OAI.PlanarUnitDistances.WedgeLaw.mismatch line 179
  22. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.left_val line 196
  23. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.right_val line 200
  24. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.row_weight line 202
  25. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.col_weight line 209
  26. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.row_val line 216
  27. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.col_val line 220
  28. def OAI.PlanarUnitDistances.TemplateCoupling.joint line 233
  29. def OAI.PlanarUnitDistances.TemplateCoupling.templates line 234
  30. def OAI.PlanarUnitDistances.TemplateCoupling.slice line 235
  31. lemma OAI.PlanarUnitDistances.TemplateCoupling.slice_weight line 238
  32. lemma OAI.PlanarUnitDistances.TemplateCoupling.template_val line 241
  33. lemma OAI.PlanarUnitDistances.TemplateCoupling.slice_avg line 247
  34. lemma OAI.PlanarUnitDistances.TemplateCoupling.slice_event line 254
  35. lemma OAI.PlanarUnitDistances.TemplateCoupling.slice_right_weight line 259
  36. lemma OAI.PlanarUnitDistances.TemplateCoupling.col_eq line 263
  37. lemma OAI.PlanarUnitDistances.TemplateCoupling.center_statistic line 279
  38. lemma OAI.PlanarUnitDistances.TemplateCoupling.center_variation line 299
  39. lemma OAI.PlanarUnitDistances.TemplateCoupling.center_score line 302
  40. def OAI.PlanarUnitDistances.CrossSampling.crossMass line 315
  41. def OAI.PlanarUnitDistances.CrossSampling.rowMass line 316
  42. def OAI.PlanarUnitDistances.CrossSampling.colMass line 317
  43. def OAI.PlanarUnitDistances.CrossSampling.Bad line 319
  44. def OAI.PlanarUnitDistances.CrossSampling.Corner line 322
  45. def OAI.PlanarUnitDistances.CrossSampling.LowRow line 325
  46. def OAI.PlanarUnitDistances.CrossSampling.LowCol line 327
  47. def OAI.PlanarUnitDistances.CrossSampling.HeavyAvoid line 329
  48. lemma OAI.PlanarUnitDistances.CrossSampling.atom_eq line 332
  49. lemma OAI.PlanarUnitDistances.CrossSampling.row_le_cross_add_atom line 336
  50. lemma OAI.PlanarUnitDistances.CrossSampling.col_le_cross_add_atom line 344
  51. lemma OAI.PlanarUnitDistances.CrossSampling.bad_decomposition line 354
  52. lemma OAI.PlanarUnitDistances.CrossSampling.low_fiber_bound line 395
  53. lemma OAI.PlanarUnitDistances.CrossSampling.heavyavoid_bound line 422
  54. abbrev OAI.PlanarUnitDistances.CrossSampling.Rest line 460
  55. def OAI.PlanarUnitDistances.CrossSampling.fillTwo line 461
  56. lemma OAI.PlanarUnitDistances.CrossSampling.fillTwo_i line 466
  57. lemma OAI.PlanarUnitDistances.CrossSampling.fillTwo_j line 469
  58. lemma OAI.PlanarUnitDistances.CrossSampling.fillTwo_rest line 472
  59. lemma OAI.PlanarUnitDistances.CrossSampling.card_neq line 477
  60. lemma OAI.PlanarUnitDistances.CrossSampling.card_rest line 480
  61. lemma OAI.PlanarUnitDistances.CrossSampling.corner_bound line 484
  62. lemma OAI.PlanarUnitDistances.CrossSampling.sampling_bound line 518
  63. def OAI.PlanarUnitDistances.CrossTemplates.Candidates line 548
  64. def OAI.PlanarUnitDistances.CrossTemplates.Failure line 551
  65. lemma OAI.PlanarUnitDistances.CrossTemplates.all_cross_lower line 554
  66. theorem OAI.PlanarUnitDistances.CrossTemplates.failure_bound line 572
  67. lemma OAI.PlanarUnitDistances.CrossTemplates.miss_markov line 604
  68. theorem OAI.PlanarUnitDistances.CrossTemplates.candidate_miss line 617
  69. def OAI.PlanarUnitDistances.CommonTemplate.posteriorState line 645
  70. def OAI.PlanarUnitDistances.CommonTemplate.historyLaw line 648
  71. lemma OAI.PlanarUnitDistances.CommonTemplate.posterior_val line 651
  72. lemma OAI.PlanarUnitDistances.CommonTemplate.mixture_val line 665
  73. lemma OAI.PlanarUnitDistances.CommonTemplate.event_mem_mass line 674
  74. lemma OAI.PlanarUnitDistances.CommonTemplate.witnesses_mass line 683
  75. theorem OAI.PlanarUnitDistances.CommonTemplate.actual_transfer line 704
  76. theorem OAI.PlanarUnitDistances.CommonTemplate.aggregate_score line 746