OAI/Combinatorics/StripMass/MomentGrowth.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.positiveLaw_inverseQuarterSum_growth_upper line 13
  2. theorem OAI.CriticalStrip.positiveLaw_least_inverseQuarter_growth_lower line 49
  3. theorem OAI.CriticalStrip.positive_arch_integral_growth line 86
  4. lemma OAI.CriticalStrip.pairKernel_symm line 108
  5. lemma OAI.CriticalStrip.prod_upper_square line 114
  6. lemma OAI.CriticalStrip.prod_upper_perm line 140
  7. lemma OAI.CriticalStrip.density_perm_of_nonneg line 160
  8. lemma OAI.CriticalStrip.density_zero_of_not_injective line 168
  9. abbrev OAI.CriticalStrip.unitCubeMeasure line 183
  10. lemma OAI.CriticalStrip.ae_unitCube line 186
  11. lemma OAI.CriticalStrip.unitCube_restrict_ordered line 192
  12. lemma OAI.CriticalStrip.integral_symmetric_unitCube line 199
  13. lemma OAI.CriticalStrip.integral_density_unitCube line 250
  14. lemma OAI.CriticalStrip.density_cons line 256
  15. lemma OAI.CriticalStrip.density_nonneg_of_nonneg line 263
  16. lemma OAI.CriticalStrip.density_cube_le_product line 269
  17. lemma OAI.CriticalStrip.integrable_density_unitCube line 280
  18. lemma OAI.CriticalStrip.integrable_cube_mul_density line 287
  19. lemma OAI.CriticalStrip.reflectionProduct_perm line 297
  20. lemma OAI.CriticalStrip.expectation_reflection_unitCube line 301
  21. def OAI.CriticalStrip.reflectionResidue line 312
  22. lemma OAI.CriticalStrip.reflectionResidue_perm line 315
  23. lemma OAI.CriticalStrip.reflectionResidue_zero_cons line 326
  24. lemma OAI.CriticalStrip.reflectionResidue_density_cons line 335