OAI/Analysis/Pureness/Tensor/
355 declarations, 0 contain sorry, 0 declared as axioms; 72 files
Files
- AlgebraicQuotientTensorLift.lean 6 declarations
- AlgebraicStarDescent.lean 3 declarations
- AlgebraicTensorKernel.lean 7 declarations
- CauchySpatialEvaluation.lean 6 declarations
- CauchySpatialExtension.lean 6 declarations
- CauchySpatialFaithful.lean 1 declarations
- CauchySpatialNullDescent.lean 5 declarations
- CauchySpatialOriginalAgreement.lean 2 declarations
- CauchySpatialRange.lean 5 declarations
- CommutingAlgTensorInjective.lean 1 declarations
- CommutingFaithfulProducts.lean 3 declarations
- CommutingStarTensor.lean 2 declarations
- CommutingTensorClosure.lean 9 declarations
- CommutingTensorCoefficients.lean 3 declarations
- CommutingTensorInjective.lean 1 declarations
- CommutingTensorNorm.lean 5 declarations
- FiniteMatrixNuclearity.lean 1 declarations
- FiniteMatrixTensor.lean 5 declarations
- FiniteTensorEnvelopes.lean 5 declarations
- NuclearSpatialTensor.lean 4 declarations
- NuclearTensorNorm.lean 2 declarations
- OriginalFreeGroupSpatialTensor.lean 16 declarations
- OriginalScalarSpatialTensor.lean 11 declarations
- ScalarMatrixTensor.lean 5 declarations
- ScalarMatrixTensorCompletion.lean 9 declarations
- ScalarMatrixTensorFaithful.lean 3 declarations
- SpatialCenteredPolynomials.lean 6 declarations
- SpatialCommutingTensor.lean 10 declarations
- SpatialCompletionIndependence.lean 8 declarations
- SpatialCoordinateProjection.lean 9 declarations
- SpatialCreationVacuum.lean 5 declarations
- SpatialExpectationFaithful.lean 4 declarations
- SpatialExpectationKernel.lean 6 declarations
- SpatialFiniteCompression.lean 5 declarations
- SpatialFiniteFourier.lean 4 declarations
- SpatialFourierCoefficients.lean 4 declarations
- SpatialFourierConvergence.lean 2 declarations
- SpatialFreeGroupFaithful.lean 3 declarations
- SpatialFreeGroupRadial.lean 7 declarations
- SpatialFreeGroupShell.lean 6 declarations
- SpatialGroupConjugation.lean 5 declarations
- SpatialGroupFourier.lean 2 declarations
- SpatialGroupMatrixSlices.lean 2 declarations
- SpatialGroupPolynomialDensity.lean 4 declarations
- SpatialGroupPolynomialMap.lean 6 declarations
- SpatialHilbertBasisDensity.lean 6 declarations
- SpatialPartialNormBounds.lean 2 declarations
- SpatialPartialTranslations.lean 14 declarations
- SpatialPowersPolynomial.lean 5 declarations
- SpatialPowersSmallAverage.lean 6 declarations
- SpatialRadialTruncation.lean 5 declarations
- SpatialRepresentationComparison.lean 3 declarations
- SpatialRepresentationIndependence.lean 8 declarations
- SpatialSchurBounded.lean 2 declarations
- SpatialSchurNorm.lean 2 declarations
- SpatialSliceCompression.lean 1 declarations
- SpatialSliceNaturality.lean 3 declarations
- SpatialSubgroupPolynomial.lean 3 declarations
- SpatialSubgroupRestriction.lean 6 declarations
- SpatialSymbolMultiplier.lean 6 declarations
- SpatialSymbolPolynomial.lean 4 declarations
- SpatialTensorContinuousLegs.lean 5 declarations
- SpatialTensorFaithful.lean 2 declarations
- SpatialTensorFunctoriality.lean 3 declarations
- SpatialTensorIntertwining.lean 5 declarations
- SpatialTensorMaps.lean 7 declarations
- SpatialTensorNorm.lean 1 declarations
- SpatialTensorQuotient.lean 11 declarations
- SpatialTraceAgreement.lean 6 declarations
- SpatialUnitVectorSlice.lean 1 declarations
- SpatialVectorSlice.lean 9 declarations
- UniversalLeftTensorQuotient.lean 5 declarations