OAI/Analysis/Pureness/Projections/
128 declarations, 0 contain sorry, 0 declared as axioms; 37 files
Files
- AWFactorCorners.lean 2 declarations
- FiniteSpectralIntegral.lean 7 declarations
- FiniteSpectralIntegralAbelian.lean 2 declarations
- FiniteSpectralIntegralBounds.lean 6 declarations
- FiniteSpectralIntegralCommuting.lean 1 declarations
- FiniteSpectralIntegralContinuity.lean 3 declarations
- FiniteSpectralIntegralOrder.lean 2 declarations
- FiniteSpectralIntegralOrthogonal.lean 7 declarations
- FiniteSpectralIntegralPolar.lean 4 declarations
- FiniteSpectralIntegralPositivity.lean 6 declarations
- FiniteSpectralIntegralRankRecovery.lean 4 declarations
- FiniteSpectralIntegralRootBounds.lean 4 declarations
- FiniteSpectralIntegralRootLimit.lean 3 declarations
- FiniteSpectralIntegralScaling.lean 5 declarations
- FiniteSpectralTwoQuasitrace.lean 5 declarations
- OrthogonalPartialIsometry.lean 3 declarations
- PartialIsometryExtension.lean 3 declarations
- PartialIsometryMatch.lean 7 declarations
- ProjectionDimension.lean 6 declarations
- ProjectionDimensionQuasitrace.lean 3 declarations
- ProjectionDimensionUniqueness.lean 3 declarations
- QuotientEquivalentSubprojections.lean 1 declarations
- QuotientFiniteSpectralApproximation.lean 1 declarations
- QuotientMatchLimits.lean 2 declarations
- QuotientMaximalMatch.lean 2 declarations
- QuotientNonzeroSpectralCorner.lean 3 declarations
- QuotientPartialIsometryLimits.lean 3 declarations
- QuotientPartitionRefinement.lean 4 declarations
- QuotientProjectionComparison.lean 2 declarations
- QuotientProjectionDeterminesValue.lean 2 declarations
- QuotientProjectionJoins.lean 3 declarations
- QuotientProjectionLimits.lean 5 declarations
- QuotientProjectionNormality.lean 3 declarations
- QuotientSpectralBands.lean 5 declarations
- QuotientSpectralPartition.lean 3 declarations
- SpectralCornerPartialIsometry.lean 2 declarations
- UltralimitAWNormality.lean 1 declarations