OAI/Combinatorics/StripMass/ScalarBridge.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.pfaffian_eq_exterior line 16
  2. lemma OAI.CriticalStrip.Diagram.augmentedKernel_skew_complex line 36
  3. lemma OAI.CriticalStrip.Diagram.scalarNormalization_eq_exterior line 50
  4. lemma OAI.CriticalStrip.Diagram.scalarValue_eq_exterior line 78
  5. def OAI.CriticalStrip.Diagram.archPolynomialAt line 88
  6. lemma OAI.CriticalStrip.Diagram.archPolynomialAt_monic_degree line 91
  7. lemma OAI.CriticalStrip.Diagram.nextScalar_eval line 102
  8. lemma OAI.CriticalStrip.Diagram.archPolynomialAt_eval_quotient line 107
  9. lemma OAI.CriticalStrip.Diagram.infinitely_many_regular_arguments line 129
  10. theorem OAI.CriticalStrip.Diagram.archPolynomialAt_confluent line 148
  11. def OAI.CriticalStrip.PathBetween line 182
  12. lemma OAI.CriticalStrip.pathBetween_source line 186
  13. lemma OAI.CriticalStrip.adjacent_symmetric line 189
  14. lemma OAI.CriticalStrip.PathBetween.reverse line 191
  15. def OAI.CriticalStrip.translateTriangle line 199
  16. lemma OAI.CriticalStrip.translateTriangle_up line 201
  17. lemma OAI.CriticalStrip.translateTriangle_down line 203
  18. lemma OAI.CriticalStrip.translateTriangle_band line 205
  19. lemma OAI.CriticalStrip.translateTriangle_zero line 207
  20. lemma OAI.CriticalStrip.translateTriangle_add line 209
  21. lemma OAI.CriticalStrip.translateTriangle_injective line 213
  22. lemma OAI.CriticalStrip.adjacent_translate_iff line 218
  23. lemma OAI.CriticalStrip.PathBetween.translate line 222
  24. lemma OAI.CriticalStrip.pathBetween_translate_iff line 233
  25. def OAI.CriticalStrip.translatePaths line 239
  26. def OAI.CriticalStrip.betweenArchWeight line 246
  27. def OAI.CriticalStrip.betweenArchKernel line 249
  28. lemma OAI.CriticalStrip.betweenArchWeight_nonneg line 251
  29. lemma OAI.CriticalStrip.betweenArchWeight_translate line 258
  30. theorem OAI.CriticalStrip.betweenArchKernel_eq line 268
  31. lemma OAI.CriticalStrip.summable_betweenArchWeight_iff line 272
  32. lemma OAI.CriticalStrip.betweenArchWeight_reverse line 277
  33. def OAI.CriticalStrip.cutArchWeight line 286
  34. lemma OAI.CriticalStrip.cutArchWeight_nonneg line 289
  35. lemma OAI.CriticalStrip.cutArchWeight_path_sum line 292
  36. lemma OAI.CriticalStrip.summable_add_diagonal_iff line 301
  37. lemma OAI.CriticalStrip.tsum_add_diagonal line 316
  38. theorem OAI.CriticalStrip.cutArchWeight_summable_iff line 336
  39. theorem OAI.CriticalStrip.physical_moment_eq_cut_sum line 351
  40. def OAI.CriticalStrip.steppedDomain line 368
  41. def OAI.CriticalStrip.stepArchWeight line 373
  42. def OAI.CriticalStrip.stepArchKernel line 376
  43. lemma OAI.CriticalStrip.stepArchWeight_nonneg line 378
  44. lemma OAI.CriticalStrip.stepArchWeight_le line 385
  45. lemma OAI.CriticalStrip.stepArchWeight_reverse line 392
  46. def OAI.CriticalStrip.reversePaths line 396
  47. lemma OAI.CriticalStrip.stepArchKernel_reverse line 402
  48. lemma OAI.CriticalStrip.betweenArchWeight_mono line 407
  49. lemma OAI.CriticalStrip.betweenArchWeight_restrict line 417
  50. lemma OAI.CriticalStrip.stepArchWeight_translate line 430
  51. def OAI.CriticalStrip.stepCutArchWeight line 444
  52. lemma OAI.CriticalStrip.stepCutArchWeight_nonneg line 447
  53. lemma OAI.CriticalStrip.stepCutArchWeight_le line 450
  54. lemma OAI.CriticalStrip.stepCutArchWeight_summable line 453
  55. lemma OAI.CriticalStrip.eventually_stepContains line 458
  56. lemma OAI.CriticalStrip.eventually_stepExcludes line 473
  57. lemma OAI.CriticalStrip.stepArchWeight_eventually_tall line 486
  58. lemma OAI.CriticalStrip.stepArchWeight_eventually_short line 497
  59. theorem OAI.CriticalStrip.step_cut_mass_tall_limit line 506
  60. theorem OAI.CriticalStrip.step_cut_mass_short_limit line 519