OAI/Probability/ParisiFinite/GenericDegrees.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Generic Degrees.

  1. def OAI.SKCavity.genericDegrees line 61
  2. def OAI.SKCavity.genericMixedAmplitude line 63
  3. lemma OAI.SKCavity.genericMixedAmplitude_mem line 66
  4. def OAI.SKCavity.genericMixedCoeff line 72
  5. def OAI.SKCavity.overlapGGDefect line 76
  6. lemma OAI.SKCavity.genericMixed_defect_le line 85
  7. theorem OAI.SKCavity.tendsto_genericMixed_GG_defect line 98
  8. lemma OAI.SKCavity.tendsto_genericMixed_variance_density line 111
  9. theorem OAI.SKCavity.tendsto_genericMixed_pressureDensity_error line 123
  10. lemma OAI.SKCavity.replicaMean_prefix line 145
  11. lemma OAI.SKCavity.averagedReplica_prefix line 155
  12. def OAI.SKCavity.fieldReplicaMass line 160
  13. lemma OAI.SKCavity.fieldReplicaMass_nonneg line 163
  14. lemma OAI.SKCavity.sum_fieldReplicaMass line 166
  15. def OAI.SKCavity.fieldOverlapLaw line 173
  16. lemma OAI.SKCavity.integral_fieldOverlapLaw line 177
  17. abbrev OAI.SKCavity.OverlapBlock line 185
  18. def OAI.SKCavity.blockOfArray line 187
  19. def OAI.SKCavity.blockOfReplicas line 189
  20. lemma OAI.SKCavity.continuous_blockOfArray line 192
  21. lemma OAI.SKCavity.blockOfArray_configurationOverlap line 196
  22. lemma OAI.SKCavity.integral_fieldOverlapLaw_block line 206
  23. def OAI.SKCavity.genericOverlapLaw line 216
  24. lemma OAI.SKCavity.genericOverlapLaw_Gram line 219
  25. lemma OAI.SKCavity.genericOverlap_limit_Gram line 223
  26. def OAI.SKCavity.arrayGGDefect line 241
  27. lemma OAI.SKCavity.continuous_arrayGGDefect line 248
  28. lemma OAI.SKCavity.arrayGGDefect_fieldOverlapLaw line 259
  29. theorem OAI.SKCavity.genericOverlap_limit_GG line 284
  30. theorem OAI.SKCavity.exists_generic_GG_Gram_limit line 300
  31. lemma OAI.SKCavity.integrable_continuousMap line 316
  32. def OAI.SKCavity.continuousIntegral line 322
  33. def OAI.SKCavity.overlapIntegral line 332
  34. lemma OAI.SKCavity.overlapIntegral_apply line 337
  35. def OAI.SKCavity.continuousGG line 343
  36. def OAI.SKCavity.overlapPower line 349
  37. lemma OAI.SKCavity.continuousGG_power line 351
  38. lemma OAI.SKCavity.arrayGGDefect_const_mul line 362
  39. lemma OAI.SKCavity.genericOverlap_limit_GG_unbounded line 369
  40. theorem OAI.SKCavity.genericOverlap_limit_continuousGG line 387
  41. def OAI.SKCavity.blockOverlapMap line 421
  42. lemma OAI.SKCavity.continuous_blockOverlapMap line 424
  43. def OAI.SKCavity.jointOverlapLaw line 427
  44. instance OAI.SKCavity.instIsFiniteJointOverlapLaw line 430
  45. lemma OAI.SKCavity.integral_jointOverlapLaw line 433
  46. def OAI.SKCavity.blockLaw line 442
  47. def OAI.SKCavity.entryLaw line 445
  48. instance OAI.SKCavity.instIsFiniteBlockLaw line 448
  49. instance OAI.SKCavity.instIsFiniteEntryLaw line 450
  50. lemma OAI.SKCavity.integral_blockLaw line 453
  51. lemma OAI.SKCavity.integral_entryLaw line 459
  52. theorem OAI.SKCavity.GG_measure_identity line 467
  53. theorem OAI.SKCavity.genericOverlap_limit_measureGG line 495
  54. lemma OAI.SKCavity.replicaWeight_perm line 511
  55. lemma OAI.SKCavity.replicaMean_perm line 516
  56. lemma OAI.SKCavity.replicaMean_injection line 528
  57. lemma OAI.SKCavity.averagedReplica_injection line 536
  58. def OAI.SKCavity.selectedBlock line 548
  59. lemma OAI.SKCavity.continuous_selectedBlock line 551
  60. lemma OAI.SKCavity.integral_fieldOverlapLaw_selected line 555
  61. lemma OAI.SKCavity.genericOverlap_limit_exchangeable_integral line 573
  62. theorem OAI.SKCavity.genericOverlap_limit_exchangeable line 596
  63. def OAI.SKCavity.GGIdentities line 614
  64. theorem OAI.SKCavity.genericOverlap_limit_GGIdentities line 618
  65. lemma OAI.SKCavity.GG_event_identity line 622
  66. lemma OAI.SKCavity.entryLaw_probability line 644