PaperFormalizer · Formalized papers
Formalized papers
Near Inclusions of von Neumann Algebras Without Small Spatial Embeddings
Lean code
A standalone Lake project: the paper's Lean, the toolkit modules it imports, and
Check.lean
.
Check.lean
Papers/OaiNearInclusionsVon/Basic.lean
Papers/OaiNearInclusionsVon/Helpers/Amplification.lean
Papers/OaiNearInclusionsVon/Helpers/AmplificationAlgebra.lean
Papers/OaiNearInclusionsVon/Helpers/AmplificationBicommutant.lean
Papers/OaiNearInclusionsVon/Helpers/CircleCoefficientSums.lean
Papers/OaiNearInclusionsVon/Helpers/CircleConstruction.lean
Papers/OaiNearInclusionsVon/Helpers/CircleLaurent.lean
Papers/OaiNearInclusionsVon/Helpers/CirclePathBounds.lean
Papers/OaiNearInclusionsVon/Helpers/CircleSummability.lean
Papers/OaiNearInclusionsVon/Helpers/Clock.lean
Papers/OaiNearInclusionsVon/Helpers/Corner.lean
Papers/OaiNearInclusionsVon/Helpers/CornerCommutation.lean
Papers/OaiNearInclusionsVon/Helpers/CornerFinalization.lean
Papers/OaiNearInclusionsVon/Helpers/CornerPolar.lean
Papers/OaiNearInclusionsVon/Helpers/CornerSpectral.lean
Papers/OaiNearInclusionsVon/Helpers/CornerTransport.lean
Papers/OaiNearInclusionsVon/Helpers/FreeGroupSpace.lean
Papers/OaiNearInclusionsVon/Helpers/Gap.lean
Papers/OaiNearInclusionsVon/Helpers/LaurentUnitary.lean
Papers/OaiNearInclusionsVon/Helpers/MainCornerModel.lean
Papers/OaiNearInclusionsVon/Helpers/MainFactorAlgebras.lean
Papers/OaiNearInclusionsVon/Helpers/MainJointLimits.lean
Papers/OaiNearInclusionsVon/Helpers/MainRepresentation.lean
Papers/OaiNearInclusionsVon/Helpers/MainSeparation.lean
Papers/OaiNearInclusionsVon/Helpers/MainSequence.lean
Papers/OaiNearInclusionsVon/Helpers/MainWeakCompact.lean
Papers/OaiNearInclusionsVon/Helpers/MatrixLimits.lean
Papers/OaiNearInclusionsVon/Helpers/NearBlocks.lean
Papers/OaiNearInclusionsVon/Helpers/NearConstruction.lean
Papers/OaiNearInclusionsVon/Helpers/NearExpansion.lean
Papers/OaiNearInclusionsVon/Helpers/NearReordering.lean
Papers/OaiNearInclusionsVon/Helpers/NearSummability.lean
Papers/OaiNearInclusionsVon/Helpers/SourceCarrier.lean
Papers/OaiNearInclusionsVon/Helpers/UnitarySpectrum.lean
Papers/OaiNearInclusionsVon/Helpers.lean
Papers/OaiNearInclusionsVon/ReusedTree/Basic.lean
Papers/OaiNearInclusionsVon/ReusedTree/Helpers/LpOperators.lean
Papers/OaiNearInclusionsVon/ReusedTree/Helpers/OperatorMaps.lean
Papers/OaiNearInclusionsVon/ReusedTree/Helpers/TreeGram.lean
Papers/OaiNearInclusionsVon/ReusedTree/Helpers/TreePathDiagonal.lean
Papers/OaiNearInclusionsVon/ReusedTree/Helpers/TreePathOperators.lean
Papers/OaiNearInclusionsVon/ReusedTree/Helpers/TreePerturbation.lean
Papers/OaiNearInclusionsVon/ReusedTree/Helpers/TreeUnitary.lean
Papers/OaiNearInclusionsVon/ReusedTree/Helpers/TreeVectors.lean
Papers/OaiNearInclusionsVon/Run.lean
Papers/OaiNearInclusionsVon/TCircle.lean
Papers/OaiNearInclusionsVon/TMain.lean
Papers/OaiNearInclusionsVon/TNear.lean
Papers/OaiNearInclusionsVon.lean
Papers.lean
README.md
Toolkit/Foundations/Analysis/Normed/CStarNormBounds.lean
Toolkit/Foundations/Analysis/Normed/FiniteDimensionalOperators.lean
Toolkit/Foundations/Analysis/Normed/WeakOperatorLimits.lean
Toolkit/Foundations/Analysis/SpecialFunctions/ComplexExpLevelSet.lean
Toolkit.lean
lakefile.toml
lean-toolchain