OAI/Probability/SKBarriers/Replicas/TripleTailValue.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.vectorStep_add_frozen line 18
  2. theorem OAI.SK.Analytic.vectorIncrementChain_pullback line 30
  3. theorem OAI.SK.Analytic.vectorIncrementChain_real line 38
  4. def OAI.SK.Analytic.tripleCoordinate line 44
  5. theorem OAI.SK.Analytic.tripleCoordinate_apply line 46
  6. theorem OAI.SK.Analytic.tripleStep_coordinate line 48
  7. theorem OAI.SK.Analytic.tripleStep_axis0 line 57
  8. theorem OAI.SK.Analytic.tripleStep_axis1 line 64
  9. theorem OAI.SK.Analytic.tripleStep_axis2 line 71
  10. theorem OAI.SK.Analytic.tripleTailBlock_value line 78
  11. theorem OAI.SK.Analytic.tripleTailSchedule_value line 84