OAI/Analysis/InterpolatedFactors/Matrices.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Amplification.matrixBlock line 15
  2. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_apply line 18
  3. theorem OAI.FreeGroupFactorMain.Amplification.productCoordinate_productSingle line 23
  4. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_matrixBlock line 29
  5. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_zero line 35
  6. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_mul line 39
  7. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_star line 50
  8. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_mem line 59
  9. def OAI.FreeGroupFactorMain.Amplification.finiteMatrix line 68
  10. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_sum line 71
  11. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_finiteMatrix line 80
  12. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_finiteMatrix_out line 85
  13. theorem OAI.FreeGroupFactorMain.Amplification.finiteMatrix_mem line 99
  14. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_add line 104
  15. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_smul line 109
  16. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_sum line 114
  17. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_mul_finiteMatrix line 121
  18. theorem OAI.FreeGroupFactorMain.Amplification.finiteMatrix_mul line 131
  19. theorem OAI.FreeGroupFactorMain.Amplification.finiteMatrix_add line 141
  20. theorem OAI.FreeGroupFactorMain.Amplification.finiteMatrix_star line 146
  21. theorem OAI.FreeGroupFactorMain.Amplification.finiteMatrix_smul line 152
  22. def OAI.FreeGroupFactorMain.Amplification.finiteDiagonal line 157
  23. theorem OAI.FreeGroupFactorMain.Amplification.finiteDiagonal_sum line 160
  24. theorem OAI.FreeGroupFactorMain.Amplification.finiteDiagonal_mul line 170
  25. theorem OAI.FreeGroupFactorMain.Amplification.finiteDiagonal_star line 178
  26. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_sandwich line 186
  27. theorem OAI.FreeGroupFactorMain.Amplification.finiteDiagonal_sandwich line 192
  28. def OAI.FreeGroupFactorMain.Amplification.finiteProjection line 201
  29. theorem OAI.FreeGroupFactorMain.Amplification.finiteProjection_projection line 207
  30. theorem OAI.FreeGroupFactorMain.Amplification.finiteDiagonal_entries line 219
  31. abbrev OAI.FreeGroupFactorMain.Amplification.FiniteCorner line 232
  32. theorem OAI.FreeGroupFactorMain.Amplification.finiteCorner_entry_sandwich line 235
  33. def OAI.FreeGroupFactorMain.Amplification.finiteCornerEntry line 243
  34. theorem OAI.FreeGroupFactorMain.Amplification.finiteCorner_reconstruct line 256
  35. theorem OAI.FreeGroupFactorMain.Amplification.finiteCorner_ext line 267
  36. def OAI.FreeGroupFactorMain.Amplification.finiteCornerOfMatrix line 276
  37. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerEntry_ofMatrix line 296
  38. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerEntry_add line 303
  39. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerEntry_smul line 311
  40. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerEntry_star line 319
  41. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerEntry_mul line 326
  42. def OAI.FreeGroupFactorMain.Amplification.finiteCornerIso line 337