PaperFormalizer · Formalized papers

Lean code

A standalone Lake project: the paper's Lean, the toolkit modules it imports, and Check.lean.

Check.lean
Papers/OaiLinearVarianceRandom/All.lean
Papers/OaiLinearVarianceRandom/Basic.lean
Papers/OaiLinearVarianceRandom/Helpers/AssignmentSets.lean
Papers/OaiLinearVarianceRandom/Helpers/ClauseCounting.lean
Papers/OaiLinearVarianceRandom/Helpers/DelayTools.lean
Papers/OaiLinearVarianceRandom/Helpers/DelayTowers.lean
Papers/OaiLinearVarianceRandom/Helpers/HiddenClauses.lean
Papers/OaiLinearVarianceRandom/Helpers/HittingMoments.lean
Papers/OaiLinearVarianceRandom/Helpers/HittingTail.lean
Papers/OaiLinearVarianceRandom/Helpers/MomentLaws.lean
Papers/OaiLinearVarianceRandom/Helpers/Moments.lean
Papers/OaiLinearVarianceRandom/Helpers/OccupationMeasure.lean
Papers/OaiLinearVarianceRandom/Helpers/OccupationPaths.lean
Papers/OaiLinearVarianceRandom/Helpers/Omission.lean
Papers/OaiLinearVarianceRandom/Helpers/OrdinaryClauses.lean
Papers/OaiLinearVarianceRandom/Helpers/OrdinaryDrift.lean
Papers/OaiLinearVarianceRandom/Helpers/OrdinaryHiddenClauses.lean
Papers/OaiLinearVarianceRandom/Helpers/PivotalVector.lean
Papers/OaiLinearVarianceRandom/Helpers/Pivotality.lean
Papers/OaiLinearVarianceRandom/Helpers/Potential.lean
Papers/OaiLinearVarianceRandom/Helpers/RefinedHiddenClauses.lean
Papers/OaiLinearVarianceRandom/Helpers/RootExposure.lean
Papers/OaiLinearVarianceRandom/Helpers/TestClauses.lean
Papers/OaiLinearVarianceRandom/Helpers/TestFamilyBounds.lean
Papers/OaiLinearVarianceRandom/Helpers/TestFamilyConditioning.lean
Papers/OaiLinearVarianceRandom/Helpers/TestNecessity.lean
Papers/OaiLinearVarianceRandom/Helpers/UpperVariance.lean
Papers/OaiLinearVarianceRandom/Helpers.lean
Papers/OaiLinearVarianceRandom/TDelay.lean
Papers/OaiLinearVarianceRandom/TDuration.lean
Papers/OaiLinearVarianceRandom/TMain.lean
Papers/OaiLinearVarianceRandom/TWindow.lean
Papers/OaiLinearVarianceRandom.lean
Papers.lean
README.md
Toolkit/Foundations/Probability/Processes/DriftRecursion.lean
Toolkit.lean
built-against.json
lakefile.toml
lean-toolchain