OAI/Probability/SKBarriers/Hierarchy/HierarchyJointLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.gaussian_convex_tilt_integrable line 22
  2. def OAI.SK.Analytic.hierarchyLogDensity line 41
  3. theorem OAI.SK.Analytic.hierarchyLogDensity_continuous line 47
  4. theorem OAI.SK.Analytic.hierarchyLogDensity_integrable line 56
  5. theorem OAI.SK.Analytic.hierarchyLogDensity_moment_integrable line 71
  6. def OAI.SK.Analytic.hierarchyLaw line 102
  7. theorem OAI.SK.Analytic.hierarchyJoint_integrable line 107
  8. theorem OAI.SK.Analytic.hierarchyLaw_probability line 125
  9. theorem OAI.SK.Analytic.hierarchyJointMoment_pos line 139
  10. theorem OAI.SK.Analytic.hierarchyLaw_moment line 148
  11. theorem OAI.SK.Analytic.hierarchyLaw_variance line 175