OAI/Probability/CriticalZ3/Scales.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalScales.contourError line 12
  2. theorem OAI.CriticalScales.contourError_pos line 14
  3. theorem OAI.CriticalScales.contourError_lt_half line 15
  4. theorem OAI.CriticalScales.contour_power line 17
  5. theorem OAI.CriticalScales.contour_budget line 25
  6. theorem OAI.CriticalScales.error_budgets line 38
  7. def OAI.CriticalZ3.Model.law line 70
  8. def OAI.CriticalZ3.Model.InfiniteAt line 74
  9. def OAI.CriticalZ3.Model.SeedInfinite line 78
  10. instance OAI.CriticalZ3.Model.law_probability line 82
  11. theorem OAI.CriticalZ3.Model.law_eq_product line 85
  12. theorem OAI.CriticalZ3.Model.law_coe_eq_product line 88
  13. theorem OAI.CriticalZ3.Model.exists_seed line 94
  14. theorem OAI.CriticalZ3.Model.lower_quarterFaces line 100
  15. structure OAI.CriticalZ3.ScaleData line 110
  16. theorem OAI.CriticalZ3.exists_scales line 143
  17. theorem OAI.CriticalZ3.ScaleData.q_pos line 188
  18. theorem OAI.CriticalZ3.ScaleData.successCard_le line 190
  19. theorem OAI.CriticalZ3.ScaleData.success_bound line 193
  20. theorem OAI.CriticalZ3.ScaleData.extension_budget line 198