OAI/Combinatorics/StripMass/WeightComparison.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.hasDerivAt_omegaLogHalf line 13
  2. lemma OAI.CriticalStrip.omegaLogHalf_derivative_lower line 56
  3. def OAI.CriticalStrip.upperLikelihoodWeight line 79
  4. lemma OAI.CriticalStrip.upperLikelihoodWeight_exp line 81
  5. theorem OAI.CriticalStrip.upperLikelihoodWeight_monotone line 88
  6. def OAI.CriticalStrip.scaledLaguerreWeight line 114
  7. def OAI.CriticalStrip.scaledLaguerreDensity line 116
  8. def OAI.CriticalStrip.laguerreDensityScale line 121
  9. lemma OAI.CriticalStrip.laguerreDensityScale_pos line 124
  10. lemma OAI.CriticalStrip.pairKernel_smul line 130
  11. lemma OAI.CriticalStrip.laguerreDensity_scaled line 136
  12. lemma OAI.CriticalStrip.orderedChamber_eq_laguerre_cutoff line 149
  13. lemma OAI.CriticalStrip.measurableSet_orderedChamber_Ioo line 156
  14. lemma OAI.CriticalStrip.orderedChamber_smul line 161
  15. lemma OAI.CriticalStrip.integral_orderedChamber_scaled line 177
  16. lemma OAI.CriticalStrip.inverseQuarterSum_smul line 187
  17. lemma OAI.CriticalStrip.measurable_scaledLaguerreWeight line 196
  18. lemma OAI.CriticalStrip.continuousOn_scaledLaguerreWeight line 200
  19. lemma OAI.CriticalStrip.scaledLaguerreWeight_pos line 206
  20. lemma OAI.CriticalStrip.scaledLaguerreWeight_le line 210
  21. lemma OAI.CriticalStrip.scaledLaguerreDensity_pos line 216
  22. lemma OAI.CriticalStrip.scaledLaguerreDensity_le line 222
  23. lemma OAI.CriticalStrip.measurable_scaledLaguerreDensity line 231
  24. lemma OAI.CriticalStrip.integrableOn_scaledLaguerreDensity line 243
  25. abbrev OAI.CriticalStrip.inverseQuarterStatistic line 251
  26. lemma OAI.CriticalStrip.inverseQuarterStatistic_nonneg line 254
  27. lemma OAI.CriticalStrip.measurable_inverseQuarterStatistic line 258
  28. lemma OAI.CriticalStrip.integrableOn_scaledLaguerre_inverseQuarter line 262
  29. lemma OAI.CriticalStrip.scaledLaguerre_cutoffNormalizer_pos line 276
  30. def OAI.CriticalStrip.upperLikelihood line 293
  31. lemma OAI.CriticalStrip.continuousOn_upperLikelihood line 296
  32. lemma OAI.CriticalStrip.upperLikelihood_pos line 306
  33. lemma OAI.CriticalStrip.upperLikelihood_monotone line 312
  34. lemma OAI.CriticalStrip.scaledWeight_mul_upperLikelihoodWeight line 322
  35. lemma OAI.CriticalStrip.scaledDensity_mul_upperLikelihood line 334
  36. lemma OAI.CriticalStrip.orderedChamber_eq_positive_cutoff line 344
  37. lemma OAI.CriticalStrip.positive_cutoffNormalizer_pos line 352
  38. theorem OAI.CriticalStrip.positive_half_inverseQuarter_le_scaled_reference line 361
  39. lemma OAI.CriticalStrip.integral_scaledLaguerre_cutoff line 414