OAI/Probability/SKGap/Stability/OrdinaryClosure.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SKGapCutoff.Recipe.LocalConstants line 18
  2. def OAI.SKGapCutoff.Recipe.LocalConstants.argument line 37
  3. def OAI.SKGapCutoff.Recipe.LocalConstants.row line 38
  4. def OAI.SKGapCutoff.Recipe.LocalConstants.normBudget line 39
  5. def OAI.SKGapCutoff.Recipe.LocalConstants.traceCost line 40
  6. def OAI.SKGapCutoff.Recipe.LocalConstants.sourceCost line 42
  7. def OAI.SKGapCutoff.Recipe.LocalConstants.fieldCost line 45
  8. lemma OAI.SKGapCutoff.Recipe.LocalConstants.A_nonneg line 48
  9. lemma OAI.SKGapCutoff.Recipe.LocalConstants.argument_nonneg line 49
  10. lemma OAI.SKGapCutoff.Recipe.LocalConstants.row_nonneg line 50
  11. lemma OAI.SKGapCutoff.Recipe.LocalConstants.normBudget_nonneg line 51
  12. lemma OAI.SKGapCutoff.Recipe.LocalConstants.traceCost_nonneg line 53
  13. structure OAI.SKGapCutoff.Recipe.LocalOrdinaryInput line 58
  14. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.argument_bound line 80
  15. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.seed_bound line 84
  16. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.aux_bound line 87
  17. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.seed_partial_bound line 90
  18. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.aux_partial_bound line 93
  19. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.small line 97
  20. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.source_control line 104
  21. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.field_control line 130
  22. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.mean_bound line 137
  23. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.ordinary_local_closure line 145