OAI/Combinatorics/ThinTrees/RationalMatrix/InverseRealization.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Inverse realization.

  1. abbrev OAI.CurrentKS.Realization.BackSolve line 15
  2. abbrev OAI.CurrentKS.Realization.backSolveCode line 16
  3. abbrev OAI.CurrentKS.Realization.solveChild line 17
  4. abbrev OAI.CurrentKS.Realization.solveParent line 18
  5. abbrev OAI.CurrentKS.Realization.solveColumnCode line 19
  6. abbrev OAI.CurrentKS.Realization.solveColumnBase line 20
  7. abbrev OAI.CurrentKS.Realization.solveColumnIndex line 21
  8. abbrev OAI.CurrentKS.Realization.solveColumnA line 22
  9. abbrev OAI.CurrentKS.Realization.solveColumnB line 23
  10. abbrev OAI.CurrentKS.Realization.solveColumnDim line 24
  11. abbrev OAI.CurrentKS.Realization.solveColumnEntries line 25
  12. abbrev OAI.CurrentKS.Realization.rhsCode line 27
  13. abbrev OAI.CurrentKS.Realization.rhsBase line 28
  14. abbrev OAI.CurrentKS.Realization.rhsIndex line 29
  15. def OAI.CurrentKS.Realization.solveRhs line 31
  16. instance OAI.CurrentKS.Realization.poly_solveRhs line 45
  17. def OAI.CurrentKS.Realization.solveTopRow line 47
  18. instance OAI.CurrentKS.Realization.poly_solveTopRow line 52
  19. def OAI.CurrentKS.Realization.liftColumnData line 54
  20. def OAI.CurrentKS.Realization.liftColumn line 63
  21. instance OAI.CurrentKS.Realization.poly_liftColumn line 72
  22. lemma OAI.CurrentKS.Realization.liftColumn_data line 76
  23. def OAI.CurrentKS.Realization.inverseLiftData line 110
  24. def OAI.CurrentKS.Realization.inverseLift line 113
  25. instance OAI.CurrentKS.Realization.poly_inverseLift line 115
  26. lemma OAI.CurrentKS.Realization.inverseLift_data line 119
  27. lemma OAI.CurrentKS.Realization.inverse_fold_correct line 129
  28. def OAI.CurrentKS.Realization.rationalInverseProgram line 140
  29. lemma OAI.CurrentKS.Realization.inverse_take_history line 146
  30. lemma OAI.CurrentKS.Realization.pivotTrace_posDef line 167
  31. lemma OAI.CurrentKS.Realization.SchurDesc.posDef line 175
  32. lemma OAI.CurrentKS.Realization.matrixInverse_parts line 179
  33. lemma OAI.CurrentKS.Realization.SchurDesc.inverse_wire line 188
  34. lemma OAI.CurrentKS.Realization.runsPoly_rationalInverse line 202