OAI/Combinatorics/StripMass/SidePaths.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.rotateTriangle line 16
  2. lemma OAI.CriticalStrip.rotateTriangle_band_lt line 19
  3. lemma OAI.CriticalStrip.rotateTriangle_up line 22
  4. lemma OAI.CriticalStrip.rotateTriangle_down line 24
  5. lemma OAI.CriticalStrip.rotateTriangle_involutive line 27
  6. lemma OAI.CriticalStrip.adjacent_rotate_iff line 35
  7. lemma OAI.CriticalStrip.PathBetween.rotate line 44
  8. lemma OAI.CriticalStrip.PathBetween.append_vertex line 58
  9. def OAI.CriticalStrip.stepSideWeight line 78
  10. def OAI.CriticalStrip.stepSideKernel line 82
  11. def OAI.CriticalStrip.stepSideMass line 84
  12. lemma OAI.CriticalStrip.stepSideWeight_nonneg line 86
  13. def OAI.CriticalStrip.sideToTallBridge line 95
  14. lemma OAI.CriticalStrip.sideToTallBridge_injective line 98
  15. lemma OAI.CriticalStrip.sideToTallBridge_spec line 106
  16. lemma OAI.CriticalStrip.sideToTallBridge_weight line 123
  17. lemma OAI.CriticalStrip.bridge_all_paths_summable line 132
  18. lemma OAI.CriticalStrip.bridge_all_paths_tsum line 137
  19. theorem OAI.CriticalStrip.stepSideWeight_summable line 143
  20. theorem OAI.CriticalStrip.stepSideMass_le_tall_bridge line 159
  21. def OAI.CriticalStrip.bridgeToSide line 179
  22. lemma OAI.CriticalStrip.bridgeToSide_injective line 182
  23. lemma OAI.CriticalStrip.bridgeToSide_spec line 188
  24. lemma OAI.CriticalStrip.bridgeToSide_weight line 210
  25. theorem OAI.CriticalStrip.stepSideMass_ge_base_bridge line 221
  26. lemma OAI.CriticalStrip.stepArchKernel_translate line 251
  27. def OAI.CriticalStrip.stepCutKernel line 257
  28. def OAI.CriticalStrip.stepCutMass line 260
  29. lemma OAI.CriticalStrip.stepCutKernel_eq line 262
  30. lemma OAI.CriticalStrip.stepCutKernel_summable line 269
  31. lemma OAI.CriticalStrip.stepCutMass_eq line 274
  32. lemma OAI.CriticalStrip.tsum_prod_split_column line 280
  33. lemma OAI.CriticalStrip.tsum_array_difference line 291
  34. def OAI.CriticalStrip.stepArchLeft line 300
  35. def OAI.CriticalStrip.stepArchRight line 303
  36. theorem OAI.CriticalStrip.step_cut_divergence line 308
  37. def OAI.CriticalStrip.SteppedBoundaryFlux line 327
  38. lemma OAI.CriticalStrip.stepSideKernel_summable line 331
  39. theorem OAI.CriticalStrip.step_moment_identity line 336
  40. lemma OAI.CriticalStrip.step_sines_pos line 390
  41. theorem OAI.CriticalStrip.moment_increment_bounds_of_boundary line 396
  42. theorem OAI.CriticalStrip.increment_comparable_of_boundary line 428
  43. theorem OAI.CriticalStrip.criticalStripMass_of_physical_identities line 444