OAI/Combinatorics/StripMass/ArchIntegrals.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.pointwiseArchIntegral_lower line 13
  2. theorem OAI.CriticalStrip.pointwiseArchIntegrand_two_majorants line 62
  3. theorem OAI.CriticalStrip.pointwiseArchIntegral_upper line 92
  4. theorem OAI.CriticalStrip.integrable_jointArchIntegrand line 175
  5. theorem OAI.CriticalStrip.integrableOn_pointwiseArchIntegral_density line 193
  6. theorem OAI.CriticalStrip.expectation_pointwiseArchIntegrand line 198
  7. theorem OAI.CriticalStrip.integral_momentIntegrand_eq_expectation line 214
  8. theorem OAI.CriticalStrip.fourthRoot_sum_le_sum line 230
  9. theorem OAI.CriticalStrip.inverseQuarterSum_le_inverseHalfSum line 243
  10. theorem OAI.CriticalStrip.integrableOn_inverseQuarterSum_density line 253
  11. theorem OAI.CriticalStrip.integrableOn_inverseQuarterCoordinate_density line 263
  12. theorem OAI.CriticalStrip.expectation_mono line 273
  13. theorem OAI.CriticalStrip.expectation_const_mul line 282
  14. theorem OAI.CriticalStrip.integral_inverse_comparison line 288
  15. def OAI.CriticalStrip.bandRank line 317
  16. def OAI.CriticalStrip.bandVertex line 319
  17. theorem OAI.CriticalStrip.bandVertex_band line 322
  18. theorem OAI.CriticalStrip.bandRank_bandVertex line 325
  19. theorem OAI.CriticalStrip.bandVertex_bandRank line 330
  20. theorem OAI.CriticalStrip.bandRank_up line 336
  21. theorem OAI.CriticalStrip.bandRank_down line 337
  22. theorem OAI.CriticalStrip.band_adjacent_iff line 340
  23. def OAI.CriticalStrip.unitAdjacent line 349
  24. theorem OAI.CriticalStrip.int_chain_directed line 351
  25. theorem OAI.CriticalStrip.int_chain_direction line 367
  26. theorem OAI.CriticalStrip.directed_chain_eq_range line 377
  27. def OAI.CriticalStrip.integerLinePath line 402
  28. theorem OAI.CriticalStrip.integerLinePath_length line 405
  29. theorem OAI.CriticalStrip.integerLinePath_head line 408
  30. theorem OAI.CriticalStrip.integerLinePath_last line 411
  31. theorem OAI.CriticalStrip.integerLinePath_nodup line 419
  32. theorem OAI.CriticalStrip.integerLinePath_chain line 424