OAI/Probability/ParisiFinite/LowBlock.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Low Block.

  1. def OAI.SKCavity.lowBlock line 60
  2. def OAI.SKCavity.lowEvent line 63
  3. def OAI.SKCavity.lowBad line 65
  4. lemma OAI.SKCavity.measurableSet_lowBlock line 68
  5. lemma OAI.SKCavity.lowEvent_one line 74
  6. lemma OAI.SKCavity.lowBad_GG line 78
  7. lemma OAI.SKCavity.lowEvent_step_cover line 98
  8. lemma OAI.SKCavity.lowEvent_step_bound line 124
  9. lemma OAI.SKCavity.lowEvent_positive line 155
  10. lemma OAI.SKCavity.gram_clique_bound line 170
  11. lemma OAI.SKCavity.exists_negative_clique_impossible line 190
  12. theorem OAI.SKCavity.GG_negative_threshold_zero line 200
  13. lemma OAI.SKCavity.GG_negative_overlap_zero line 213
  14. lemma OAI.SKCavity.GG_nonnegative_overlap line 225
  15. theorem OAI.SKCavity.urn_growth_contradiction line 241
  16. def OAI.SKCavity.initialBlock line 289
  17. lemma OAI.SKCavity.continuous_initialBlock line 292
  18. def OAI.SKCavity.rowSurvival line 297
  19. def OAI.SKCavity.survivalBlock line 300
  20. lemma OAI.SKCavity.rowSurvival_eq_preimage line 304
  21. lemma OAI.SKCavity.measurableSet_survivalBlock line 312
  22. lemma OAI.SKCavity.measurableSet_rowSurvival line 320
  23. lemma OAI.SKCavity.rowSurvival_succ line 325
  24. lemma OAI.SKCavity.rowSurvival_GG line 338
  25. def OAI.SKCavity.FiniteExchangeable line 378
  26. lemma OAI.SKCavity.genericOverlap_limit_FiniteExchangeable line 382
  27. lemma OAI.SKCavity.exchangeable_event line 386
  28. lemma OAI.SKCavity.exchangeable_event_real line 394
  29. def OAI.SKCavity.tailPerm line 400
  30. lemma OAI.SKCavity.tailPerm_old line 403
  31. lemma OAI.SKCavity.tailPerm_new line 406
  32. def OAI.SKCavity.newRow line 409
  33. lemma OAI.SKCavity.continuous_newRow line 412
  34. def OAI.SKCavity.uniqueMark line 417
  35. lemma OAI.SKCavity.measurableSet_uniqueMark line 420
  36. lemma OAI.SKCavity.uniqueMark_disjoint line 429
  37. lemma OAI.SKCavity.uniqueMark_relabel line 436
  38. lemma OAI.SKCavity.uniqueMark_equal line 454
  39. lemma OAI.SKCavity.uniqueMark_bound line 464
  40. def OAI.SKCavity.arrayRow line 484
  41. lemma OAI.SKCavity.continuous_arrayRow line 486
  42. def OAI.SKCavity.patternBlock line 490
  43. lemma OAI.SKCavity.measurableSet_patternBlock line 494
  44. lemma OAI.SKCavity.patternBlock_preimage line 499
  45. def OAI.SKCavity.doubleMarkBlock line 504
  46. lemma OAI.SKCavity.measurableSet_doubleMarkBlock line 509
  47. def OAI.SKCavity.doubleMarkAt line 515
  48. lemma OAI.SKCavity.measurableSet_doubleMarkAt line 519
  49. def OAI.SKCavity.prefixFresh line 525
  50. lemma OAI.SKCavity.prefixFresh_injective line 527
  51. lemma OAI.SKCavity.prefixFresh_old line 536
  52. lemma OAI.SKCavity.prefixFresh_last line 539
  53. lemma OAI.SKCavity.doubleMarkAt_preimage line 541
  54. lemma OAI.SKCavity.doubleMarkAt_equal line 558
  55. lemma OAI.SKCavity.rowSurvival_zero line 568
  56. theorem OAI.SKCavity.GG_duplication line 581
  57. lemma OAI.SKCavity.exchangeable_pair_event line 628
  58. theorem OAI.SKCavity.GG_duplication_of_positive line 645