PaperFormalizer · Formalized papers
Formalized papers
An \(L^3\) bound for the dyadic triangular Hilbert form
Lean code
A standalone Lake project: the paper's Lean, the toolkit modules it imports, and
Check.lean
.
Check.lean
Papers/OaiBoundDyadicTriangular/All.lean
Papers/OaiBoundDyadicTriangular/Basic.lean
Papers/OaiBoundDyadicTriangular/Helpers/AtomCompact.lean
Papers/OaiBoundDyadicTriangular/Helpers/AtomEnergy.lean
Papers/OaiBoundDyadicTriangular/Helpers/AtomIntegral.lean
Papers/OaiBoundDyadicTriangular/Helpers/AtomMass.lean
Papers/OaiBoundDyadicTriangular/Helpers/AtomReindex.lean
Papers/OaiBoundDyadicTriangular/Helpers/AtomTrace.lean
Papers/OaiBoundDyadicTriangular/Helpers/ChildMatrices.lean
Papers/OaiBoundDyadicTriangular/Helpers/Continuity.lean
Papers/OaiBoundDyadicTriangular/Helpers/DyadicApproximation.lean
Papers/OaiBoundDyadicTriangular/Helpers/DyadicChildren.lean
Papers/OaiBoundDyadicTriangular/Helpers/GapPath.lean
Papers/OaiBoundDyadicTriangular/Helpers/HessianTransport.lean
Papers/OaiBoundDyadicTriangular/Helpers/LocalHolder.lean
Papers/OaiBoundDyadicTriangular/Helpers/LocalProduct.lean
Papers/OaiBoundDyadicTriangular/Helpers/MatrixHessian.lean
Papers/OaiBoundDyadicTriangular/Helpers/MatrixSylvester.lean
Papers/OaiBoundDyadicTriangular/Helpers/ScaleHolder.lean
Papers/OaiBoundDyadicTriangular/Helpers/StepSummation.lean
Papers/OaiBoundDyadicTriangular/Helpers/Summation.lean
Papers/OaiBoundDyadicTriangular/Helpers/SupportedCalculus.lean
Papers/OaiBoundDyadicTriangular/Helpers/SupportedDerivatives.lean
Papers/OaiBoundDyadicTriangular/Helpers/SylvesterOrder.lean
Papers/OaiBoundDyadicTriangular/Helpers/TraceBlocks.lean
Papers/OaiBoundDyadicTriangular/Helpers/TraceCoordinates.lean
Papers/OaiBoundDyadicTriangular/Helpers/TraceEmbeddings.lean
Papers/OaiBoundDyadicTriangular/Helpers/TraceSpectral.lean
Papers/OaiBoundDyadicTriangular/Helpers.lean
Papers/OaiBoundDyadicTriangular/TGap.lean
Papers/OaiBoundDyadicTriangular/TIncrease.lean
Papers/OaiBoundDyadicTriangular/TMain.lean
Papers/OaiBoundDyadicTriangular/TTrace.lean
Papers/OaiBoundDyadicTriangular.lean
Papers.lean
README.md
lakefile.toml
lean-toolchain