OAI/Analysis/MatrixSigning/Realization/ValueObjectiveRealization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.traceData line 11
  2. def OAI.CurrentKS.Realization.traceMatrix line 14
  3. lemma OAI.CurrentKS.Realization.trace_data line 20
  4. def OAI.CurrentKS.Realization.valueObjectiveData line 30
  5. def OAI.CurrentKS.Realization.valueObjective line 33
  6. lemma OAI.CurrentKS.Realization.valueObjective_data line 38
  7. def OAI.CurrentKS.Realization.valueCoeffsData line 47
  8. def OAI.CurrentKS.Realization.valueCoeffs line 50
  9. lemma OAI.CurrentKS.Realization.valueCoeffs_data line 57
  10. def OAI.CurrentKS.Realization.valuePencilData line 68
  11. def OAI.CurrentKS.Realization.valuePencil line 70
  12. lemma OAI.CurrentKS.Realization.valuePencil_data line 72