OAI/Probability/ParisiFinite/CoreScaleSqLeOne.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Core Scale Sq Le One.

  1. lemma OAI.SKCavity.coreScale_sq_le_one line 60
  2. lemma OAI.SKCavity.coreFluctuation_window_bound line 65
  3. def OAI.SKCavity.windowSlope line 98
  4. lemma OAI.SKCavity.tendsto_windowSlope line 100
  5. lemma OAI.SKCavity.cavityWindowBudget_root_bound line 116
  6. lemma OAI.SKCavity.tendsto_root_window_bound line 147
  7. theorem OAI.SKCavity.exists_cavity_compatible line 169
  8. def OAI.SKCavity.compatibleSize line 233
  9. def OAI.SKCavity.compatibleAmplitude line 237
  10. lemma OAI.SKCavity.compatible_spec line 241
  11. def OAI.SKCavity.compatibleCoeff line 251
  12. def OAI.SKCavity.compatibleLaw line 254
  13. def OAI.SKCavity.compatibleValue line 257
  14. lemma OAI.SKCavity.compatibleValue_le line 260
  15. lemma OAI.SKCavity.compatibleGG_le line 263
  16. lemma OAI.SKCavity.tendsto_succ_reciprocal line 268
  17. lemma OAI.SKCavity.tendsto_compatibleGG line 273
  18. lemma OAI.SKCavity.compatible_limit_Gram line 281
  19. lemma OAI.SKCavity.compatible_limit_GG line 292
  20. lemma OAI.SKCavity.compatible_limit_GG_unbounded line 312
  21. theorem OAI.SKCavity.compatible_limit_continuousGG line 330
  22. lemma OAI.SKCavity.compatible_limit_exchangeable_integral line 356
  23. theorem OAI.SKCavity.compatible_limit_exchangeable line 379
  24. theorem OAI.SKCavity.exists_compatible_ultrametric_limit line 391
  25. def OAI.SKCavity.partitionBlock line 412
  26. def OAI.SKCavity.partitionEvent line 415
  27. lemma OAI.SKCavity.measurableSet_partitionBlock line 418
  28. lemma OAI.SKCavity.measurableSet_partitionEvent line 432
  29. def OAI.SKCavity.clusterCount line 436
  30. lemma OAI.SKCavity.clusterCount_pos line 439
  31. lemma OAI.SKCavity.partition_pair_event line 443
  32. theorem OAI.SKCavity.GG_partition_join line 455
  33. lemma OAI.SKCavity.ultrametric_partition_join_disjoint line 485
  34. def OAI.SKCavity.overlapDiscount line 501
  35. lemma OAI.SKCavity.entry_upper_mass line 504
  36. lemma OAI.SKCavity.GG_cluster_join line 511
  37. def OAI.SKCavity.ClusterReps line 518
  38. lemma OAI.SKCavity.exists_clusterReps line 521
  39. lemma OAI.SKCavity.sum_clusterCount line 531
  40. lemma OAI.SKCavity.ae_full_probability line 548
  41. theorem OAI.SKCavity.GG_cluster_innovation line 557