OAI/Analysis/MatrixSigning/Matrices/
667 declarations, 0 contain sorry, 0 declared as axioms; 82 files
Files
- DenseElimination.lean 4 declarations
- DenseMatrixSerialization.lean 12 declarations
- DenseMatrixUpdate.lean 6 declarations
- DenseRatMatrix.lean 7 declarations
- DerivInvHPath.lean 8 declarations
- DeterminantBounds.lean 8 declarations
- EliminationCallBounds.lean 5 declarations
- EliminationCompleteness.lean 2 declarations
- EliminationSoundness.lean 3 declarations
- FDerivTightPart.lean 4 declarations
- FinPivot.lean 6 declarations
- FinPivotPSD.lean 4 declarations
- HermitianMat.lean 32 declarations
- InnerMonoRightPsd.lean 8 declarations
- InnerRight.lean 9 declarations
- InvH.lean 15 declarations
- JetBoundInverseSandwich.lean 1 declarations
- JetBoundTightPart.lean 2 declarations
- JordanCLM.lean 10 declarations
- JordanCLMStrictPos.lean 1 declarations
- MatrixAddressArithmetic.lean 15 declarations
- MatrixCursorPreparation.lean 5 declarations
- MatrixReadProgram.lean 13 declarations
- MatrixRealSmul.lean 6 declarations
- MatrixWriteBridge.lean 2 declarations
- NormRetractH.lean 6 declarations
- OperatorNorm.lean 14 declarations
- OperatorNormSquare.lean 2 declarations
- PSDSeparation.lean 7 declarations
- Pivot.lean 13 declarations
- PivotControllerBody.lean 8 declarations
- PivotControllerCorrectness.lean 3 declarations
- PivotControllerLoop.lean 12 declarations
- PivotDecisionCorrectness.lean 5 declarations
- PivotDecisionMachine.lean 9 declarations
- PivotDecisionPorts.lean 5 declarations
- PivotHistory.lean 15 declarations
- PivotHistoryBounds.lean 6 declarations
- PivotHistoryMachine.lean 9 declarations
- PivotHistoryRun.lean 10 declarations
- PivotPSD.lean 8 declarations
- PivotReachableBounds.lean 10 declarations
- PivotReplayLoop.lean 9 declarations
- PivotRowBody.lean 10 declarations
- PivotRowClassify.lean 5 declarations
- PivotRowCorrectness.lean 5 declarations
- PivotRowFinish.lean 11 declarations
- PivotRowInitialize.lean 6 declarations
- PivotRowLoop.lean 14 declarations
- PivotRowRead.lean 2 declarations
- PivotScannerBounds.lean 10 declarations
- PivotTerminalMachine.lean 14 declarations
- PosLower.lean 2 declarations
- PreservedMatrixRetrieval.lean 2 declarations
- RankFactor.lean 4 declarations
- RationalElimination.lean 10 declarations
- RationalPSDDecision.lean 1 declarations
- RealDecode.lean 12 declarations
- RealTrace.lean 13 declarations
- RealTraceSum.lean 5 declarations
- RealifyHermitian.lean 2 declarations
- RetractH.lean 8 declarations
- RowDotBody.lean 12 declarations
- RowDotBounds.lean 13 declarations
- RowDotControl.lean 7 declarations
- RowDotCounter.lean 8 declarations
- RowDotMachine.lean 16 declarations
- RowDotModel.lean 16 declarations
- RowDotPrimitives.lean 15 declarations
- RowDotRegisters.lean 1 declarations
- Sandwich.lean 9 declarations
- Sandwich2.lean 6 declarations
- SandwichCLM.lean 6 declarations
- SandwichShiftInverse.lean 5 declarations
- SavedPivotPacketMachine.lean 11 declarations
- SavedPivotStack.lean 14 declarations
- Space.lean 16 declarations
- SquareScalarBound.lean 3 declarations
- SquareShift.lean 2 declarations
- TraceCLM.lean 18 declarations
- UniformElimination.lean 11 declarations
- UniformEliminationHeight.lean 3 declarations