OAI/Combinatorics/StripMass/LaguerreScaling.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.integral_scaledLaguerre_cutoff_inverseQuarter line 13
  2. lemma OAI.CriticalStrip.laguerre_cutoffNormalizer_pos line 33
  3. lemma OAI.CriticalStrip.scaled_quotient line 40
  4. theorem OAI.CriticalStrip.scaled_reference_cutoff_inverseQuarter line 51
  5. lemma OAI.CriticalStrip.integral_positiveLaw_cutoff line 61
  6. lemma OAI.CriticalStrip.positiveLaw_conditioned_eq line 69
  7. lemma OAI.CriticalStrip.integral_laguerreLaw_cutoff line 78
  8. lemma OAI.CriticalStrip.laguerreLaw_conditioned_eq line 88
  9. theorem OAI.CriticalStrip.positiveLaw_inverseQuarter_le_reference line 100
  10. def OAI.CriticalStrip.mobiusMap line 133
  11. lemma OAI.CriticalStrip.mobiusInverse_mem line 135
  12. lemma OAI.CriticalStrip.mobiusCoordinate_inverse line 139
  13. lemma OAI.CriticalStrip.inverse_mobiusCoordinate line 146
  14. lemma OAI.CriticalStrip.mobiusMap_mem line 153
  15. lemma OAI.CriticalStrip.mobiusMap_injOn line 158
  16. lemma OAI.CriticalStrip.mobiusMap_image line 163
  17. lemma OAI.CriticalStrip.hasDerivAt_mobiusCoordinate line 177
  18. def OAI.CriticalStrip.mobiusDifferential line 185
  19. lemma OAI.CriticalStrip.hasFDerivAt_mobiusMap line 189
  20. def OAI.CriticalStrip.mobiusJacobian line 200
  21. lemma OAI.CriticalStrip.det_mobiusDifferential line 202
  22. lemma OAI.CriticalStrip.mobiusJacobian_pos line 207
  23. theorem OAI.CriticalStrip.integral_mobiusMap line 213
  24. lemma OAI.CriticalStrip.integrableOn_mobiusMap_iff line 227
  25. lemma OAI.CriticalStrip.prod_pair_coordinates line 240
  26. def OAI.CriticalStrip.mobiusDensityConstant line 264
  27. lemma OAI.CriticalStrip.mobiusDensityConstant_pos line 267
  28. lemma OAI.CriticalStrip.prod_pairKernel_mobius line 271
  29. lemma OAI.CriticalStrip.scaledWeight_mul_lowerLikelihoodWeight line 285
  30. lemma OAI.CriticalStrip.scaledDensity_mul_lowerLikelihood line 295
  31. theorem OAI.CriticalStrip.density_mobiusMap line 315
  32. lemma OAI.CriticalStrip.jacobian_weighted_density line 331
  33. lemma OAI.CriticalStrip.integral_density_mobius_likelihood line 340
  34. lemma OAI.CriticalStrip.integrableOn_density_mobius_likelihood_iff line 348
  35. lemma OAI.CriticalStrip.mobiusLikelihood_Normalizer line 363
  36. lemma OAI.CriticalStrip.integrableOn_mobiusLikelihood line 368
  37. lemma OAI.CriticalStrip.mobiusLikelihood_Normalizer_pos line 374
  38. lemma OAI.CriticalStrip.continuousOn_mobiusCoordinate line 380
  39. lemma OAI.CriticalStrip.continuousOn_lowerLikelihood line 384
  40. lemma OAI.CriticalStrip.mobiusCoordinate_le_double line 411
  41. lemma OAI.CriticalStrip.self_le_mobiusCoordinate line 415
  42. lemma OAI.CriticalStrip.mobius_inverseQuarter_bounds line 419