OAI/Probability/Voronoi/CardyFormula.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

Cardy integrals and hypergeometric formulas with Poisson-Voronoi crossing definitions.

  1. def OAI.Cardy.PositivelyOriented line 14
  2. structure OAI.Cardy.JordanQuadrilateral line 23
  3. def OAI.Cardy.JordanQuadrilateral.a line 44
  4. def OAI.Cardy.JordanQuadrilateral.b line 46
  5. def OAI.Cardy.JordanQuadrilateral.c line 48
  6. def OAI.Cardy.JordanQuadrilateral.d line 50
  7. def OAI.Cardy.JordanQuadrilateral.arcAB line 52
  8. def OAI.Cardy.JordanQuadrilateral.arcCD line 54
  9. def OAI.Cardy.upperHalfPlane line 58
  10. def OAI.Cardy.IsConformalParameter line 60
  11. abbrev OAI.Cardy.Box line 73
  12. abbrev OAI.Cardy.Slot line 74
  13. abbrev OAI.Cardy.GeometrySample line 75
  14. abbrev OAI.Cardy.Sample line 76
  15. def OAI.Cardy.unitUniform line 78
  16. instance OAI.Cardy.(instance at line 80) line 80
  17. def OAI.Cardy.fairColor line 84
  18. instance OAI.Cardy.(instance at line 86) line 86
  19. def OAI.Cardy.rate line 90
  20. def OAI.Cardy.countLaw line 92
  21. def OAI.Cardy.locationLaw line 95
  22. def OAI.Cardy.colorLaw line 98
  23. instance OAI.Cardy.(instance at line 101) line 101
  24. instance OAI.Cardy.(instance at line 105) line 105
  25. instance OAI.Cardy.(instance at line 109) line 109
  26. def OAI.Cardy.geometryLaw line 113
  27. instance OAI.Cardy.(instance at line 115) line 115
  28. def OAI.Cardy.sampleLaw line 119
  29. instance OAI.Cardy.(instance at line 121) line 121
  30. def OAI.Cardy.Active line 125
  31. def OAI.Cardy.position line 127
  32. def OAI.Cardy.sites line 131
  33. def OAI.Cardy.blackSites line 133
  34. def OAI.Cardy.voronoiCell line 136
  35. def OAI.Cardy.blackRegion line 139
  36. def OAI.Cardy.Crosses line 142
  37. def OAI.Cardy.crossingEvent line 146
  38. def OAI.Cardy.crossingProbability line 149
  39. def OAI.Cardy.cardyWeight line 152
  40. def OAI.Cardy.cardyIntegral line 154
  41. def OAI.Cardy.cardyHypergeometric line 157
  42. lemma OAI.Cardy.JordanQuadrilateral.boundary_ne_of_lt line 164
  43. theorem OAI.Cardy.JordanQuadrilateral.marks_distinct line 169
  44. theorem OAI.Cardy.JordanQuadrilateral.arcAB_subset_frontier line 182
  45. theorem OAI.Cardy.JordanQuadrilateral.arcCD_subset_frontier line 187
  46. theorem OAI.Cardy.JordanQuadrilateral.endpoints_mem_arcs line 192
  47. theorem OAI.Cardy.voronoiCell_closed line 201
  48. theorem OAI.Cardy.site_mem_voronoiCell line 208
  49. theorem OAI.Cardy.blackSites_subset_sites line 212
  50. theorem OAI.Cardy.blackSites_subset_blackRegion line 216
  51. theorem OAI.Cardy.crosses_mono line 220
  52. theorem OAI.Cardy.crossingProbability_nonneg line 225
  53. theorem OAI.Cardy.crossingProbability_le_one line 228
  54. theorem OAI.Cardy.countLaw_marginal line 232
  55. theorem OAI.Cardy.colorLaw_marginal line 236
  56. theorem OAI.Cardy.rate_coe line 240
  57. theorem OAI.Cardy.geometry_colors_independent line 243
  58. theorem OAI.Cardy.sampleLaw_color_marginal line 247
  59. theorem OAI.Cardy.sampleLaw_geometry_marginal line 251
  60. theorem OAI.Cardy.counts_independent line 255
  61. theorem OAI.Cardy.colors_independent line 259
  62. theorem OAI.Cardy.fairColor_singleton line 263
  63. theorem OAI.Cardy.colorLaw_singleton line 268
  64. lemma OAI.Cardy.cardyWeight_complex line 273
  65. theorem OAI.Cardy.cardyDenominator_eq_beta line 285
  66. theorem OAI.Cardy.cardyDenominator_eq_gamma line 293
  67. theorem OAI.Cardy.cardyDenominator_pos line 307
  68. theorem OAI.Cardy.cardyIntegral_zero line 312
  69. theorem OAI.Cardy.cardyIntegral_one line 315
  70. theorem OAI.Cardy.cardyWeight_integrable line 318
  71. theorem OAI.Cardy.cardyWeight_integrable_subinterval line 330
  72. theorem OAI.Cardy.cardyWeight_nonneg line 336
  73. theorem OAI.Cardy.cardyWeight_pos line 339
  74. lemma OAI.Cardy.cardyWeight_symm line 342
  75. theorem OAI.Cardy.cardyIntegral_continuousOn line 347
  76. theorem OAI.Cardy.cardyIntegral_strictMonoOn line 353
  77. theorem OAI.Cardy.cardyIntegral_mem_Icc line 365
  78. theorem OAI.Cardy.cardyIntegral_mem_Ioo line 372
  79. theorem OAI.Cardy.cardyIntegral_reflection line 380
  80. theorem OAI.Cardy.cardyIntegral_half line 393
  81. def OAI.Cardy.cardyBinomialCoefficient line 398
  82. lemma OAI.Cardy.cardyBinomialCoefficient_pos line 401
  83. lemma OAI.Cardy.cardyBinomialCoefficient_eq_choose line 404
  84. lemma OAI.Cardy.cardy_binomial_hasSum line 412
  85. lemma OAI.Cardy.cardyWeight_hasSum line 424
  86. theorem OAI.Cardy.cardyNumerator_hasSum line 435
  87. lemma OAI.Cardy.cardyBinomialTerm_integral line 461
  88. lemma OAI.Cardy.cardyHypergeometricCoefficient_eq line 470
  89. theorem OAI.Cardy.cardyNumerator_eq_hypergeometric line 500
  90. theorem OAI.Cardy.cardyIntegral_eq_hypergeometric line 515