OAI/Probability/SKBarriers/Hierarchy/CascadeBlockLaw.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.hierarchyPressure line 15
  2. theorem OAI.SK.Analytic.hierarchyPressure_boundedDerivs line 20
  3. theorem OAI.SK.Analytic.hierarchyPathWeight_const line 27
  4. theorem OAI.SK.Analytic.parameter_ae_fiberGaussian line 41
  5. theorem OAI.SK.Analytic.hierarchyPathLaw_const line 49
  6. def OAI.SK.Analytic.parameterAppend line 70
  7. theorem OAI.SK.Analytic.parameterAppend_zero line 74
  8. theorem OAI.SK.Analytic.parameterAppend_succ line 75
  9. theorem OAI.SK.Analytic.gaussianStep_append line 78
  10. theorem OAI.SK.Analytic.hierarchyPressure_split line 83
  11. def OAI.SK.Analytic.cascadeRoot line 97
  12. theorem OAI.SK.Analytic.gaussianAverage_append line 102
  13. theorem OAI.SK.Analytic.hierarchyMomentLevel_last line 106
  14. theorem OAI.SK.Analytic.hierarchyLevel_last line 112
  15. theorem OAI.SK.Analytic.hierarchyMomentLevel_split line 118
  16. theorem OAI.SK.Analytic.hierarchyLevel_split line 134
  17. theorem OAI.SK.Analytic.BoundedDerivs.translate line 157
  18. def OAI.SK.Analytic.parameterEmbed line 175
  19. def OAI.SK.Analytic.parameterNoise line 179
  20. theorem OAI.SK.Analytic.parameterEmbed_eq line 183
  21. theorem OAI.SK.Analytic.BoundedDerivs.parameterEmbed line 191
  22. theorem OAI.SK.Analytic.parameterEmbed_continuous line 195
  23. theorem OAI.SK.Analytic.gaussianStep_parameterEmbed line 201
  24. theorem OAI.SK.Analytic.gaussianAverage_parameterEmbed line 206
  25. theorem OAI.SK.Analytic.cascadeMoment_parameterEmbed line 211
  26. theorem OAI.SK.Analytic.cascadePressure_parameterEmbed line 221
  27. theorem OAI.SK.Analytic.cascadeMoment_const_integral line 229