OAI/Geometry/UnitDistances/Transfer.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.RestrictedTransfer.mass line 8
  2. lemma OAI.PlanarUnitDistances.RestrictedTransfer.mass_nonneg line 14
  3. lemma OAI.PlanarUnitDistances.RestrictedTransfer.mass_mono line 17
  4. lemma OAI.PlanarUnitDistances.RestrictedTransfer.mass_compl line 19
  5. lemma OAI.PlanarUnitDistances.RestrictedTransfer.mass_union_le line 24
  6. lemma OAI.PlanarUnitDistances.RestrictedTransfer.atom_le_mass line 31
  7. lemma OAI.PlanarUnitDistances.RestrictedTransfer.mass_le_one line 34
  8. abbrev OAI.PlanarUnitDistances.RestrictedTransfer.State line 40
  9. def OAI.PlanarUnitDistances.RestrictedTransfer.row line 42
  10. def OAI.PlanarUnitDistances.RestrictedTransfer.col line 43
  11. def OAI.PlanarUnitDistances.RestrictedTransfer.Permitted line 45
  12. lemma OAI.PlanarUnitDistances.RestrictedTransfer.high_row_unique line 48
  13. lemma OAI.PlanarUnitDistances.RestrictedTransfer.high_col_unique line 61
  14. def OAI.PlanarUnitDistances.RestrictedTransfer.rowException line 74
  15. def OAI.PlanarUnitDistances.RestrictedTransfer.colException line 77
  16. def OAI.PlanarUnitDistances.RestrictedTransfer.smallException line 80
  17. def OAI.PlanarUnitDistances.RestrictedTransfer.exception line 84
  18. lemma OAI.PlanarUnitDistances.RestrictedTransfer.rowException_mass line 87
  19. lemma OAI.PlanarUnitDistances.RestrictedTransfer.colException_mass line 93
  20. lemma OAI.PlanarUnitDistances.RestrictedTransfer.smallException_mass line 100
  21. lemma OAI.PlanarUnitDistances.RestrictedTransfer.exception_mass line 126
  22. lemma OAI.PlanarUnitDistances.RestrictedTransfer.outside_exception_mem line 137
  23. def OAI.PlanarUnitDistances.RestrictedTransfer.historyMass line 166
  24. def OAI.PlanarUnitDistances.RestrictedTransfer.posterior line 168
  25. def OAI.PlanarUnitDistances.RestrictedTransfer.statePosterior line 170
  26. lemma OAI.PlanarUnitDistances.RestrictedTransfer.historyMass_nonneg line 174
  27. lemma OAI.PlanarUnitDistances.RestrictedTransfer.historyMass_pos line 177
  28. lemma OAI.PlanarUnitDistances.RestrictedTransfer.posterior_nonneg line 184
  29. lemma OAI.PlanarUnitDistances.RestrictedTransfer.posterior_stationary line 189
  30. lemma OAI.PlanarUnitDistances.RestrictedTransfer.posterior_function line 202
  31. lemma OAI.PlanarUnitDistances.RestrictedTransfer.statePosterior_nonneg line 219
  32. lemma OAI.PlanarUnitDistances.RestrictedTransfer.statePosterior_sum line 228
  33. lemma OAI.PlanarUnitDistances.RestrictedTransfer.statePosterior_mass line 235
  34. lemma OAI.PlanarUnitDistances.RestrictedTransfer.actual_exception_mass line 247
  35. theorem OAI.PlanarUnitDistances.RestrictedTransfer.restricted_transfer line 276
  36. def OAI.PlanarUnitDistances.RestrictedTransfer.centerMixture line 351
  37. lemma OAI.PlanarUnitDistances.RestrictedTransfer.centerMixture_mass line 356
  38. theorem OAI.PlanarUnitDistances.RestrictedTransfer.edge_template_transfer line 366
  39. def OAI.PlanarUnitDistances.CrossStructure.Consistent line 419
  40. lemma OAI.PlanarUnitDistances.CrossStructure.consistent_adj line 422
  41. lemma OAI.PlanarUnitDistances.CrossStructure.consistent_symm line 426
  42. lemma OAI.PlanarUnitDistances.CrossStructure.bit_unique line 430
  43. lemma OAI.PlanarUnitDistances.CrossStructure.bit_true line 432
  44. lemma OAI.PlanarUnitDistances.CrossStructure.bit_false line 434
  45. def OAI.PlanarUnitDistances.CrossStructure.Shape line 437
  46. lemma OAI.PlanarUnitDistances.CrossStructure.card_pair_le line 443
  47. lemma OAI.PlanarUnitDistances.CrossStructure.card_triple_le line 447
  48. lemma OAI.PlanarUnitDistances.CrossStructure.pair_coord_inj line 453
  49. lemma OAI.PlanarUnitDistances.CrossStructure.determined_of_inj line 468
  50. theorem OAI.PlanarUnitDistances.CrossStructure.witnesses line 478
  51. lemma OAI.PlanarUnitDistances.FiniteLaw.cond_tower_dep line 565
  52. def OAI.PlanarUnitDistances.FiniteStarCoupling.left line 584
  53. def OAI.PlanarUnitDistances.FiniteStarCoupling.right line 585
  54. def OAI.PlanarUnitDistances.FiniteStarCoupling.row line 586
  55. def OAI.PlanarUnitDistances.FiniteStarCoupling.col line 587
  56. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.row_avg line 589
  57. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.col_avg line 594
  58. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.row_event line 599
  59. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.col_event line 603
  60. def OAI.PlanarUnitDistances.FiniteStarCoupling.DP line 608
  61. def OAI.PlanarUnitDistances.FiniteStarCoupling.DQ line 610
  62. def OAI.PlanarUnitDistances.FiniteStarCoupling.VP line 612
  63. def OAI.PlanarUnitDistances.FiniteStarCoupling.VQ line 614
  64. def OAI.PlanarUnitDistances.FiniteStarCoupling.bad line 616
  65. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.vp_le line 618
  66. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.vq_le line 620
  67. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.dp_lower line 622
  68. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.dq_lower line 630
  69. theorem OAI.PlanarUnitDistances.FiniteStarCoupling.slice_score line 639
  70. def OAI.PlanarUnitDistances.RareScore.exceptional line 703
  71. def OAI.PlanarUnitDistances.RareScore.nonshared line 706
  72. lemma OAI.PlanarUnitDistances.RareScore.normal_bits line 709
  73. lemma OAI.PlanarUnitDistances.RareScore.exceptional_bits line 715
  74. lemma OAI.PlanarUnitDistances.RareScore.minority_exception line 722
  75. def OAI.PlanarUnitDistances.RareScore.ind line 729
  76. lemma OAI.PlanarUnitDistances.RareScore.ind_nonneg line 730
  77. lemma OAI.PlanarUnitDistances.RareScore.ind_le_one line 731
  78. def OAI.PlanarUnitDistances.RareScore.slot line 733
  79. lemma OAI.PlanarUnitDistances.RareScore.slot_lower line 736
  80. theorem OAI.PlanarUnitDistances.RareScore.star_lower line 759
  81. def OAI.PlanarUnitDistances.WedgeProfiles.value line 791
  82. def OAI.PlanarUnitDistances.WedgeProfiles.sign line 792
  83. lemma OAI.PlanarUnitDistances.WedgeProfiles.edge_residual line 794
  84. lemma OAI.PlanarUnitDistances.WedgeProfiles.wedge_residual line 809
  85. lemma OAI.PlanarUnitDistances.WedgeProfiles.wedge_size line 821
  86. lemma OAI.PlanarUnitDistances.FiniteLaw.event_eq_sum line 845
  87. lemma OAI.PlanarUnitDistances.FiniteLaw.event_congr line 852
  88. lemma OAI.PlanarUnitDistances.FiniteLaw.event_true line 856
  89. lemma OAI.PlanarUnitDistances.FiniteLaw.event_false line 858
  90. lemma OAI.PlanarUnitDistances.FiniteLaw.event_exists_le line 861
  91. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_sum line 878
  92. lemma OAI.PlanarUnitDistances.FiniteLaw.sum_event_fibers line 883
  93. def OAI.PlanarUnitDistances.FiniteLaw.independent line 888
  94. lemma OAI.PlanarUnitDistances.FiniteLaw.indicator_forall line 896
  95. lemma OAI.PlanarUnitDistances.FiniteLaw.independent_event line 909
  96. lemma OAI.PlanarUnitDistances.FiniteLaw.independent_all line 924
  97. lemma OAI.PlanarUnitDistances.FiniteLaw.equiv_avg line 929
  98. lemma OAI.PlanarUnitDistances.FiniteLaw.independent_split line 936
  99. lemma OAI.PlanarUnitDistances.FiniteLaw.independent_two_split line 953