OAI/RepresentationTheory/VertexAlgebra/
2412 declarations, 0 contain sorry, 0 declared as axioms; 143 files
Files
- AdjointMass.lean 34 declarations
- AlgebraCovariance.lean 7 declarations
- ApproximatingFlowDerivative.lean 25 declarations
- BicommutantFinite.lean 13 declarations
- BicommutantOrbit.lean 9 declarations
- BicommutantSelfAdjoint.lean 4 declarations
- BicommutantStrongNet.lean 3 declarations
- BlockGrowth.lean 28 declarations
- BoundedFlows.lean 47 declarations
- BoundedIntertwinerCore.lean 12 declarations
- BoundedIntertwinerFinite.lean 10 declarations
- BoundedIntertwinerNorm.lean 1 declarations
- BoundedIntertwinerNormal.lean 1 declarations
- BoundedIntertwinerRepresentation.lean 5 declarations
- BoundedMultiplierSingle.lean 53 declarations
- BoundedWOTDensity.lean 2 declarations
- CoefficientDifferentiated.lean 25 declarations
- CoefficientSummableBound.lean 33 declarations
- ColumnControl.lean 39 declarations
- ConformalNetContinuation.lean 2 declarations
- ConstrainedSquareBound.lean 30 declarations
- CovarianceContinuation.lean 8 declarations
- CreationBoundaryDerivative.lean 7 declarations
- CreationBoundaryTaylor.lean 7 declarations
- CreationBoundaryUniqueness.lean 2 declarations
- CreationDistribution.lean 6 declarations
- CreationZeroExtension.lean 4 declarations
- CutoffPowerControl.lean 22 declarations
- DiffeomorphismContinuity.lean 3 declarations
- DiffeomorphismStressSmooth.lean 32 declarations
- EnergyCutoff.lean 29 declarations
- EnergyCutoffNorm.lean 50 declarations
- EnergyShiftPow.lean 27 declarations
- FiniteSums.lean 33 declarations
- FixedArc.lean 4 declarations
- Foundations.lean 5 imports, no declarations
- GeneratedIntertwinerAction.lean 5 declarations
- GeneratedNormalUniqueness.lean 1 declarations
- GeneratorSharpGrowth.lean 17 declarations
- GeometryContinuation.lean 9 declarations
- GradeComponentC.lean 50 declarations
- GraphCommutants.lean 45 declarations
- GraphCovariance.lean 3 declarations
- GraphEquiv.lean 38 declarations
- GraphInvariantOf.lean 51 declarations
- HighFieldGraph.lean 18 declarations
- HilbertCore.lean 59 declarations
- HilbertRegularization.lean 31 declarations
- InverseEnergySelf.lean 30 declarations
- LocalImplementer.lean 6 declarations
- LocalNormalMap.lean 28 declarations
- LocalNormalSeries.lean 23 declarations
- Locality.lean 48 declarations
- LoweringNormSq.lean 19 declarations
- Main.lean 3 imports, no declarations
- MainClauseOne.lean 1 declarations
- MinimalComparator.lean 62 declarations
- MobiusAnomaly.lean 10 declarations
- MobiusContinuity.lean 5 declarations
- MobiusExistence.lean 13 declarations
- MobiusFullGeometry.lean 8 declarations
- MobiusGeometry.lean 13 declarations
- MobiusGroup.lean 14 declarations
- MobiusRepresentation.lean 20 declarations
- MobiusStandardAction.lean 10 declarations
- MobiusStandardTopology.lean 18 declarations
- MobiusVacuum.lean 6 declarations
- ModuleAdjointDescent.lean 4 declarations
- ModuleAdjoints.lean 5 declarations
- ModuleBands.lean 11 declarations
- ModuleBlockControl.lean 8 declarations
- ModuleBlockGrowth.lean 11 declarations
- ModuleBlockSquareBound.lean 2 declarations
- ModuleBootstrap.lean 4 declarations
- ModuleColumnOperators.lean 16 declarations
- ModuleCommutatorBounds.lean 6 declarations
- ModuleCreationEstimates.lean 4 declarations
- ModuleCreationModel.lean 6 declarations
- ModuleCreationRangeReduction.lean 3 declarations
- ModuleCreationTotality.lean 6 declarations
- ModuleCreationVacuum.lean 6 declarations
- ModuleCurrentEnergy.lean 1 declarations
- ModuleCutoffs.lean 18 declarations
- ModuleEnergyMain.lean 5 declarations
- ModuleEnergyModel.lean 12 declarations
- ModuleGeneratorMajorant.lean 4 declarations
- ModuleGrading.lean 16 declarations
- ModuleGraphIntertwiners.lean 19 declarations
- ModuleIntegrationTarget.lean 4 declarations
- ModuleIntegrationUniqueness.lean 2 declarations
- ModuleMobiusAlgebra.lean 3 declarations
- ModuleMobiusEstimates.lean 11 declarations
- ModuleMobiusTransfer.lean 10 declarations
- ModuleModeAlgebra.lean 6 declarations
- ModuleOptimalCutoff.lean 1 declarations
- ModuleOptimalEnergy.lean 2 declarations
- ModulePositiveColumn.lean 3 declarations
- ModulePositiveEnergy.lean 5 declarations
- ModuleRoughEnergy.lean 3 declarations
- ModuleSharpBounded.lean 2 declarations
- ModuleSharpBounds.lean 4 declarations
- ModuleSharpContraction.lean 8 declarations
- ModuleSharpGrowth.lean 30 declarations
- ModuleSharpMajorant.lean 19 declarations
- ModuleSharpNormalProducts.lean 19 declarations
- ModuleSharpPolynomial.lean 8 declarations
- ModuleSl2Bound.lean 1 declarations
- ModuleSmearedFields.lean 12 declarations
- ModuleSpectralNorms.lean 10 declarations
- ModuleZeroSharp.lean 6 declarations
- MulLeftPow.lean 46 declarations
- NetAxioms.lean 8 declarations
- NetVacuum.lean 4 declarations
- NormalUniqueness.lean 4 declarations
- ObservableScalars.lean 37 declarations
- PrimaryStressWeak.lean 30 declarations
- ProjectiveTopology.lean 6 declarations
- PropagatorContinuation.lean 2 declarations
- RegularizerFactorAdd.lean 32 declarations
- ResolventSubalgebra.lean 3 declarations
- RotationConjugateCommutant.lean 73 declarations
- RotationImplementer.lean 4 declarations
- SelfAdjointHomExt.lean 2 declarations
- SelfAdjointResolvent.lean 4 declarations
- SmoothConjugateInner.lean 28 declarations
- SmoothConjugatePrimary.lean 26 declarations
- SmoothEnergyPower.lean 43 declarations
- SmoothSmearShift.lean 21 declarations
- SmoothTopology.lean 24 declarations
- SourceModuleEnergy.lean 1 declarations
- SourceStrongRationality.lean 4 declarations
- StressCutoffNormalized.lean 41 declarations
- StressCutoffNormalized2.lean 36 declarations
- StressEvolution.lean 28 declarations
- StressPropagatorDerivative.lean 57 declarations
- StressPropagatorPath.lean 2 declarations
- StressSmoothness.lean 56 declarations
- StrongContinuity.lean 3 declarations
- SummableNormSobolev.lean 31 declarations
- SymmetricWeakCommute.lean 41 declarations
- TimeAverageGraph.lean 31 declarations
- VacuumMemNegative.lean 50 declarations
- VirasoroLinearEnergy.lean 20 declarations