OAI/Analysis/Steinitz/Filter.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Symmetric contraction updates and filtered matrix states.

  1. structure OAI.EuclideanSteinitz.Filter.Step line 12
  2. def OAI.EuclideanSteinitz.Filter.insert line 17
  3. def OAI.EuclideanSteinitz.Filter.Step.apply line 20
  4. def OAI.EuclideanSteinitz.Filter.Step.move line 23
  5. def OAI.EuclideanSteinitz.Filter.Step.Good line 26
  6. def OAI.EuclideanSteinitz.Filter.run line 29
  7. def OAI.EuclideanSteinitz.Filter.product line 33
  8. def OAI.EuclideanSteinitz.Filter.state line 37
  9. def OAI.EuclideanSteinitz.Filter.Fresh line 40
  10. lemma OAI.EuclideanSteinitz.Filter.insert_mul_transpose line 44
  11. lemma OAI.EuclideanSteinitz.Filter.mul_insert_transpose line 50
  12. lemma OAI.EuclideanSteinitz.Filter.insert_mul_transpose_zero line 56
  13. lemma OAI.EuclideanSteinitz.Filter.step_apply_column line 65
  14. lemma OAI.EuclideanSteinitz.Filter.Step.coisometry line 70
  15. lemma OAI.EuclideanSteinitz.Filter.rankOne_psd line 88
  16. lemma OAI.EuclideanSteinitz.Filter.Step.contract line 93
  17. lemma OAI.EuclideanSteinitz.Filter.Step.admissible line 98
  18. lemma OAI.EuclideanSteinitz.Filter.Step.fresh_tail line 103
  19. lemma OAI.EuclideanSteinitz.Filter.run_coisometry line 108
  20. lemma OAI.EuclideanSteinitz.Filter.product_contract line 123
  21. lemma OAI.EuclideanSteinitz.Filter.product_unit line 138
  22. lemma OAI.EuclideanSteinitz.Filter.state_posDef line 144
  23. lemma OAI.EuclideanSteinitz.Filter.insert_diagonal line 154
  24. lemma OAI.EuclideanSteinitz.Filter.Step.state_next line 163
  25. lemma OAI.EuclideanSteinitz.Filter.run_state line 186
  26. lemma OAI.EuclideanSteinitz.Filter.follow_old line 201
  27. lemma OAI.EuclideanSteinitz.Filter.insert_mul_zero line 212
  28. lemma OAI.EuclideanSteinitz.Filter.run_mul line 217
  29. def OAI.EuclideanSteinitz.Filter.newSet line 230
  30. lemma OAI.EuclideanSteinitz.Filter.mem_newSet line 233
  31. def OAI.EuclideanSteinitz.Filter.oldMask line 236
  32. def OAI.EuclideanSteinitz.Filter.oldQ line 237
  33. def OAI.EuclideanSteinitz.Filter.newQ line 239
  34. lemma OAI.EuclideanSteinitz.Filter.oldQ_eq line 242
  35. lemma OAI.EuclideanSteinitz.Filter.oldQ_add_newQ line 250
  36. lemma OAI.EuclideanSteinitz.Filter.oldQ_psd line 257
  37. lemma OAI.EuclideanSteinitz.Filter.newQ_psd line 264
  38. lemma OAI.EuclideanSteinitz.Filter.oldQ_sandwich line 271
  39. lemma OAI.EuclideanSteinitz.Filter.fresh_oldMask line 278
  40. lemma OAI.EuclideanSteinitz.Filter.fresh_newQ line 288
  41. lemma OAI.EuclideanSteinitz.Filter.run_oldMask line 297
  42. lemma OAI.EuclideanSteinitz.Filter.run_cross line 308
  43. lemma OAI.EuclideanSteinitz.Filter.old_state line 313
  44. lemma OAI.EuclideanSteinitz.Filter.run_old_state line 319
  45. lemma OAI.EuclideanSteinitz.Filter.run_old_cross line 326
  46. lemma OAI.EuclideanSteinitz.Filter.run_new_state line 332
  47. lemma OAI.EuclideanSteinitz.Filter.fresh_lift_new_zero line 344
  48. lemma OAI.EuclideanSteinitz.Filter.weighted_increment line 349