OAI/Combinatorics/StripMass/FluxWindow.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.HoneycombBranch.IsExit line 15
  2. def OAI.CriticalStrip.HoneycombBranch.exitWeight line 20
  3. def OAI.CriticalStrip.HoneycombBranch.window line 23
  4. lemma OAI.CriticalStrip.HoneycombBranch.mem_window line 26
  5. def OAI.CriticalStrip.HoneycombBranch.clip line 31
  6. def OAI.CriticalStrip.HoneycombBranch.finiteExits line 34
  7. def OAI.CriticalStrip.HoneycombBranch.physicalExits line 37
  8. def OAI.CriticalStrip.HoneycombBranch.sideExits line 40
  9. lemma OAI.CriticalStrip.HoneycombBranch.source_clip line 43
  10. lemma OAI.CriticalStrip.HoneycombBranch.finiteExit_nonempty line 48
  11. lemma OAI.CriticalStrip.HoneycombBranch.physicalExit_isExit line 54
  12. lemma OAI.CriticalStrip.HoneycombBranch.eventually_window line 61
  13. lemma OAI.CriticalStrip.HoneycombBranch.eventually_physicalExit line 69
  14. lemma OAI.CriticalStrip.HoneycombBranch.physicalExit_limit line 84
  15. lemma OAI.CriticalStrip.HoneycombBranch.crossing_column line 114
  16. lemma OAI.CriticalStrip.HoneycombBranch.sideExit_column line 120
  17. lemma OAI.CriticalStrip.HoneycombBranch.sideExit_spec line 133
  18. lemma OAI.CriticalStrip.HoneycombBranch.side_sum_bound line 149
  19. lemma OAI.CriticalStrip.HoneycombBranch.sideExit_bound line 162
  20. lemma OAI.CriticalStrip.HoneycombBranch.finite_split line 186
  21. theorem OAI.CriticalStrip.HoneycombBranch.infinite_boundary_flux line 198
  22. structure OAI.CriticalStrip.HoneycombBranch.BoundaryPorts line 227
  23. abbrev OAI.CriticalStrip.HoneycombBranch.ExitWord line 234
  24. def OAI.CriticalStrip.HoneycombBranch.ValidBoundaryPath line 238
  25. abbrev OAI.CriticalStrip.HoneycombBranch.BoundaryPath line 243
  26. def OAI.CriticalStrip.HoneycombBranch.boundaryPathWeight line 245
  27. lemma OAI.CriticalStrip.HoneycombBranch.boundaryPathWeight_nonneg line 248
  28. lemma OAI.CriticalStrip.HoneycombBranch.source_outside line 253
  29. lemma OAI.CriticalStrip.HoneycombBranch.exists_exit_port line 258
  30. def OAI.CriticalStrip.HoneycombBranch.exitPort line 263
  31. lemma OAI.CriticalStrip.HoneycombBranch.exitPort_spec line 265
  32. lemma OAI.CriticalStrip.HoneycombBranch.exitPort_terminal line 268
  33. lemma OAI.CriticalStrip.HoneycombBranch.visited_map_retract line 272
  34. def OAI.CriticalStrip.HoneycombBranch.exitToPath line 280
  35. lemma OAI.CriticalStrip.HoneycombBranch.exitToPath_injective line 296
  36. lemma OAI.CriticalStrip.HoneycombBranch.exitToPath_surjective line 309
  37. def OAI.CriticalStrip.HoneycombBranch.exitPathEquiv line 351
  38. lemma OAI.CriticalStrip.HoneycombBranch.exitPathEquiv_length line 354
  39. lemma OAI.CriticalStrip.HoneycombBranch.boundaryPath_summable_iff line 359
  40. lemma OAI.CriticalStrip.HoneycombBranch.exitWord_summable_iff line 365
  41. lemma OAI.CriticalStrip.HoneycombBranch.exit_weight_norm line 370
  42. theorem OAI.CriticalStrip.HoneycombBranch.exitWeight_summable line 377
  43. theorem OAI.CriticalStrip.HoneycombBranch.exitWeight_tsum line 390
  44. theorem OAI.CriticalStrip.HoneycombBranch.boundary_flux line 415
  45. def OAI.CriticalStrip.HoneycombBranch.steppedVertices line 433
  46. lemma OAI.CriticalStrip.HoneycombBranch.steppedVertices_embed line 436
  47. lemma OAI.CriticalStrip.HoneycombBranch.steppedVertices_bound line 441
  48. def OAI.CriticalStrip.HoneycombBranch.sidePort line 446
  49. def OAI.CriticalStrip.HoneycombBranch.stepTop line 448
  50. lemma OAI.CriticalStrip.HoneycombBranch.lower_top_turn line 450
  51. lemma OAI.CriticalStrip.HoneycombBranch.step_top_turn line 488
  52. lemma OAI.CriticalStrip.HoneycombBranch.step_side_turn line 498