OAI/Combinatorics/StripMass/Basic.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.rho line 14

    Also declared: ComparatorChallenges/CriticalStripMass.lean:13 (same declaration text).

  2. def OAI.CriticalStrip.c line 15

    Also declared: ComparatorChallenges/CriticalStripMass.lean:14 (same declaration text).

  3. def OAI.CriticalStrip.lambda line 16

    Also declared: ComparatorChallenges/CriticalStripMass.lean:15 (same declaration text).

  4. def OAI.CriticalStrip.d line 17

    Also declared: ComparatorChallenges/CriticalStripMass.lean:16 (same declaration text).

  5. def OAI.CriticalStrip.C line 18

    Also declared: ComparatorChallenges/CriticalStripMass.lean:17 (same declaration text).

  6. def OAI.CriticalStrip.eta line 19

    Also declared: ComparatorChallenges/CriticalStripMass.lean:18 (same declaration text).

  7. abbrev OAI.CriticalStrip.Triangle line 21

    Also declared: ComparatorChallenges/CriticalStripMass.lean:20 (same declaration text).

  8. def OAI.CriticalStrip.up line 23

    Also declared: ComparatorChallenges/CriticalStripMass.lean:22 (same declaration text).

  9. def OAI.CriticalStrip.down line 24

    Also declared: ComparatorChallenges/CriticalStripMass.lean:23 (same declaration text).

  10. def OAI.CriticalStrip.upDownAdjacent line 26

    Also declared: ComparatorChallenges/CriticalStripMass.lean:25 (same declaration text).

  11. def OAI.CriticalStrip.adjacent line 31

    Also declared: ComparatorChallenges/CriticalStripMass.lean:30 (same declaration text).

  12. def OAI.CriticalStrip.IsPath line 34

    Also declared: ComparatorChallenges/CriticalStripMass.lean:33 (same declaration text).

  13. def OAI.CriticalStrip.archWeight line 39

    Also declared: ComparatorChallenges/CriticalStripMass.lean:38 (same declaration text).

  14. def OAI.CriticalStrip.bridgeWeight line 44

    Also declared: ComparatorChallenges/CriticalStripMass.lean:43 (same declaration text).

  15. def OAI.CriticalStrip.K line 48

    Also declared: ComparatorChallenges/CriticalStripMass.lean:47 (same declaration text).

  16. def OAI.CriticalStrip.bridgeKernel line 49

    Also declared: ComparatorChallenges/CriticalStripMass.lean:48 (same declaration text).

  17. def OAI.CriticalStrip.archMass line 50

    Also declared: ComparatorChallenges/CriticalStripMass.lean:49 (same declaration text).

  18. def OAI.CriticalStrip.bridgeMass line 51

    Also declared: ComparatorChallenges/CriticalStripMass.lean:50 (same declaration text).

  19. def OAI.CriticalStrip.moment line 52

    Also declared: ComparatorChallenges/CriticalStripMass.lean:51 (same declaration text).

  20. def OAI.CriticalStrip.StripSumsFinite line 55

    Also declared: ComparatorChallenges/CriticalStripMass.lean:54 (same declaration text).

  21. def OAI.CriticalStrip.Comparable line 62

    Also declared: ComparatorChallenges/CriticalStripMass.lean:61 (same declaration text).

  22. def OAI.CriticalStrip.CriticalStripMass line 67

    Also declared: ComparatorChallenges/CriticalStripMass.lean:66 (same declaration text).

  23. def OAI.CriticalStrip.homogeneousQ line 76
  24. def OAI.CriticalStrip.harmonicCoordinate line 80
  25. def OAI.CriticalStrip.HasProjection line 82
  26. def OAI.CriticalStrip.MonicProblem line 88
  27. def OAI.CriticalStrip.omega line 92
  28. def OAI.CriticalStrip.pairKernel line 94
  29. def OAI.CriticalStrip.orderedDomain line 96
  30. def OAI.CriticalStrip.density line 99
  31. def OAI.CriticalStrip.normalizer line 102
  32. def OAI.CriticalStrip.expectation line 104
  33. def OAI.CriticalStrip.reflectionProduct line 107
  34. def OAI.CriticalStrip.momentIntegrand line 110
  35. def OAI.CriticalStrip.PositiveIntegralCore line 115
  36. theorem OAI.CriticalStrip.omega_nonneg line 123
  37. theorem OAI.CriticalStrip.omega_pos line 127
  38. theorem OAI.CriticalStrip.omega_le_rpow line 137
  39. theorem OAI.CriticalStrip.measurable_omega line 156
  40. theorem OAI.CriticalStrip.integrableOn_omega line 160
  41. theorem OAI.CriticalStrip.pairKernel_pos line 168
  42. theorem OAI.CriticalStrip.pairKernel_nonneg line 173
  43. theorem OAI.CriticalStrip.pairKernel_le_one line 178
  44. theorem OAI.CriticalStrip.density_pos line 186
  45. theorem OAI.CriticalStrip.density_le_product line 196
  46. theorem OAI.CriticalStrip.measurable_density line 210
  47. theorem OAI.CriticalStrip.isOpen_orderedDomain line 220
  48. theorem OAI.CriticalStrip.integrableOn_density line 237
  49. theorem OAI.CriticalStrip.orderedDomain_nonempty line 249
  50. theorem OAI.CriticalStrip.normalizer_pos line 261
  51. theorem OAI.CriticalStrip.integrableOn_power_omega line 276
  52. theorem OAI.CriticalStrip.integrableOn_coordinate_weight line 290
  53. def OAI.CriticalStrip.inverseHalfSum line 320
  54. theorem OAI.CriticalStrip.integrableOn_inverseHalfSum_density line 322
  55. theorem OAI.CriticalStrip.abs_one_sub_prod_le line 327
  56. theorem OAI.CriticalStrip.abs_reflectionFactor_le_one line 343
  57. theorem OAI.CriticalStrip.abs_one_sub_reflectionFactor_le line 353
  58. theorem OAI.CriticalStrip.abs_reflectionProduct_le_one line 368
  59. theorem OAI.CriticalStrip.reflectionProduct_endpoint_bound line 374
  60. theorem OAI.CriticalStrip.measurable_reflectionProduct line 384
  61. theorem OAI.CriticalStrip.integrableOn_reflectionProduct_density line 391
  62. theorem OAI.CriticalStrip.integrableOn_deficit_density line 400
  63. theorem OAI.CriticalStrip.expectation_deficit line 404
  64. theorem OAI.CriticalStrip.expectation_nonneg line 412