OAI/Probability/ParisiFinite/RestrictCode.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Restrict Code.

  1. def OAI.SKCavity.restrictCode line 60
  2. lemma OAI.SKCavity.partition_restrict line 62
  3. lemma OAI.SKCavity.partition_extend_iff line 66
  4. lemma OAI.SKCavity.partition_existing_iff line 87
  5. lemma OAI.SKCavity.partition_fresh_iff line 106
  6. lemma OAI.SKCavity.partition_zero line 113
  7. lemma OAI.SKCavity.partition_one_real line 118
  8. lemma OAI.SKCavity.GG_partition_existing line 132
  9. lemma OAI.SKCavity.GG_partition_fresh line 148
  10. theorem OAI.SKCavity.threshold_partition_unique line 165
  11. def OAI.SKCavity.oldRowCondition line 204
  12. lemma OAI.SKCavity.measurableSet_oldRowCondition line 207
  13. lemma OAI.SKCavity.ultra_row_event line 212
  14. lemma OAI.SKCavity.blockLaw_real line 225
  15. theorem OAI.SKCavity.GG_row_tail_identity line 232
  16. lemma OAI.SKCavity.row_tail_unique line 258
  17. def OAI.SKCavity.overlapTails line 288
  18. lemma OAI.SKCavity.overlapTails_measurable line 290
  19. lemma OAI.SKCavity.overlapTails_generate line 294
  20. lemma OAI.SKCavity.overlapTails_pi line 304
  21. lemma OAI.SKCavity.overlapTails_univ line 311
  22. lemma OAI.SKCavity.overlapTails_spanning line 318
  23. def OAI.SKCavity.rowTailBoxes line 321
  24. lemma OAI.SKCavity.rowTailBoxes_generate line 324
  25. lemma OAI.SKCavity.rowTailBoxes_pi line 327
  26. lemma OAI.SKCavity.rowTailBoxes_spanning line 330
  27. lemma OAI.SKCavity.rowTailBoxes_characterization line 333
  28. def OAI.SKCavity.blockRowMap line 353
  29. lemma OAI.SKCavity.continuous_blockRowMap line 356
  30. def OAI.SKCavity.blockRowLaw line 359
  31. instance OAI.SKCavity.blockRowLaw_probability line 362
  32. lemma OAI.SKCavity.blockRowLaw_eq line 366
  33. def OAI.SKCavity.joinBlock line 391
  34. lemma OAI.SKCavity.continuous_joinBlock line 395
  35. lemma OAI.SKCavity.joinBlock_blockRowMap line 410
  36. lemma OAI.SKCavity.joinBlock_map_law line 421
  37. lemma OAI.SKCavity.blockLaw_zero line 428
  38. theorem OAI.SKCavity.GG_ultrametric_blocks_unique line 436
  39. lemma OAI.SKCavity.abs_log_sub_le line 458
  40. lemma OAI.SKCavity.inv_sq_weighted_le line 476
  41. lemma OAI.SKCavity.log_error_young line 483
  42. lemma OAI.SKCavity.replicaMean_mono line 498
  43. lemma OAI.SKCavity.replicaMean_finiteSum line 505
  44. lemma OAI.SKCavity.replicaMean_centered_sq_sum line 511
  45. def OAI.SKCavity.empiricalMean line 533
  46. lemma OAI.SKCavity.empiricalMean_positive line 536
  47. lemma OAI.SKCavity.empiricalMean_variance line 541
  48. lemma OAI.SKCavity.average_variance_le line 557
  49. lemma OAI.SKCavity.replicaMean_empirical line 576
  50. lemma OAI.SKCavity.empiricalMean_inv_sq line 585
  51. lemma OAI.SKCavity.replicaMean_inv_sq_empirical line 593
  52. lemma OAI.SKCavity.average_inv_sq line 597
  53. lemma OAI.SKCavity.replicaMean_abs line 601
  54. theorem OAI.SKCavity.empirical_log_error line 610
  55. lemma OAI.SKCavity.empirical_log_mean_error line 635