OAI/Probability/ParisiFinite/TreeNodeDepth.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Tree Node Depth.

  1. def OAI.SKCavity.treeNodeDepth line 64
  2. lemma OAI.SKCavity.treeNodeDepth_path line 68
  3. lemma OAI.SKCavity.treeNodePath_injective line 81
  4. lemma OAI.SKCavity.treeNodePath_eq_levels line 86
  5. def OAI.SKCavity.treeGaussianCoeff line 90
  6. lemma OAI.SKCavity.field_treeGaussianCoeff line 94
  7. lemma OAI.SKCavity.treeGaussianCoeff_at_path line 107
  8. lemma OAI.SKCavity.kernel_treeGaussianCoeff line 118
  9. lemma OAI.SKCavity.tree_code_gaussian_law line 131
  10. def OAI.SKCavity.treeGaussianMoment line 143
  11. lemma OAI.SKCavity.treeGaussianMoment_mem_unit line 146
  12. lemma OAI.SKCavity.treeMarkMoment_tendsto_gaussian line 166
  13. lemma OAI.ParisiFinite.integrable_of_uniform_abs line 188
  14. lemma OAI.ParisiFinite.integrable_exp_of_uniform_abs line 194
  15. lemma OAI.ParisiFinite.logMean_uniform_abs line 204
  16. lemma OAI.ParisiFinite.tendsto_logMean_of_uniform_abs line 220
  17. lemma OAI.SKCavity.gaussianQuantizer_logMean line 250
  18. lemma OAI.SKCavity.gaussianQuantizer_logMean_tendsto line 259
  19. def OAI.SKCavity.finiteRisk line 282
  20. def OAI.SKCavity.finiteHierarchyRisk line 285
  21. lemma OAI.SKCavity.finiteRisk_const line 289
  22. lemma OAI.SKCavity.finiteRisk_exp line 296
  23. lemma OAI.SKCavity.hierarchyMark_eq_finiteRisk line 303
  24. lemma OAI.SKCavity.hierarchyLog_eq_finiteHierarchyRisk line 329
  25. lemma OAI.SKCavity.finiteRisk_eq_logMean line 340
  26. lemma OAI.SKCavity.finiteRisk_uniform_abs line 346
  27. lemma OAI.SKCavity.finiteHierarchyRisk_uniform_abs line 372
  28. def OAI.SKCavity.gaussianHierarchyRisk line 388
  29. lemma OAI.SKCavity.continuous_gaussianLogMean line 393
  30. lemma OAI.SKCavity.continuous_finCons line 421
  31. lemma OAI.SKCavity.gaussianHierarchyRisk_continuous_bound line 430
  32. lemma OAI.SKCavity.gaussianHierarchyRisk_uniform_abs line 451
  33. theorem OAI.SKCavity.quantizedHierarchyRisk_tendsto line 458
  34. def OAI.SKCavity.gaussianHierarchyMoment line 518
  35. lemma OAI.SKCavity.hierarchyMarkedMoment_tendsto_gaussian line 522
  36. lemma OAI.SKCavity.gaussianHierarchyMoment_mem_unit line 533
  37. lemma OAI.SKCavity.normalized_moment_bound line 543
  38. lemma OAI.SKCavity.affine_log_bounded line 553
  39. theorem OAI.SKCavity.GG_gaussian_hierarchy_log_identity line 571
  40. lemma OAI.SKCavity.card_injective_replica_maps line 618
  41. lemma OAI.SKCavity.descFactorial_ratio_tendsto line 631
  42. theorem OAI.SKCavity.replica_average_moment_tendsto line 656