OAI/Combinatorics/HoneycombChords/StripExhaustion.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Finite rectangle exhaustion of strict honeycomb bridges.

  1. def OAI.CriticalHoneycomb.StripExhaustion.turn line 16
  2. lemma OAI.CriticalHoneycomb.StripExhaustion.turn_injective line 18
  3. lemma OAI.CriticalHoneycomb.StripExhaustion.turn_adj line 24
  4. lemma OAI.CriticalHoneycomb.StripExhaustion.adj_symm line 29
  5. lemma OAI.CriticalHoneycomb.StripExhaustion.reverse_chain line 33
  6. def OAI.CriticalHoneycomb.StripExhaustion.reflected line 37
  7. lemma OAI.CriticalHoneycomb.StripExhaustion.reflected_injective line 39
  8. lemma OAI.CriticalHoneycomb.StripExhaustion.reflected_length line 45
  9. lemma OAI.CriticalHoneycomb.StripExhaustion.reflected_last line 47
  10. def OAI.CriticalHoneycomb.StripExhaustion.terminal line 50
  11. lemma OAI.CriticalHoneycomb.StripExhaustion.terminal_last line 51
  12. lemma OAI.CriticalHoneycomb.StripExhaustion.reflected_head line 53
  13. lemma OAI.CriticalHoneycomb.StripExhaustion.finite_trace_bound line 57
  14. lemma OAI.CriticalHoneycomb.StripExhaustion.reflected_trace line 72
  15. lemma OAI.CriticalHoneycomb.StripExhaustion.terminal_bound line 90
  16. def OAI.CriticalHoneycomb.StripExhaustion.exitIndex line 102
  17. lemma OAI.CriticalHoneycomb.StripExhaustion.exitIndex_value line 105
  18. def OAI.CriticalHoneycomb.StripExhaustion.reflectedChord line 112
  19. theorem OAI.CriticalHoneycomb.StripExhaustion.strip_finite_sum_le line 128
  20. lemma OAI.CriticalHoneycomb.StripExhaustion.real_strip_summable line 154
  21. lemma OAI.CriticalHoneycomb.StripExhaustion.real_strip_tsum_le line 161
  22. theorem OAI.CriticalHoneycomb.StripExhaustion.bridgeMass_le_one line 172
  23. theorem OAI.CriticalHoneycomb.StripExhaustion.bridgeMass_finite line 183
  24. def OAI.CriticalHoneycomb.StripExhaustion.ConfinedAt line 195
  25. instance OAI.CriticalHoneycomb.StripExhaustion.confinedAtDecidable line 198
  26. def OAI.CriticalHoneycomb.StripExhaustion.placements line 201
  27. def OAI.CriticalHoneycomb.StripExhaustion.placementFraction line 205
  28. lemma OAI.CriticalHoneycomb.StripExhaustion.placements_nonnegative line 208
  29. lemma OAI.CriticalHoneycomb.StripExhaustion.placements_le line 213
  30. lemma OAI.CriticalHoneycomb.StripExhaustion.placementFraction_nonnegative line 221
  31. lemma OAI.CriticalHoneycomb.StripExhaustion.placementFraction_le_one line 223
  32. def OAI.CriticalHoneycomb.StripExhaustion.interiorPlacement line 228
  33. lemma OAI.CriticalHoneycomb.StripExhaustion.interiorPlacement_injective line 230
  34. lemma OAI.CriticalHoneycomb.StripExhaustion.interior_confined line 236
  35. lemma OAI.CriticalHoneycomb.StripExhaustion.placements_lower line 245
  36. lemma OAI.CriticalHoneycomb.StripExhaustion.central_fraction_limit line 264
  37. lemma OAI.CriticalHoneycomb.StripExhaustion.placementFraction_limit line 278
  38. def OAI.CriticalHoneycomb.StripExhaustion.averagingMass line 289
  39. theorem OAI.CriticalHoneycomb.StripExhaustion.averagingMass_limit line 292
  40. abbrev OAI.CriticalHoneycomb.StripExhaustion.RectAllAt line 309
  41. def OAI.CriticalHoneycomb.StripExhaustion.unplace line 312
  42. lemma OAI.CriticalHoneycomb.StripExhaustion.unplace_length line 331
  43. lemma OAI.CriticalHoneycomb.StripExhaustion.unplace_confined line 333
  44. lemma OAI.CriticalHoneycomb.StripExhaustion.terminal_confined line 342
  45. def OAI.CriticalHoneycomb.StripExhaustion.exitAt line 347
  46. lemma OAI.CriticalHoneycomb.StripExhaustion.exitAt_value line 350
  47. def OAI.CriticalHoneycomb.StripExhaustion.place line 356
  48. lemma OAI.CriticalHoneycomb.StripExhaustion.turn_turn line 378
  49. lemma OAI.CriticalHoneycomb.StripExhaustion.unplace_place line 382
  50. lemma OAI.CriticalHoneycomb.StripExhaustion.rectAll_ext line 391
  51. lemma OAI.CriticalHoneycomb.StripExhaustion.place_unplace line 405
  52. def OAI.CriticalHoneycomb.StripExhaustion.placementEquiv line 413
  53. lemma OAI.CriticalHoneycomb.StripExhaustion.rectangle_one_source line 424
  54. lemma OAI.CriticalHoneycomb.StripExhaustion.confined_summable line 438
  55. lemma OAI.CriticalHoneycomb.StripExhaustion.rectangle_average_eq line 444
  56. theorem OAI.CriticalHoneycomb.StripExhaustion.physical_rectangle_average_limit line 461