OAI/Probability/InvariantIsing/Spectral/
545 declarations, 0 contain sorry, 0 declared as axioms; 128 files
Files
- ClippedEmpiricalTransform.lean 2 declarations
- CompactFiniteTestControl.lean 1 declarations
- CompactPartitionContinuity.lean 3 declarations
- CompactPartitionPressure.lean 6 declarations
- CompactResolventTests.lean 3 declarations
- CompactSpectralClipping.lean 6 declarations
- CompactSpectralPartition.lean 17 declarations
- CompactSpectralPressure.lean 1 declarations
- CompactSpectralQuantizers.lean 1 declarations
- CompactTestsInMeasure.lean 1 declarations
- EmpiricalClippingDistance.lean 1 declarations
- EmpiricalFieldMoment.lean 1 declarations
- EmpiricalLawContinuity.lean 2 declarations
- EmpiricalSpectralLaw.lean 5 declarations
- FiniteSpectralContinuity.lean 7 declarations
- FiniteSpectralMeasure.lean 6 declarations
- HermitianEigenvalueLimits.lean 2 declarations
- HermitianEigenvalueRoots.lean 4 declarations
- MeasureInverseContinuity.lean 4 declarations
- MeasureMagneticContinuity.lean 1 declarations
- MeasureMagneticLawInvariance.lean 1 declarations
- MeasureMagneticTransport.lean 1 declarations
- MeasurePointMass.lean 3 declarations
- MeasureRBounds.lean 7 declarations
- MeasureResolvent.lean 14 declarations
- MeasureSpectralContinuity.lean 3 declarations
- MeasureVariationalContinuity.lean 4 declarations
- MeasureWeakResolvent.lean 2 declarations
- PositiveRankOneInverse.lean 1 declarations
- PositiveRankOneQuadratic.lean 2 declarations
- PositiveResolventBounds.lean 4 declarations
- PositiveResolventContraction.lean 1 declarations
- PositiveResolventEigenbasis.lean 2 declarations
- PositiveResolventFluctuation.lean 2 declarations
- PositiveResolventSpectrum.lean 3 declarations
- PositiveResolventVariance.lean 2 declarations
- PositiveSpectralLabels.lean 6 declarations
- PositiveSpectralPartition.lean 3 declarations
- PositiveSpectralRounding.lean 2 declarations
- ResolventLipschitz.lean 1 declarations
- ResolventMeasureUniqueness.lean 5 declarations
- ResolventMomentIdentification.lean 1 declarations
- ResolventPowerDerivative.lean 4 declarations
- ScaledSpectralLaw.lean 6 declarations
- ScaledSpectralSigned.lean 2 declarations
- SelectedAlphabetPressure.lean 1 declarations
- SelectedCompactPressure.lean 1 declarations
- SelectedOrbitAlmostSure.lean 1 declarations
- SelectedPartitionPressure.lean 2 declarations
- SelectedSpectralExcess.lean 2 declarations
- SelectedSpectralPressure.lean 2 declarations
- SelectedTypePressure.lean 1 declarations
- Spectral.lean 13 declarations
- SpectralApproximationSqueeze.lean 1 declarations
- SpectralArrayDiagonalLimit.lean 2 declarations
- SpectralArrayEnergy.lean 6 declarations
- SpectralArrayGG.lean 20 declarations
- SpectralArrayGeometry.lean 13 declarations
- SpectralBallPartition.lean 6 declarations
- SpectralBallQuantizer.lean 4 declarations
- SpectralBoundedSynchronization.lean 1 declarations
- SpectralCalculus.lean 17 declarations
- SpectralCanonicalIdentification.lean 1 declarations
- SpectralCanonicalSymbols.lean 5 declarations
- SpectralCanonicalWard.lean 1 declarations
- SpectralClipping.lean 7 declarations
- SpectralComparison.lean 6 declarations
- SpectralContactContradiction.lean 1 declarations
- SpectralContactTails.lean 3 declarations
- SpectralContinuity.lean 4 declarations
- SpectralConvexity.lean 3 declarations
- SpectralCountAlignment.lean 4 declarations
- SpectralCountComparison.lean 4 declarations
- SpectralCountEndpoint.lean 3 declarations
- SpectralCovariance.lean 7 declarations
- SpectralDeficitDerivative.lean 2 declarations
- SpectralDensityContinuity.lean 3 declarations
- SpectralDiagonalCenters.lean 4 declarations
- SpectralDiagonalPerturbation.lean 5 declarations
- SpectralDiagonalWardLimits.lean 4 declarations
- SpectralEndpoints.lean 7 declarations
- SpectralEnergy.lean 14 declarations
- SpectralEnergyPrimitive.lean 2 declarations
- SpectralExcess.lean 5 declarations
- SpectralExcessContinuity.lean 2 declarations
- SpectralExcessScale.lean 1 declarations
- SpectralExistence.lean 3 declarations
- SpectralExtremeLimits.lean 5 declarations
- SpectralFubini.lean 3 declarations
- SpectralGG.lean 7 declarations
- SpectralGGGeometry.lean 9 declarations
- SpectralGroupIdentification.lean 2 declarations
- SpectralGroupMass.lean 2 declarations
- SpectralGroupRoots.lean 9 declarations
- SpectralLabelCounts.lean 4 declarations
- SpectralMultiplicity.lean 1 declarations
- SpectralNullBoundaryCover.lean 1 declarations
- SpectralNullBoundaryPartition.lean 3 declarations
- SpectralOrder.lean 4 declarations
- SpectralOverlapPaths.lean 18 declarations
- SpectralPartition.lean 16 declarations
- SpectralPartitionCounts.lean 1 declarations
- SpectralPartitionIndex.lean 4 declarations
- SpectralPartitionLaw.lean 3 declarations
- SpectralPartitionPaths.lean 8 declarations
- SpectralPartitionPressure.lean 1 declarations
- SpectralPathLimit.lean 1 declarations
- SpectralPathSynchronization.lean 6 declarations
- SpectralPaths.lean 7 declarations
- SpectralPermutation.lean 9 declarations
- SpectralPerturbedBlocks.lean 2 declarations
- SpectralPrimitive.lean 4 declarations
- SpectralProjectionMass.lean 5 declarations
- SpectralQuantileMoments.lean 6 declarations
- SpectralQuantilePaths.lean 7 declarations
- SpectralQuantileSynchronization.lean 3 declarations
- SpectralQuantizationWeak.lean 1 declarations
- SpectralReconstruction.lean 2 declarations
- SpectralReplicaLaw.lean 10 declarations
- SpectralReplicaProduct.lean 3 declarations
- SpectralSymbols.lean 4 declarations
- SpectralTemperature.lean 3 declarations
- SpectralTemperatureFunctional.lean 7 declarations
- SpectralTreeTail.lean 2 declarations
- SpectralWardAlgebra.lean 5 declarations
- SpectralWardLimits.lean 3 declarations
- SpectralWardPaths.lean 2 declarations
- SpectralWardSymbols.lean 2 declarations