OAI/Geometry/UnitDistances/Cross.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PlanarUnitDistances.FiniteLaw.Law line 9
  2. def OAI.PlanarUnitDistances.FiniteLaw.avg line 16
  3. def OAI.PlanarUnitDistances.FiniteLaw.event line 18
  4. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_congr line 22
  5. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_ite line 25
  6. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_const line 32
  7. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_add line 34
  8. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_sub line 36
  9. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_smul line 38
  10. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_mono line 40
  11. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_nonneg line 42
  12. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_le_const line 44
  13. lemma OAI.PlanarUnitDistances.FiniteLaw.const_le_avg line 46
  14. lemma OAI.PlanarUnitDistances.FiniteLaw.event_nonneg line 48
  15. lemma OAI.PlanarUnitDistances.FiniteLaw.event_le_one line 51
  16. lemma OAI.PlanarUnitDistances.FiniteLaw.event_compl line 54
  17. lemma OAI.PlanarUnitDistances.FiniteLaw.event_mono line 62
  18. lemma OAI.PlanarUnitDistances.FiniteLaw.event_union_le line 65
  19. def OAI.PlanarUnitDistances.FiniteLaw.pair line 72
  20. lemma OAI.PlanarUnitDistances.FiniteLaw.pair_avg line 77
  21. lemma OAI.PlanarUnitDistances.FiniteLaw.pair_fst line 80
  22. lemma OAI.PlanarUnitDistances.FiniteLaw.pair_snd line 83
  23. lemma OAI.PlanarUnitDistances.FiniteLaw.pair_prod line 86
  24. lemma OAI.PlanarUnitDistances.FiniteLaw.pair_union line 90
  25. def OAI.PlanarUnitDistances.StrictCross.Adj line 109
  26. lemma OAI.PlanarUnitDistances.StrictCross.symm line 112
  27. lemma OAI.PlanarUnitDistances.StrictCross.same_row line 117
  28. lemma OAI.PlanarUnitDistances.StrictCross.swap_iff line 131
  29. lemma OAI.PlanarUnitDistances.StrictCross.same_column line 135
  30. lemma OAI.PlanarUnitDistances.StrictCross.corners line 142
  31. lemma OAI.PlanarUnitDistances.StrictCross.third_off_row line 153
  32. lemma OAI.PlanarUnitDistances.StrictCross.three_independent line 161
  33. theorem OAI.PlanarUnitDistances.StrictCross.classification line 170
  34. def OAI.PlanarUnitDistances.StrictCross.coefficient line 210
  35. lemma OAI.PlanarUnitDistances.StrictCross.coefficient_lower line 213
  36. lemma OAI.PlanarUnitDistances.StrictCross.score_polynomial line 216
  37. def OAI.PlanarUnitDistances.StarScore.frequency line 232
  38. def OAI.PlanarUnitDistances.StarScore.variation line 233
  39. def OAI.PlanarUnitDistances.StarScore.slot line 235
  40. def OAI.PlanarUnitDistances.StarScore.score line 241
  41. lemma OAI.PlanarUnitDistances.StarScore.frequency_nonneg line 244
  42. lemma OAI.PlanarUnitDistances.StarScore.frequency_le_one line 245
  43. lemma OAI.PlanarUnitDistances.StarScore.variation_nonneg line 246
  44. lemma OAI.PlanarUnitDistances.StarScore.variation_le_half line 250
  45. lemma OAI.PlanarUnitDistances.StarScore.coefficient_upper line 253
  46. lemma OAI.PlanarUnitDistances.StarScore.coefficient_nonneg line 255
  47. lemma OAI.PlanarUnitDistances.StarScore.slot_lower line 258
  48. lemma OAI.PlanarUnitDistances.StarScore.slot_upper line 263
  49. lemma OAI.PlanarUnitDistances.StarScore.mismatch line 268
  50. lemma OAI.PlanarUnitDistances.StarScore.score_lower line 285
  51. lemma OAI.PlanarUnitDistances.StarScore.score_ge_half_neg line 298
  52. theorem OAI.PlanarUnitDistances.StarScore.determined line 302
  53. theorem OAI.PlanarUnitDistances.StarScore.constant_good line 337
  54. theorem OAI.PlanarUnitDistances.StarScore.constant_bit line 357
  55. def OAI.PlanarUnitDistances.FiniteLaw.fiberMass line 373
  56. lemma OAI.PlanarUnitDistances.FiniteLaw.fiberMass_eq line 376
  57. lemma OAI.PlanarUnitDistances.FiniteLaw.fiberMass_nonneg line 384
  58. lemma OAI.PlanarUnitDistances.FiniteLaw.atom_le_fiber line 387
  59. lemma OAI.PlanarUnitDistances.FiniteLaw.fiberMass_total line 393
  60. def OAI.PlanarUnitDistances.FiniteLaw.push line 399
  61. lemma OAI.PlanarUnitDistances.FiniteLaw.push_avg line 404
  62. def OAI.PlanarUnitDistances.FiniteLaw.cond line 415
  63. lemma OAI.PlanarUnitDistances.FiniteLaw.cond_weight line 434
  64. lemma OAI.PlanarUnitDistances.FiniteLaw.cond_tower line 450
  65. lemma OAI.PlanarUnitDistances.FiniteLaw.cond_support line 462
  66. lemma OAI.PlanarUnitDistances.FiniteLaw.cond_event_fiber line 468
  67. lemma OAI.PlanarUnitDistances.FiniteLaw.push_avg_mono_pos line 479
  68. lemma OAI.PlanarUnitDistances.FiniteLaw.cond_event_tower line 488