OAI/Combinatorics/StripMass/CoordinateBoxes.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.isOpen_coordinateBox line 13
  2. lemma OAI.CriticalStrip.isOpen_cutoffEvent line 21
  3. lemma OAI.CriticalStrip.laguerreDomain_cutoff_nonempty line 24
  4. theorem OAI.CriticalStrip.laguerreLaw_cutoff_pos line 37
  5. theorem OAI.CriticalStrip.laguerreLaw_conditioned_antitone line 56
  6. def OAI.CriticalStrip.positiveLaw line 69
  7. theorem OAI.CriticalStrip.positiveLaw_isProbabilityMeasure line 73
  8. theorem OAI.CriticalStrip.ae_positiveLaw_orderedDomain line 81
  9. theorem OAI.CriticalStrip.integral_positiveLaw line 87
  10. theorem OAI.CriticalStrip.integrable_positiveLaw_iff line 100
  11. theorem OAI.CriticalStrip.positiveLaw_covariance line 110
  12. theorem OAI.CriticalStrip.positiveLaw_covariance_antitone line 123
  13. theorem OAI.CriticalStrip.positiveLaw_cutoff_covariance line 137
  14. theorem OAI.CriticalStrip.positiveLaw_integrable_inverseQuarterSum line 155
  15. theorem OAI.CriticalStrip.positiveLaw_integrable_inverseQuarterCoordinate line 159
  16. theorem OAI.CriticalStrip.positiveLaw_measureReal line 165
  17. lemma OAI.CriticalStrip.orderedDomain_cutoff_nonempty line 174
  18. theorem OAI.CriticalStrip.positiveLaw_cutoff_pos line 188
  19. theorem OAI.CriticalStrip.positiveLaw_conditioned_antitone line 206
  20. lemma OAI.CriticalStrip.continuousOn_inverse_coordinate line 217
  21. lemma OAI.CriticalStrip.antitoneOn_inverse_coordinate line 221
  22. lemma OAI.CriticalStrip.continuousOn_inverseQuarterSum line 227
  23. lemma OAI.CriticalStrip.antitoneOn_inverseQuarterSum line 235
  24. theorem OAI.CriticalStrip.positiveLaw_cutoff_inverseQuarterSum line 242
  25. theorem OAI.CriticalStrip.laguerreLaw_cutoff_inverseQuarterSum line 251
  26. theorem OAI.CriticalStrip.laguerreLaw_cutoff_inverse_coordinate line 260
  27. lemma OAI.CriticalStrip.mem_cutoffEvent_iff_last line 269
  28. theorem OAI.CriticalStrip.omega_antitoneOn line 284
  29. def OAI.CriticalStrip.mobiusCoordinate line 296
  30. lemma OAI.CriticalStrip.mobiusCoordinate_mem line 298
  31. lemma OAI.CriticalStrip.mobiusCoordinate_strictMonoOn line 303
  32. lemma OAI.CriticalStrip.pairKernel_mobius line 310
  33. lemma OAI.CriticalStrip.harmonicPair_monotone line 321
  34. def OAI.CriticalStrip.mobiusPairFactor line 335
  35. lemma OAI.CriticalStrip.mobiusPairFactor_pos line 337
  36. lemma OAI.CriticalStrip.mobiusPairFactor_antitone line 340
  37. lemma OAI.CriticalStrip.exponential_over_power_antitone line 346
  38. lemma OAI.CriticalStrip.exponential_over_natPower_eq line 365
  39. def OAI.CriticalStrip.lowerLikelihoodWeight line 371
  40. lemma OAI.CriticalStrip.lowerLikelihoodWeight_pos line 374
  41. lemma OAI.CriticalStrip.lowerLikelihoodWeight_antitone line 379
  42. def OAI.CriticalStrip.lowerLikelihood line 393
  43. lemma OAI.CriticalStrip.lowerLikelihood_pos line 397
  44. theorem OAI.CriticalStrip.lowerLikelihood_antitone line 403
  45. def OAI.CriticalStrip.omegaLogHalf line 421