OAI/Probability/SKBarriers/Hierarchy/WeightedHierarchyProbability.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.weightedHierarchyWeight line 17
  2. theorem OAI.SK.Analytic.weightedHierarchyWeight_regular line 22
  3. theorem OAI.SK.Analytic.weightedHierarchyWeight_nonneg line 29
  4. theorem OAI.SK.Analytic.weightedHierarchyWeight_sum line 34
  5. theorem OAI.SK.Analytic.weightedHierarchyMean_eq_sum line 45
  6. def OAI.SK.Analytic.weightedHierarchyReplica line 60
  7. theorem OAI.SK.Analytic.weightedHierarchyReplica_integrable line 65
  8. theorem OAI.SK.Analytic.weightedHierarchyReplica_const line 88
  9. theorem OAI.SK.Analytic.weightedHierarchyReplica_mono line 94
  10. theorem OAI.SK.Analytic.weightedHierarchyReplica_sum line 102
  11. theorem OAI.SK.Analytic.weightedHierarchyReplica_const_mul line 110
  12. theorem OAI.SK.Analytic.weightedHierarchyReplica_separable_square line 116