OAI/Probability/SKBarriers/Hierarchy/HierarchyPenalty.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.hierarchyPenalty line 25
  2. theorem OAI.SK.Analytic.hierarchyPenalty_regular line 33
  3. def OAI.SK.Analytic.hierarchyPathWeight line 50
  4. theorem OAI.SK.Analytic.hierarchyPathWeight_eq line 58
  5. theorem OAI.SK.Analytic.hierarchy_fixed_spin_density line 69
  6. def OAI.SK.Analytic.ParameterInvariant line 77
  7. theorem OAI.SK.Analytic.parameterDerivative_zero_of_invariant line 80
  8. theorem OAI.SK.Analytic.ParameterInvariant.gaussianStep line 90
  9. theorem OAI.SK.Analytic.hierarchyPenalty_invariant line 99
  10. theorem OAI.SK.Analytic.hierarchy_fixed_spin_linear_variance line 115