OAI/Probability/ParisiFinite/HierarchyNumeratorNonneg.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Hierarchy Numerator Nonneg.

  1. lemma OAI.SKCavity.hierarchyNumerator_nonneg line 65
  2. def OAI.SKCavity.parameterHierarchyMoment line 86
  3. lemma OAI.SKCavity.parameterHierarchyMoment_mem_unit line 90
  4. lemma OAI.SKCavity.parameterHierarchyMoment_continuous line 120
  5. def OAI.SKCavity.parameterHierarchyLogSeries line 142
  6. lemma OAI.SKCavity.parameterHierarchyLogSeries_radius line 146
  7. lemma OAI.SKCavity.parameterHierarchyLog_hasFPowerSeriesAt line 169
  8. theorem OAI.SKCavity.parameterHierarchy_log_identity line 202
  9. theorem OAI.SKCavity.parameterHierarchy_finiteRisk_identity_all line 237
  10. theorem OAI.SKCavity.GG_finiteRisk_identity_all line 288
  11. theorem OAI.SKCavity.GG_gaussian_hierarchy_log_identity_all line 330
  12. theorem OAI.SKCavity.hierarchy_empirical_log_tendsto_all line 374
  13. theorem OAI.SKCavity.hierarchy_empirical_positive_tendsto_all line 428
  14. lemma OAI.SKCavity.treePathLaw_coordinate line 483
  15. lemma OAI.SKCavity.hierarchySampleLaw_coordinate line 510
  16. lemma OAI.SKCavity.hierarchySampleLaw_integrable_coordinate line 525
  17. lemma OAI.SKCavity.hierarchySampleLaw_integral_coordinate line 536
  18. theorem OAI.ParisiFinite.step_tendsto line 554
  19. lemma OAI.ParisiFinite.clip_lipschitz line 593
  20. lemma OAI.ParisiFinite.clip_tendsto line 597
  21. def OAI.SKCavity.scalarHierarchy line 614
  22. lemma OAI.SKCavity.scalarHierarchy_lipschitz line 618
  23. lemma OAI.SKCavity.gaussianHierarchyRisk_sum line 625
  24. lemma OAI.SKCavity.scalarHierarchy_tendsto line 639
  25. lemma OAI.SKCavity.scalarHierarchy_clip_tendsto line 652
  26. lemma OAI.SKCavity.logMean_mul_const line 658
  27. lemma OAI.SKCavity.scalarHierarchy_mul_const line 668