OAI/Analysis/OInfinity/
1617 declarations, 0 contain sorry, 0 declared as axioms; 129 files
Files
- AffineReflectionPath.lean 19 declarations
- BandOperators.lean 5 declarations
- BandProducts.lean 7 declarations
- BergRotation.lean 37 declarations
- BergSeam.lean 17 declarations
- BergShift.lean 25 declarations
- BergTent.lean 14 declarations
- BergTower.lean 42 declarations
- BinaryFragmentation.lean 17 declarations
- BinaryLeafRows.lean 6 declarations
- BufferAbsorption.lean 32 declarations
- BufferAnchor.lean 4 declarations
- BufferedIteration.lean 8 declarations
- BufferedPaths.lean 8 declarations
- BufferedProperComparison.lean 2 declarations
- BufferedRelativeWitness.lean 2 declarations
- BufferedTail.lean 5 declarations
- CARCombination.lean 15 declarations
- CARShiftModes.lean 28 declarations
- CPAP.lean 19 declarations
- CancellationBandwidth.lean 6 declarations
- CancellationTransport.lean 6 declarations
- CanonicalBuffer.lean 7 declarations
- CanonicalBufferAbsorption.lean 2 declarations
- CanonicalShift.lean 15 declarations
- CentralBuffer.lean 1 declarations
- CentralBufferImage.lean 2 declarations
- CentralIsometries.lean 21 declarations
- ClockCancellation.lean 24 declarations
- ClockCocycleFamily.lean 9 declarations
- ClockCorrection.lean 20 declarations
- ClockFragmentation.lean 22 declarations
- ClockGram.lean 15 declarations
- ClockPolar.lean 10 declarations
- ClockTransport.lean 27 declarations
- ClockedBands.lean 12 declarations
- ClockedCancellation.lean 7 declarations
- CocycleCancellation.lean 5 declarations
- CocycleCentrality.lean 12 declarations
- CocycleFlip.lean 16 declarations
- CocycleGluing.lean 14 declarations
- CommonCornerShrink.lean 8 declarations
- CompressionTransfer.lean 6 declarations
- ConnectedCocycleGluing.lean 18 declarations
- ConnectedGeneratorWitness.lean 2 declarations
- ConnectedHalfFlipGenerators.lean 3 declarations
- ConnectedHalfFlipTheorem.lean 1 declarations
- ConnectedProperComparison.lean 6 declarations
- ConnectedRowCompletion.lean 3 declarations
- ControlledAbsorption.lean 6 declarations
- CornerContraction.lean 7 declarations
- CornerContractionPath.lean 16 declarations
- CornerShortPath.lean 8 declarations
- CornerStabilization.lean 8 declarations
- DyadicProjections.lean 25 declarations
- EvenCARRelations.lean 12 declarations
- EvenModeCAR.lean 18 declarations
- EvenRowCAR.lean 25 declarations
- EvenShiftModes.lean 23 declarations
- FiniteCAR.lean 26 declarations
- FinitePermutation.lean 16 declarations
- FiniteRowCompletion.lean 4 declarations
- FiniteRowDefect.lean 16 declarations
- FiniteRowIsometry.lean 14 declarations
- FiniteWords.lean 14 declarations
- FixedComplementPaths.lean 3 declarations
- FixedSparePath.lean 30 declarations
- FixedSpareStabilization.lean 20 declarations
- FockCompression.lean 21 declarations
- FockConvergence.lean 17 declarations
- FockRangeProjection.lean 10 declarations
- FockReturn.lean 11 declarations
- FockShift.lean 11 declarations
- HalfFlipRecursion.lean 49 declarations
- IncompleteBinaryPath.lean 12 declarations
- IncompleteCocycle.lean 20 declarations
- IncompleteTails.lean 11 declarations
- IteratedBandTransport.lean 7 declarations
- JointClock.lean 3 declarations
- JointCycleIdentity.lean 15 declarations
- JointRohlin.lean 13 declarations
- JointRohlinWitness.lean 9 declarations
- JointWordCycle.lean 6 declarations
- JordanWigner.lean 27 declarations
- JordanWignerEstimates.lean 16 declarations
- MaskedBandRows.lean 10 declarations
- MaskedRotations.lean 20 declarations
- MaskedShift.lean 12 declarations
- MixedComplement.lean 5 declarations
- MixedNegative.lean 12 declarations
- MixedSwap.lean 5 declarations
- MixedTower.lean 26 declarations
- NegativeBinary.lean 6 declarations
- NegativeComparison.lean 14 declarations
- NegativeCompletion.lean 17 declarations
- NegativeCorner.lean 19 declarations
- NegativeGlobal.lean 4 declarations
- NuclearModel.lean 12 declarations
- ProjectionCorner.lean 18 declarations
- ProperBufferAbsorption.lean 3 declarations
- RelativeCocycle.lean 9 declarations
- RelativeCompletedComparison.lean 2 declarations
- RelativeGramCorrection.lean 12 declarations
- RelativeUnitaryPath.lean 5 declarations
- RohlinGluing.lean 8 declarations
- RohlinPartitions.lean 9 declarations
- RohlinPolar.lean 4 declarations
- RohlinShift.lean 10 declarations
- RohlinUnitarity.lean 5 declarations
- RowCocycleDefect.lean 13 declarations
- RowCompletionBase.lean 5 declarations
- RowCompletionBuffer.lean 6 declarations
- ShrinkPaths.lean 6 declarations
- Simple.lean 14 declarations
- TailCancellationWitness.lean 4 declarations
- TensorApproximation.lean 9 declarations
- TensorGram.lean 11 declarations
- TensorNorm.lean 40 declarations
- ToeplitzCompression.lean 11 declarations
- TransportedBuffer.lean 7 declarations
- VacuumBufferAbsorption.lean 2 declarations
- VacuumCorner.lean 25 declarations
- VacuumSplit.lean 5 declarations
- ZeroCorner.lean 16 declarations
- ZeroCornerRows.lean 15 declarations
- ZeroUnitBuffer.lean 4 declarations
- ZeroUnitComparison.lean 4 declarations
- ZeroUnitCompletion.lean 9 declarations
- ZeroUnitRows.lean 3 declarations