OAI/Analysis/Steinitz/Predictor.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Predictor-column energy and exact feedback cancellation.

  1. def OAI.EuclideanSteinitz.Filter.rawRow line 14
  2. def OAI.EuclideanSteinitz.Filter.predictorRows line 16
  3. lemma OAI.EuclideanSteinitz.Filter.predictorRows_length line 21
  4. lemma OAI.EuclideanSteinitz.Filter.predictorRows_get line 28
  5. lemma OAI.EuclideanSteinitz.Filter.vectorMass_vecMul line 41
  6. lemma OAI.EuclideanSteinitz.Filter.rawRow_mass line 48
  7. lemma OAI.EuclideanSteinitz.Filter.rawRow_zero_col line 62
  8. lemma OAI.EuclideanSteinitz.Filter.rawRow_loss line 66
  9. lemma OAI.EuclideanSteinitz.Filter.predictor_column_budget line 88
  10. lemma OAI.EuclideanSteinitz.Filter.insertion_budget line 107
  11. lemma OAI.EuclideanSteinitz.Filter.predictor_column_bound line 128
  12. lemma OAI.EuclideanSteinitz.Filter.predictor_row_bound line 139
  13. lemma OAI.EuclideanSteinitz.Filter.predictor_future_zero line 149
  14. def OAI.EuclideanSteinitz.Filter.rowMap line 173
  15. lemma OAI.EuclideanSteinitz.Filter.rowMap_apply line 175
  16. lemma OAI.EuclideanSteinitz.Filter.rowMap_single line 180
  17. lemma OAI.EuclideanSteinitz.Filter.rowMatrix_norm line 183
  18. lemma OAI.EuclideanSteinitz.Filter.rawRow_eval line 193
  19. def OAI.EuclideanSteinitz.Filter.noiseRow line 198
  20. lemma OAI.EuclideanSteinitz.Filter.noiseRow_mass line 202
  21. lemma OAI.EuclideanSteinitz.Filter.noiseRow_eval line 208
  22. lemma OAI.EuclideanSteinitz.Filter.insert_mulVec_eq line 213
  23. lemma OAI.EuclideanSteinitz.Filter.step_cancel line 217
  24. lemma OAI.EuclideanSteinitz.Filter.run_prefix_cancel line 227