OAI/Analysis/ModularTheory/
565 declarations, 0 contain sorry, 0 declared as axioms; 88 files
Files
- AlgebraicAdjoint.lean 2 declarations
- AlgebraicNormalForm.lean 14 declarations
- AmplifiedModularAction.lean 5 declarations
- AmplifiedModularExpectation.lean 3 declarations
- CommutantExpectation.lean 3 declarations
- CompressedCorners.lean 8 declarations
- CoreDualAction.lean 8 declarations
- CoreIntegrals.lean 8 declarations
- CoreSeparation.lean 9 declarations
- CoreSquareWeight.lean 6 declarations
- CoreTracial.lean 6 declarations
- CornerGNS.lean 4 declarations
- CornerGNSActions.lean 2 declarations
- CornerGNSRange.lean 4 declarations
- CornerProductNorm.lean 2 declarations
- CornerRepresentation.lean 10 declarations
- CornerRepresentedBound.lean 2 declarations
- CornerRightVectors.lean 1 declarations
- CornerTensorBound.lean 6 declarations
- CornerVectors.lean 6 declarations
- CovariantKernel.lean 5 declarations
- CovariantSlices.lean 4 declarations
- CrossedProduct.lean 11 declarations
- CutoffTotality.lean 3 declarations
- DualAction.lean 9 declarations
- DualKernelPairing.lean 5 declarations
- DualRegularization.lean 9 declarations
- DualUnitary.lean 12 declarations
- FieldPairing.lean 3 declarations
- FiniteAdjoint.lean 9 declarations
- FiniteProjections.lean 12 declarations
- FiniteStates.lean 5 declarations
- FiniteTrace.lean 15 declarations
- FiniteWeightDensity.lean 4 declarations
- FiniteWeightSpace.lean 7 declarations
- FixedPointExpectation.lean 1 declarations
- FixedPointIdentification.lean 4 declarations
- FourierCompression.lean 13 declarations
- FourierOrbit.lean 3 declarations
- FourierTranslation.lean 4 declarations
- GaussianRegularizers.lean 10 declarations
- HalfGraphCutoff.lean 3 declarations
- KernelIdentification.lean 9 declarations
- KernelRegularization.lean 5 declarations
- LpFaithful.lean 7 declarations
- LpGauge.lean 13 declarations
- LpRepresentation.lean 4 declarations
- LpTranslation.lean 6 declarations
- NormalAdjoint.lean 8 declarations
- NormalAdjointMap.lean 6 declarations
- NormalAdjointWeight.lean 1 declarations
- NormalWeightTotality.lean 3 declarations
- OperatorTensorBound.lean 1 declarations
- OriginalNorm.lean 4 declarations
- OriginalRightAction.lean 4 declarations
- ProjectionExhaustion.lean 6 declarations
- RightContinuity.lean 5 declarations
- RightTranslation.lean 11 declarations
- ScalarCompression.lean 20 declarations
- SpectralFourier.lean 9 declarations
- SpectralGaussian.lean 11 declarations
- SpectralShift.lean 11 declarations
- StandardTensorBound.lean 5 declarations
- TomitaLp.lean 10 declarations
- TomitaOrbit.lean 8 declarations
- TomitaRegularizer.lean 8 declarations
- TomitaTime.lean 10 declarations
- TraceConjugation.lean 7 declarations
- TraceExplicitConjugation.lean 3 declarations
- TraceNormalConjugation.lean 2 declarations
- TracialCompression.lean 2 declarations
- TracialCorners.lean 7 declarations
- TracialRightAction.lean 11 declarations
- TranslationCalculus.lean 9 declarations
- TranslationWeight.lean 5 declarations
- WeightAdjointMap.lean 7 declarations
- WeightClosed.lean 1 declarations
- WeightCutoffs.lean 10 declarations
- WeightFaithful.lean 5 declarations
- WeightGNS.lean 8 declarations
- WeightGram.lean 8 declarations
- WeightMonomials.lean 11 declarations
- WeightMonotone.lean 2 declarations
- WeightRightMultiplier.lean 2 declarations
- WeightedDensity.lean 6 declarations
- WeightedFourierBound.lean 4 declarations
- WeightedFourierLimit.lean 6 declarations
- WeightedGaussianKernel.lean 4 declarations