OAI/Probability/ParisiFinite/LogSeriesTermBound.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Log Series Term Bound.

  1. lemma OAI.SKCavity.log_series_term_bound line 64
  2. lemma OAI.SKCavity.integral_log_unit_series line 76
  3. theorem OAI.SKCavity.empirical_log_limit_of_distinct_moments line 105
  4. def OAI.SKCavity.treePathVector line 177
  5. lemma OAI.SKCavity.treePathVector_continuous line 180
  6. def OAI.SKCavity.treePathLaw line 183
  7. instance OAI.SKCavity.treePathLaw_probability line 186
  8. lemma OAI.SKCavity.integral_treePathLaw line 191
  9. def OAI.SKCavity.pathCoeff line 196
  10. lemma OAI.SKCavity.field_pathCoeff line 199
  11. lemma OAI.SKCavity.kernel_pathCoeff line 204
  12. lemma OAI.SKCavity.treePath_marginal_integral line 214
  13. def OAI.SKCavity.hierarchySampleLaw line 260
  14. def OAI.SKCavity.hierarchyBlockSample line 264
  15. lemma OAI.SKCavity.hierarchyBlockSample_measurable line 269
  16. lemma OAI.SKCavity.hierarchyBlockSample_on_event line 275
  17. lemma OAI.SKCavity.hierarchySampleLaw_integral line 289
  18. lemma OAI.SKCavity.hierarchySampleLaw_integral_block line 301
  19. lemma OAI.SKCavity.hierarchySampleLaw_probability line 319
  20. theorem OAI.SKCavity.hierarchySampleLaw_marginal_integral line 336
  21. lemma OAI.SKCavity.hierarchySampleLaw_product line 380
  22. theorem OAI.SKCavity.hierarchy_empirical_log_tendsto line 396
  23. lemma OAI.SKCavity.unit_average line 448
  24. lemma OAI.SKCavity.affine_average line 454
  25. lemma OAI.SKCavity.integral_affine_average_log line 461
  26. lemma OAI.SKCavity.gaussianHierarchyRisk_add_const line 486
  27. theorem OAI.SKCavity.hierarchy_empirical_positive_tendsto line 505
  28. lemma OAI.ParisiFinite.bounded_exp_mass_derivative line 559
  29. lemma OAI.ParisiFinite.logMean_coefficient_continuousAt_zero line 585
  30. lemma OAI.ParisiFinite.logMean_coefficient_continuous line 602
  31. lemma OAI.SKCavity.finiteRisk_measure line 635
  32. lemma OAI.SKCavity.finiteRisk_coefficient_tendsto line 641
  33. lemma OAI.SKCavity.finiteHierarchyRisk_coefficient_tendsto line 663