`OAI/Topology/CoarseAssembly/`

2083 declarations, 0 contain sorry, 0 declared as axioms; 334 files

Files

AlgebraicRoe.lean 8 declarations
AmpleRipsFamily.lean 4 declarations
AnalyticFamilyIndex.lean 3 declarations
AnalyticKHomology.lean 10 declarations
Assembly.lean 5 declarations
Averaging.lean 13 declarations
AveragingEnergy.lean 8 declarations
AveragingPropagation.lean 8 declarations
BilateralShift.lean 10 declarations
BinaryCycle.lean 3 declarations
BinaryHilbertSum.lean 18 declarations
BlockIsometryRelations.lean 5 declarations
BlockOperators.lean 9 declarations
BlockSumDecomposition.lean 4 declarations
BoundaryAssemblyMaps.lean 13 declarations
BoundaryComponents.lean 6 declarations
BoundaryConclusion.lean 6 declarations
BoundaryEmbedding.lean 8 declarations
BoundaryGeometry.lean 6 declarations
BoundaryIndex.lean 2 declarations
BoundaryLoopMaps.lean 16 declarations
BoundaryRoePerturbation.lean 1 declarations
BoundaryWalks.lean 14 declarations
BoundedCycleTransform.lean 5 declarations
BoundedFamilyHomotopy.lean 5 declarations
BoundedFamilySubdivision.lean 7 declarations
BoundedGeometry.lean 8 declarations
BoundedRipsTransform.lean 3 declarations
BoundedTransform.lean 3 declarations
BoundedTransformCompact.lean 6 declarations
BoundedTransformNaturality.lean 3 declarations
CayleyBoundary.lean 8 declarations
CayleyContinuity.lean 3 declarations
CayleyIntertwining.lean 4 declarations
CayleyNaturality.lean 3 declarations
CayleyNonunitalNaturality.lean 5 declarations
CayleyNormControl.lean 5 declarations
CayleyUnitization.lean 10 declarations
CharacterExtension.lean 9 declarations
ChosenHolonomy.lean 3 declarations
CircleCoefficient.lean 8 declarations
CircleInputReduction.lean 1 declarations
CirclePairing.lean 6 declarations
CircleSequenceRepresentation.lean 5 declarations
ClopenNaturality.lean 2 declarations
ClopenRestriction.lean 6 declarations
CocycleCircleMap.lean 15 declarations
CocyclePathLifting.lean 8 declarations
CoefficientDecomposition.lean 4 declarations
CoefficientFamilyMultiplier.lean 5 declarations
CoefficientInclusion.lean 2 declarations
CoefficientIsometry.lean 9 declarations
CoefficientRoeHom.lean 4 declarations
CompactBlockSum.lean 9 declarations
CompactFamilyHomotopy.lean 4 declarations
CompactFamilyMap.lean 4 declarations
CompactFunctionalCalculus.lean 4 declarations
CompactHomotopy.lean 8 declarations
CompactIndex.lean 2 declarations
CompactIndexPairing.lean 7 declarations
ComponentHilbertInclusion.lean 4 declarations
ComponentInclusion.lean 2 declarations
ComponentRestrictionNaturality.lean 2 declarations
ComponentRipsPreimage.lean 1 declarations
ConcreteIndexDiagrams.lean 7 declarations
ConcreteIndexFamilies.lean 6 declarations
ConcreteIndexSquares.lean 4 declarations
ConcretePersistence.lean 3 declarations
ConcreteSpaces.lean 10 declarations
ConcreteTransfer.lean 2 declarations
ConcreteTransferMaps.lean 5 declarations
CongruenceEdgeOperators.lean 8 declarations
CongruenceElementary.lean 17 declarations
CongruenceFibers.lean 5 declarations
CongruenceMaps.lean 6 declarations
CongruenceQuotients.lean 8 declarations
CongruenceSpectral.lean 8 declarations
CongruenceSurjective.lean 3 declarations
Conjugation.lean 5 declarations
ConstructedBoundaryAssembly.lean 3 declarations
ConstructedConclusion.lean 1 declarations
ContinuousUnitalization.lean 8 declarations
ControlledBoundaryClass.lean 6 declarations
ControlledBoundaryHomotopy.lean 1 declarations
ControlledBoundaryNearby.lean 1 declarations
ControlledCoarseAssembly.lean 7 declarations
ControlledMatrices.lean 10 declarations
ControlledRipsCoarsening.lean 13 declarations
ControlledRipsCoordinates.lean 4 declarations
ControlledRipsCycles.lean 11 declarations
CountableAdditivity.lean 9 declarations
CountableHilbertSum.lean 6 declarations
CycleCompactPerturbation.lean 7 declarations
CycleDirectSumNormalization.lean 3 declarations
CycleIndex.lean 10 declarations
CycleUnitaryNormalization.lean 2 declarations
Definitions.lean 198 declarations
DegenerateCutDown.lean 5 declarations
DegenerateRegularization.lean 6 declarations
DiagonalApproximation.lean 2 declarations
DiagonalBoundaryCoordinates.lean 4 declarations
DiagonalFamilyContinuity.lean 3 declarations
DiagonalFamilyDefect.lean 3 declarations
DiagonalMultiplier.lean 7 declarations
DiagonalSpatialFamily.lean 7 declarations
DirectSumIndex.lean 7 declarations
DirectSumIntertwining.lean 4 declarations
DiscConnected.lean 5 declarations
EmbeddingBoundaryComparison.lean 2 declarations
EmbeddingTransition.lean 7 declarations
EssentialCommutant.lean 4 declarations
EssentialToeplitz.lean 4 declarations
EssentialToeplitzIndex.lean 2 declarations
ExplicitBoundaryConclusion.lean 11 declarations
ExplicitBoundaryRepresentative.lean 11 declarations
ExplicitCircleFamily.lean 6 declarations
ExplicitCutDown.lean 10 declarations
ExplicitFamilyFilling.lean 5 declarations
ExplicitPersistence.lean 7 declarations
FamilyBoundaryAddition.lean 1 declarations
FamilyCoefficientEmbedding.lean 6 declarations
FamilyDecomposition.lean 3 declarations
FamilyEmbeddingIndependence.lean 2 declarations
FamilyFilling.lean 4 declarations
FiberConnected.lean 4 declarations
FiberConstants.lean 8 declarations
FiberDegree.lean 16 declarations
FiberEmbedding.lean 7 declarations
FiberedGraph.lean 9 declarations
FiberedPersistence.lean 10 declarations
FilledDisc.lean 14 declarations
FilledEdges.lean 14 declarations
FilledWalks.lean 4 declarations
FiniteCompactRoe.lean 3 declarations
FiniteCycle.lean 1 declarations
FiniteCycleDecomposition.lean 2 declarations
FiniteCycleSum.lean 8 declarations
FiniteFiberMaps.lean 16 declarations
FiniteHeadBoundary.lean 3 declarations
FiniteHeadNormalization.lean 9 declarations
FiniteLocalization.lean 5 declarations
FiniteRips.lean 4 declarations
FiniteTailIndependence.lean 1 declarations
FiniteWindingIndex.lean 4 declarations
FiniteWords.lean 8 declarations
FredholmInvertible.lean 2 declarations
FredholmModule.lean 4 declarations
FredholmParametrix.lean 4 declarations
FredholmSquare.lean 2 declarations
GraphFiberOperators.lean 3 declarations
GraphMetric.lean 5 declarations
HexagonSides.lean 17 declarations
HilbertHeadTail.lean 9 declarations
HilbertSum.lean 6 declarations
Holonomy.lean 7 declarations
HomogeneousReindex.lean 10 declarations
HomotopyFilling.lean 6 declarations
HomotopySubdivision.lean 1 declarations
InclusionFunctoriality.lean 3 declarations
InclusionModule.lean 6 declarations
IndexFamilyTransport.lean 1 declarations
IndexPairing.lean 5 declarations
InvolutionUnitaryPath.lean 6 declarations
InvolutiveNormalization.lean 10 declarations
IsometricDecomposition.lean 2 declarations
IsometricExtension.lean 5 declarations
IsometryDilation.lean 9 declarations
IsometryUnitary.lean 4 declarations
K1Nearby.lean 6 declarations
K1TwoByTwo.lean 11 declarations
KazhdanInput.lean 4 declarations
KernelProjection.lean 11 declarations
LateRipsCoarsening.lean 2 declarations
Lattice.lean 10 declarations
LatticeCharge.lean 14 declarations
LatticeHat.lean 17 declarations
LocalCompactPerturbation.lean 5 declarations
LocalizationContinuity.lean 5 declarations
LocalizationNormContinuity.lean 3 declarations
LocalizationUniformEstimate.lean 4 declarations
LocallyCompactAlgebra.lean 9 declarations
LocallyFinite.lean 7 declarations
LoopCircle.lean 7 declarations
MultiplicativeIndexPairing.lean 6 declarations
MultiplierBoundaryClass.lean 4 declarations
MultiplierBoundaryHomotopy.lean 2 declarations
MultiplierBoundaryNearby.lean 1 declarations
MultiplierIsometryInvariance.lean 7 declarations
MultiplierOrthogonalEmbeddings.lean 3 declarations
MultiplierUnitaryHomotopy.lean 6 declarations
NegativeCircleCycle.lean 6 declarations
NegativeProjection.lean 8 declarations
NonUnitalK1.lean 8 declarations
NonunitalUnitaryExtension.lean 3 declarations
NormalizedRipsFamily.lean 4 declarations
OperatorNormalization.lean 2 declarations
OrthogonalBlock.lean 8 declarations
OrthogonalCoordinates.lean 6 declarations
OrthogonalExtensionBoundary.lean 3 declarations
OrthogonalSumBoundary.lean 6 declarations
PartialIsometryDilation.lean 10 declarations
PartitionCompactPerturbation.lean 7 declarations
PartitionCompression.lean 5 declarations
PartitionInclusion.lean 7 declarations
PartitionIntertwining.lean 3 declarations
PartitionIsometry.lean 4 declarations
PartitionMapNorm.lean 3 declarations
PartitionSpatialControl.lean 4 declarations
PathFiberOperators.lean 5 declarations
Persistence.lean 4 declarations
PointCoefficient.lean 6 declarations
PointwiseEmbeddingTransition.lean 5 declarations
ProductIndex.lean 5 declarations
ProjectionBlocks.lean 8 declarations
ProjectionSwap.lean 11 declarations
ProjectionUnitaryPath.lean 11 declarations
ProperGeometry.lean 3 declarations
PseudolocalAlgebra.lean 12 declarations
PublishedInputReduction.lean 4 declarations
RawCycleIndex.lean 6 declarations
RealNormalization.lean 6 declarations
RegularConstants.lean 4 declarations
RegularizedCoarsening.lean 3 declarations
RegularizedCycle.lean 6 declarations
RegularizedPrecomposition.lean 4 declarations
RegularizedRipsFamily.lean 1 declarations
RegularizedRipsRelations.lean 3 declarations
RelativeHomotopy.lean 3 declarations
RelativeIsometry.lean 2 declarations
RelativeMultiplication.lean 4 declarations
RelativeNaturality.lean 1 declarations
RelativeNearby.lean 2 declarations
RelativePartialIsometry.lean 2 declarations
RelativeTwoByTwo.lean 8 declarations
RelativeTwoConjugation.lean 11 declarations
RelativeTwoDiagonal.lean 4 declarations
RelativeTwoHomotopy.lean 6 declarations
RelativeUnitary.lean 7 declarations
RepresentedCutDown.lean 5 declarations
RepresentedIndex.lean 11 declarations
RepresentedNormalization.lean 2 declarations
RipsBoundaryDegeneracy.lean 7 declarations
RipsBoundaryRepresentative.lean 4 declarations
RipsCompactSupport.lean 1 declarations
RipsDirectSumBoundary.lean 2 declarations
RipsEmbedding.lean 8 declarations
RipsEmbeddingIndependence.lean 4 declarations
RipsFamilyCompactPerturbation.lean 2 declarations
RipsFamilyInclusion.lean 2 declarations
RipsFamilyMap.lean 6 declarations
RipsFamilyRestriction.lean 3 declarations
RipsFiniteHomotopy.lean 2 declarations
RipsFiniteTail.lean 2 declarations
RipsFixedRepresentationHomotopy.lean 1 declarations
RipsInclusionNaturality.lean 8 declarations
RipsLocalization.lean 9 declarations
RipsMapCalculus.lean 7 declarations
RipsPartition.lean 4 declarations
RipsPathCoarsening.lean 4 declarations
RipsPaths.lean 12 declarations
RipsProperEmbedding.lean 3 declarations
RipsRealClass.lean 3 declarations
RipsRealization.lean 9 declarations
RipsReindex.lean 5 declarations
RipsScaleCompatibility.lean 8 declarations
RipsUniformHomotopy.lean 2 declarations
RipsUnitaryFamily.lean 3 declarations
RipsUnitaryLocalization.lean 6 declarations
RipsUnrestrictedHomotopy.lean 1 declarations
RipsWindingTest.lean 3 declarations
Roe.lean 12 declarations
RoeCalculus.lean 12 declarations
RoeCompactRows.lean 6 declarations
RoeIdealizer.lean 3 declarations
RoeInclusion.lean 8 declarations
RoeLocalCompactness.lean 4 declarations
RoeRows.lean 3 declarations
RoeTransfer.lean 5 declarations
SampledHomotopy.lean 10 declarations
SampledHomotopyDecomposition.lean 5 declarations
SampledHomotopyEstimates.lean 2 declarations
SampledRipsEstimates.lean 2 declarations
Sandwich.lean 2 declarations
SandwichNormControl.lean 2 declarations
ScalarCutDown.lean 9 declarations
ScalarCycleNormalization.lean 3 declarations
SeparableEmbedding.lean 2 declarations
SeparatedBoundaryCongruence.lean 2 declarations
SeparatedCoarseAssembly.lean 3 declarations
SeparatedFamilyBoundary.lean 3 declarations
SeparatedFamilyHomotopy.lean 1 declarations
SeparatedFamilyInclusion.lean 1 declarations
SeparatedFamilyNearby.lean 1 declarations
SeparatedFamilyPerturbation.lean 2 declarations
SeparatedGeometry.lean 5 declarations
SeparatedIndexCoarsening.lean 4 declarations
SeparatedIndexNaturality.lean 4 declarations
SeparatedRips.lean 4 declarations
SeparatedRipsIndex.lean 1 declarations
SeparatedUnion.lean 5 declarations
ShiftIndex.lean 9 declarations
ShortLoops.lean 17 declarations
SigmaCycle.lean 10 declarations
SigmaCycleRepresentation.lean 5 declarations
SigmaCycleRestriction.lean 8 declarations
SigmaFunctionNorms.lean 4 declarations
SpatialAveraging.lean 4 declarations
SpatialBlocks.lean 8 declarations
SpatialBoundaryNaturality.lean 2 declarations
SpatialLocalization.lean 7 declarations
StructureQuotient.lean 6 declarations
SummandComplement.lean 9 declarations
SupportedNormalization.lean 4 declarations
TensorFibers.lean 15 declarations
ToeplitzCompression.lean 7 declarations
ToeplitzProductIndex.lean 5 declarations
TopologicalK1.lean 14 declarations
TraceObstruction.lean 4 declarations
TraceSeparation.lean 6 declarations
TranscendentalUnit.lean 2 declarations
TransferCriterion.lean 3 declarations
TransferLift.lean 5 declarations
UnconditionalConclusion.lean 3 declarations
UniformCycleNormalization.lean 7 declarations
UniformSubdivision.lean 5 declarations
UnitalCycleInvertible.lean 1 declarations
UnitalCycleNormalization.lean 1 declarations
UnitalRepresentative.lean 5 declarations
UnitalStructureAlgebra.lean 7 declarations
UnitaryHomotopyIndex.lean 3 declarations
UnitaryIndex.lean 7 declarations
UnrestrictedBoundedHomotopy.lean 3 declarations
WindingHomotopy.lean 6 declarations
WindingIndexEvaluation.lean 4 declarations