OAI/Probability/SKBarriers/Hierarchy/HierarchyJointMoment.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.hierarchyJointMoment line 22
  2. theorem OAI.SK.Analytic.hierarchy_gauge_linear_variance line 27
  3. def OAI.SK.Analytic.coordinateProjection line 63
  4. theorem OAI.SK.Analytic.coordinateProjection_last line 68
  5. theorem OAI.SK.Analytic.coordinateProjection_castSucc line 71
  6. theorem OAI.SK.Analytic.coordinateSquare_eq_sum line 75
  7. theorem OAI.SK.Analytic.coordinateProjection_axis line 86
  8. theorem OAI.SK.Analytic.coordinateProjection_sign line 96
  9. def OAI.SK.Analytic.coordinateLinear line 107
  10. theorem OAI.SK.Analytic.coordinateLinear_apply line 110
  11. theorem OAI.SK.Analytic.coordinateLinear_axis line 114
  12. theorem OAI.SK.Analytic.coordinateLinear_sq_le line 118