OAI/Analysis/IrrationalRotation/Spectral/
420 declarations, 0 contain sorry, 0 declared as axioms; 64 files
Files
- AffiliatedPositiveResolvent.lean 7 declarations
- BrownDiracReduction.lean 5 declarations
- CFCLogSeries.lean 10 declarations
- CircleVectorDeterminant.lean 2 declarations
- DeterminantContinuity.lean 7 declarations
- DeterminantHomogeneity.lean 7 declarations
- DeterminantNormBound.lean 7 declarations
- DeterminantRegularization.lean 5 declarations
- DeterminantScalarHomogeneity.lean 3 declarations
- DeterminantSemicontinuity.lean 7 declarations
- DeterminantUnitary.lean 4 declarations
- DeterminantWeightBridge.lean 5 declarations
- FieldDiagonalPolar.lean 4 declarations
- FieldResolvent.lean 15 declarations
- FieldResolventTransport.lean 3 declarations
- FullPolarDiffuseCriterion.lean 1 declarations
- GeneralPolar.lean 31 declarations
- InvertibleDeterminant.lean 7 declarations
- PartialResolventCalculus.lean 18 declarations
- PartialResolventIntertwining.lean 3 declarations
- PhaseBlockQuasinilpotent.lean 1 declarations
- PolarAlgebraSeparation.lean 4 declarations
- PolarEmptyFamily.lean 2 declarations
- PolarFactor.lean 8 declarations
- PolarOrbitInvariance.lean 10 declarations
- PolarStructure.lean 15 declarations
- PositivePartialResolvent.lean 7 declarations
- PositivePartialResolventAlternative.lean 20 declarations
- ProductBlockQuasinilpotent.lean 2 declarations
- ProductBrownMeasure.lean 3 declarations
- ProductDeterminant.lean 12 declarations
- ProductDeterminantBounds.lean 1 declarations
- ProductFinitePolar.lean 12 declarations
- ProductPolarAssembly.lean 3 declarations
- ProductPolarComplete.lean 4 declarations
- ProductPolarDiffuse.lean 5 declarations
- ProductPolarModulus.lean 2 declarations
- ProductPolarModulusComplex.lean 5 declarations
- ProductPolarRange.lean 6 declarations
- ProductQuasinilpotent.lean 10 declarations
- ProductSpectralBundle.lean 2 declarations
- ProductTracialSpectral.lean 5 declarations
- ProductWeightPolar.lean 6 declarations
- QuasinilpotentBrown.lean 3 declarations
- QuasinilpotentCommuting.lean 6 declarations
- QuasinilpotentDeterminantReduction.lean 3 declarations
- QuasinilpotentNonscalar.lean 4 declarations
- QuasinilpotentPotentialContinuity.lean 6 declarations
- QuasinilpotentSeries.lean 13 declarations
- QuasinilpotentTraceDerivative.lean 4 declarations
- RegularPolarAtomicity.lean 5 declarations
- RotationDeterminant.lean 5 declarations
- RotationQuasinilpotent.lean 5 declarations
- RotationResolvent.lean 6 declarations
- RotationTracialDeterminant.lean 9 declarations
- ScalarDeterminantZero.lean 5 declarations
- Spectral.lean 8 declarations
- SpectralNaturality.lean 8 declarations
- TracialInvertibleDeterminant.lean 4 declarations
- UnitarySpectralTransport.lean 4 declarations
- VectorDeterminantBounds.lean 5 declarations
- VectorSpectral.lean 4 declarations
- WeightedShiftPolar.lean 15 declarations
- WeightedShiftPolarIdentification.lean 2 declarations