OAI/Combinatorics/StripMass/ReflectionFractions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.reflection_partialFractions_distinct line 13
  2. lemma OAI.CriticalStrip.integral_unitCube_cons line 120
  3. lemma OAI.CriticalStrip.integrable_unitCube_cons line 130
  4. lemma OAI.CriticalStrip.integrable_unitCube_of_abs_le_weights line 139
  5. lemma OAI.CriticalStrip.reflection_with_density_cons line 148
  6. lemma OAI.CriticalStrip.lagrange_reverse_denominator_sum line 163
  7. def OAI.CriticalStrip.reflectionMomentKernel line 186
  8. lemma OAI.CriticalStrip.measurable_reflectionMomentKernel line 189
  9. lemma OAI.CriticalStrip.abs_reflectionMomentKernel_le_weights line 196
  10. lemma OAI.CriticalStrip.integrable_reflectionMomentKernel line 218
  11. lemma OAI.CriticalStrip.reflectionMomentKernel_sum_swaps line 224
  12. lemma OAI.CriticalStrip.integral_reflectionMomentKernel_zero line 260
  13. theorem OAI.CriticalStrip.reflection_expectation_moments line 289
  14. def OAI.CriticalStrip.meanCharacteristic line 310
  15. lemma OAI.CriticalStrip.integrable_coordinateProduct_density line 315
  16. lemma OAI.CriticalStrip.meanCharacteristic_eval line 322
  17. lemma OAI.CriticalStrip.meanCharacteristic_natDegree line 341
  18. lemma OAI.CriticalStrip.polynomial_transformedBasis line 349
  19. def OAI.CriticalStrip.reflectionResidueKernel line 369
  20. lemma OAI.CriticalStrip.measurable_reflectionResidueKernel line 372
  21. lemma OAI.CriticalStrip.reflectionResidueKernel_perm line 380
  22. lemma OAI.CriticalStrip.reflectionResidueKernel_cons line 387
  23. lemma OAI.CriticalStrip.abs_reflectionResidueKernel_zero_le line 394
  24. lemma OAI.CriticalStrip.abs_reflectionResidueKernel_le line 419
  25. lemma OAI.CriticalStrip.integrable_reflectionResidueKernel line 431