OAI/Analysis/HyperbolicCones/
455 declarations, 0 contain sorry, 0 declared as axioms; 101 files
Files
- BlockNormalization.lean 1 declarations
- BlockReduction.lean 3 declarations
- BlockScaling.lean 2 declarations
- ComplexPositive.lean 6 declarations
- CompressionBasic.lean 2 declarations
- ConeContinuity.lean 3 declarations
- ConeInterior.lean 1 declarations
- ConeMatrix.lean 8 declarations
- ConeOpen.lean 4 declarations
- ConePositive.lean 1 declarations
- ConeRoots.lean 2 declarations
- ConeZero.lean 3 declarations
- CongruenceMaps.lean 8 declarations
- ConstantRank.lean 2 declarations
- Coordinates.lean 6 declarations
- Deformation.lean 1 import, no declarations
- DeformationBasic.lean 16 declarations
- DeformationCone.lean 5 declarations
- DeformationFamily.lean 9 declarations
- DeformationRoots.lean 10 declarations
- FiniteTopology.lean 8 declarations
- Form.lean 3 imports, no declarations
- FormBasic.lean 15 declarations
- FormPositive.lean 8 declarations
- FormRigidity.lean 14 declarations
- FormSign.lean 2 declarations
- GramProjection.lean 5 declarations
- Hyperbolicity.lean 2 declarations
- InverseBounds.lean 4 declarations
- InverseOrder.lean 4 declarations
- KernelLimit.lean 3 declarations
- KernelLocal.lean 1 declarations
- KernelSmooth.lean 5 declarations
- KernelSpectrum.lean 9 declarations
- KernelTangent.lean 1 declarations
- LeastEigenvalue.lean 9 declarations
- LineEvaluation.lean 3 declarations
- LinePolynomial.lean 5 declarations
- LineShift.lean 3 declarations
- Main.lean 2 declarations
- MatrixBasic.lean 11 declarations
- MatrixComplex.lean 5 declarations
- MatrixLinear.lean 3 declarations
- MatrixPositive.lean 3 declarations
- MatrixResolvent.lean 3 declarations
- MaxEigenvalue.lean 2 declarations
- Model.lean 35 declarations
- NormBounds.lean 4 declarations
- NormCongruence.lean 3 declarations
- NormIdentity.lean 2 declarations
- NormLimits.lean 4 declarations
- NormThreshold.lean 3 declarations
- OperatorEntries.lean 5 declarations
- Pencil.lean 1 declarations
- PencilBlocks.lean 6 declarations
- PencilCompression.lean 2 declarations
- PencilConjugation.lean 6 declarations
- PencilKernel.lean 3 declarations
- PencilLimit.lean 8 declarations
- PencilOrder.lean 5 declarations
- PencilRecovery.lean 5 declarations
- PencilRegularization.lean 4 declarations
- PencilRepresentation.lean 3 declarations
- PencilSplit.lean 2 declarations
- PencilTopology.lean 3 declarations
- PolynomialBasic.lean 3 declarations
- PolynomialEvaluation.lean 6 declarations
- PolynomialHomogeneous.lean 5 declarations
- PolynomialScaling.lean 5 declarations
- PositiveCore.lean 1 declarations
- PositiveMaps.lean 3 declarations
- PositivePath.lean 1 declarations
- QuadraticDeformation.lean 13 declarations
- RankInverse.lean 3 declarations
- RankNorm.lean 8 declarations
- RankQuadratics.lean 3 declarations
- RawBlocks.lean 1 declarations
- RescalingBasic.lean 2 declarations
- ResidualBound.lean 2 declarations
- ResidualOrder.lean 3 declarations
- ResolventFormula.lean 4 declarations
- ResolventImaginary.lean 5 declarations
- ResolventPositive.lean 3 declarations
- RootFactorization.lean 4 declarations
- ScalingAlgebra.lean 5 declarations
- ShiftValue.lean 2 declarations
- SpectralBounds.lean 4 declarations
- SpectralContinuity.lean 2 declarations
- SpectralProjection.lean 2 declarations
- SplitAssembly.lean 2 declarations
- SplitBasic.lean 7 declarations
- SplitFrame.lean 4 declarations
- StrictBlock.lean 2 declarations
- TangentBasic.lean 5 declarations
- TangentExpansion.lean 2 declarations
- TangentFigure.lean 9 declarations
- TangentIdentity.lean 1 declarations
- TangentLimit.lean 1 declarations
- TangentObstruction.lean 1 declarations
- TangentRigidity.lean 1 declarations
- ZeroPolynomial.lean 4 declarations