OAI/Probability/Contingency/PreparedResidual.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Prepared Residual.

  1. def OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.groupMass line 16
  2. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.group_sum line 21
  3. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.group_limit line 62
  4. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.mass_upper line 111
  5. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.mass_lower line 136
  6. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.stack_law line 177
  7. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.cached_selector line 191
  8. def OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.cacheMaximum line 224
  9. def OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.cacheWords line 226
  10. def OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.cacheInput line 229
  11. def OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.integerEntries line 232
  12. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.member_le_sum line 236
  13. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.cache_width line 246
  14. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.cache_total line 257
  15. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.cache_entries line 266
  16. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.integer_cache_sampler line 277
  17. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.entries_below line 315
  18. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.entries_lookup line 324
  19. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.finite_weights_law line 343
  20. def OAI.Contingency.residualVector line 365
  21. theorem OAI.Contingency.residualVector_sum line 368
  22. theorem OAI.Contingency.residual_cache_law line 374
  23. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.cache_maximum_size_le line 403
  24. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.integer_cache_rare_time line 416
  25. def OAI.Contingency.residualSelectionBudget line 461
  26. theorem OAI.Contingency.residual_cache_rare_time line 474
  27. theorem OAI.Contingency.residual_cache_corrected_limit line 509
  28. theorem OAI.Contingency.prepared_residual_stage line 534