OAI/LinearAlgebra/MatrixFields/Histories/InverseLinearRecovery.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.ExactRecovery.delete line 19
  2. def OAI.MatrixAllFields.MatrixMultiplication.ExactRecovery.presence line 23
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactRecovery.mem_presence line 27
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactRecovery.restrict_rectangles line 31
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactRecovery.repair_of_cover line 50
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactRecovery.card_mask_rectangles line 93
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactRecovery.repair_of_counting line 100
  8. def OAI.MatrixAllFields.MatrixMultiplication.OrbitCounting.orbitSet line 156
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitCounting.smul_mem_orbitSet line 158
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitCounting.card_fiber_eq line 161
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitCounting.card_group line 174
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitCounting.bad_shift_count line 192
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitCounting.bad_shift_bound line 215
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitCounting.bad_shift_fraction line 222
  15. def OAI.MatrixAllFields.MatrixMultiplication.OrbitRecovery.badShifts line 250
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitRecovery.badShifts_card_le line 256
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitRecovery.badShifts_fraction_le_at line 275
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitRecovery.floor_loss_fraction line 304
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitRecovery.repair_from_orbit_loss line 310
  20. def OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.shiftCount line 366
  21. def OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.replicationCount line 369
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.shiftCount_pos line 372
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.support_loss_bound line 381
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.cardinal_budget line 400
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.exists_cover line 422
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.shiftCount_div_nat_le line 441
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.tendsto_shiftCount_div_nat line 456
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.eventually_shiftCount_div_nat_le_log line 473
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.log_replicationCount line 504
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.eventually_log_replicationCount_div_nat_le_log line 510
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.tendsto_log_replicationCount_div_nat line 520
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.eventually_replicationCount_le_exp line 530
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryGrowth.tendsto_log_prod_div_nat line 541
  34. abbrev OAI.MatrixAllFields.MatrixMultiplication.InverseLinearRecovery.MaskRectangles line 569
  35. def OAI.MatrixAllFields.MatrixMultiplication.InverseLinearRecovery.RecoveredBy line 571
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.InverseLinearRecovery.repair_inverse_linear line 579
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.InverseLinearRecovery.card_recovery_copies line 607
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.InverseLinearRecovery.subexponential_copies line 613