OAI/Probability/ParisiFinite/ExpectedReindexStates.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Expected Reindex States.

  1. lemma OAI.SKCavity.expected_reindex_states line 63
  2. lemma OAI.SKCavity.expected_kernel_distance_le line 71
  3. def OAI.SKCavity.idealSite line 86
  4. def OAI.SKCavity.idealCorrection line 89
  5. lemma OAI.SKCavity.kernel_idealSite line 92
  6. lemma OAI.SKCavity.kernel_idealCorrection line 97
  7. lemma OAI.SKCavity.kernel_cavityDoubledCoeff line 102
  8. def OAI.SKCavity.actualSite line 112
  9. def OAI.SKCavity.actualCorrection line 114
  10. lemma OAI.SKCavity.kernel_actualSite line 116
  11. lemma OAI.SKCavity.kernel_actualCorrection line 127
  12. lemma OAI.SKCavity.actualSite_kernel_error line 135
  13. lemma OAI.SKCavity.actualCorrection_kernel_error line 143
  14. lemma OAI.SKCavity.mixedCavity_doubled line 156
  15. def OAI.SKCavity.idealCavity line 178
  16. theorem OAI.SKCavity.mixedIncrement_ideal_error line 184
  17. lemma OAI.SKCavity.blockOfReplicas_Gram line 218
  18. def OAI.SKCavity.cavityObservable line 228
  19. lemma OAI.SKCavity.cavityObservable_on_Gram line 232
  20. lemma OAI.SKCavity.sample_ideal_cosh line 238
  21. lemma OAI.SKCavity.sample_ideal_square line 255
  22. lemma OAI.SKCavity.cavityObservable_replicas line 265
  23. def OAI.SKCavity.cavitySampleError line 270
  24. theorem OAI.SKCavity.cavityObservable_ideal_error line 275
  25. theorem OAI.SKCavity.cavityObservable_actual_error line 294
  26. lemma OAI.SKCavity.compatibleValue_lower line 314
  27. lemma OAI.SKCavity.compatibleValue_upper line 318
  28. lemma OAI.SKCavity.exists_value_subsequence line 321
  29. lemma OAI.SKCavity.compatibleValue_limit_le line 329
  30. lemma OAI.SKCavity.tendsto_compatible_correction line 337
  31. def OAI.SKCavity.scalarCavitySample line 345
  32. theorem OAI.SKCavity.scalarCavitySample_limit_error line 350
  33. lemma OAI.SKCavity.cavitySampleError_square line 367
  34. def OAI.SKCavity.quadraticCavitySamples line 376
  35. lemma OAI.SKCavity.tendsto_cavitySampleError_square line 379
  36. lemma OAI.SKCavity.quadraticCavitySamples_limit line 385
  37. theorem OAI.SKCavity.exists_scalar_ultrametric_cavity line 398
  38. def OAI.SKCavity.codeLabels line 419
  39. def OAI.SKCavity.labelCount line 421
  40. lemma OAI.SKCavity.codeLabels_mem line 424
  41. lemma OAI.SKCavity.labelCount_eq_clusterCount line 427
  42. lemma OAI.SKCavity.labelCount_pos_iff line 430
  43. lemma OAI.SKCavity.labelCount_succ line 434
  44. lemma OAI.SKCavity.codeLabels_succ line 441
  45. def OAI.SKCavity.blockFactor line 454
  46. def OAI.SKCavity.tableFactor line 457
  47. lemma OAI.SKCavity.blockFactor_one line 460
  48. lemma OAI.SKCavity.tableFactor_one line 461
  49. lemma OAI.SKCavity.blockFactor_succ line 463
  50. lemma OAI.SKCavity.tableFactor_succ line 471
  51. def OAI.SKCavity.partitionNumerator line 479
  52. lemma OAI.SKCavity.codeLabels_nonempty line 482
  53. lemma OAI.SKCavity.partitionNumerator_existing line 485
  54. lemma OAI.SKCavity.partitionNumerator_fresh line 512
  55. lemma OAI.SKCavity.ClusterReps.card_codeLabels line 535
  56. lemma OAI.SKCavity.partitionNumerator_one line 546
  57. theorem OAI.SKCavity.GG_partition_EPPF line 556
  58. def OAI.SKCavity.fallingCoeff line 597
  59. lemma OAI.SKCavity.fallingCoeff_zero line 599
  60. lemma OAI.SKCavity.fallingCoeff_succ line 600
  61. lemma OAI.SKCavity.iteratedDeriv_affine_rpow line 603
  62. lemma OAI.SKCavity.iteratedDeriv_affine_rpow_zero line 624
  63. lemma OAI.SKCavity.fallingCoeff_blockFactor line 628
  64. lemma OAI.SKCavity.iteratedDeriv_affine_rpow_zero_pos line 640
  65. def OAI.SKCavity.finiteMarkTransform line 649
  66. def OAI.SKCavity.finiteMarkMoment line 652
  67. lemma OAI.SKCavity.contDiffAt_mark line 654
  68. lemma OAI.SKCavity.finiteMarkTransform_zero line 663
  69. lemma OAI.SKCavity.iteratedDeriv_mark line 666