OAI/Analysis/BiholderTransport/LinearAlgebra/
314 declarations, 0 contain sorry, 0 declared as axioms; 99 files
Files
- ActualRadial.lean 7 declarations
- ActualRelativeHessianBound.lean 2 declarations
- Aggregate.lean 2 declarations
- BilinearAbsorption.lean 4 declarations
- BilinearClose.lean 2 declarations
- BilinearCompact.lean 4 declarations
- BilinearDet.lean 7 declarations
- BilinearGainLimit.lean 2 declarations
- BilinearMatrix.lean 8 declarations
- BilinearMetricSpeedSquare.lean 1 declarations
- BranchDividedBaseline.lean 2 declarations
- BranchHessian.lean 2 declarations
- C11HessianLimits.lean 1 declarations
- Calculus.lean 2 declarations
- ChartFirstMatrix.lean 2 declarations
- ChartOuterMatrix.lean 1 declarations
- ChartTrueMatrix.lean 3 declarations
- CompactConorm.lean 1 declarations
- CompactCrossing.lean 3 declarations
- CompactLocalPositiveBounds.lean 1 declarations
- CompactQuadratic.lean 13 declarations
- CongruenceSpectrum.lean 4 declarations
- ContactDifferential.lean 6 declarations
- ContactStationarity.lean 1 declarations
- ConvexSpectrum.lean 2 declarations
- CurvedBlowup.lean 1 declarations
- DeterminantOrder.lean 6 declarations
- Diagonal.lean 3 declarations
- DiagonalCostConvexity.lean 1 declarations
- DividedHessian.lean 2 declarations
- EigenOrder.lean 5 declarations
- EndpointSpectrumBound.lean 2 declarations
- EnvelopeKernelHessian.lean 2 declarations
- FinitePositiveWeight.lean 3 declarations
- FirstMatrixLimit.lean 2 declarations
- FirstRank.lean 1 declarations
- FixedJoinSpectrum.lean 1 declarations
- FrameDeterminantClosure.lean 1 declarations
- FunctionalCoercive.lean 1 declarations
- HalfCostUniform.lean 1 declarations
- Hessian.lean 3 declarations
- HessianBounds.lean 3 declarations
- HessianCoordinates.lean 4 declarations
- HessianMixedOperator.lean 6 declarations
- HessianSequentialUpper.lean 1 declarations
- HessianSmooth.lean 6 declarations
- HessianUpperTransfer.lean 3 declarations
- InverseProfile.lean 5 declarations
- JensenHessian.lean 2 declarations
- JoinCongruence.lean 1 declarations
- JoinOperator.lean 4 declarations
- JoinSpectrum.lean 4 declarations
- LocalMountains.lean 3 declarations
- LocalNormalChart.lean 3 declarations
- LowerTaylor.lean 8 declarations
- MatrixNormDetFactorial.lean 3 declarations
- MaximumPolePositive.lean 1 declarations
- MaximumRank.lean 1 declarations
- MiddleScaling.lean 9 declarations
- MixedOperator.lean 5 declarations
- MixedTrivializationBound.lean 1 declarations
- MovingFamilyHessian.lean 1 declarations
- MovingHessianLimit.lean 5 declarations
- MovingSplit.lean 1 declarations
- NormDetAdjoint.lean 1 declarations
- NormDetCoercivity.lean 4 declarations
- NormalRelativeHessianBound.lean 1 declarations
- OperatorBounds.lean 2 declarations
- OuterActiveMatrix.lean 1 declarations
- OuterDisplacementJetBound.lean 4 declarations
- OuterTrueMatrix.lean 1 declarations
- Pole.lean 2 declarations
- PositiveBilinearBound.lean 3 declarations
- PositiveDetCompact.lean 2 declarations
- PositiveSingular.lean 6 declarations
- PrefixActionJets.lean 4 declarations
- QuadraticTest.lean 4 declarations
- RadialHessian.lean 2 declarations
- RankOneCoercive.lean 1 declarations
- RelativeHessianBound.lean 6 declarations
- RescaledJoinOperator.lean 4 declarations
- ScaledQuadraticBoundEigenvalues.lean 1 declarations
- ScaledSlack.lean 1 declarations
- ScaledSpectrum.lean 3 declarations
- SchurBackground.lean 7 declarations
- SchurCalculus.lean 6 declarations
- SchurEnvelope.lean 4 declarations
- SchurRatioTendstoBot.lean 1 declarations
- ShearBounds.lean 3 declarations
- ShearConvexity.lean 11 declarations
- ShearedOperator.lean 6 declarations
- ShearedSpectrum.lean 1 declarations
- SpectralContinuity.lean 6 declarations
- SplitActionSchur.lean 1 declarations
- SplitEndpointJets.lean 4 declarations
- StationarySchur.lean 3 declarations
- ThreeDeterminantsClose.lean 2 declarations
- TransverseConcavity.lean 4 declarations
- TrueCenterMatrix.lean 4 declarations