Frozen Lean source
222 source modules, copied byte for byte from the verified project. Select a file to read its complete imports, namespace, declarations and proofs.
Download source and dependency pins · Verification record
- BanLat/Basic.lean
- BanLat/Disjoint.lean
- BanLat/Dual.lean
- BanLat/LLexpr.lean
- BanLat/Normed.lean
- BanLat/Operators/Hom.lean
- BanLat/Operators/OrderBounded.lean
- BanLat/Operators/Positive.lean
- BanLat/Operators/Regular.lean
- BanLat/Operators/RieszKantorovich.lean
- BanLat/OrderComplete.lean
- BanLat/OrderUnit.lean
- BanLat/RieszDec.lean
- BanLat/Substructures/Band/Basic.lean
- BanLat/Substructures/Band/DisjointComplement.lean
- BanLat/Substructures/Band/Generated.lean
- BanLat/Substructures/Band/Lattice.lean
- BanLat/Substructures/Band/PPP.lean
- BanLat/Substructures/Band/Projection.lean
- BanLat/Substructures/Ideal.lean
- BanLat/Substructures/Sublattice.lean
- PL1/ALAlternative.lean
- PL1/ALAtomic.lean
- PL1/ALDyadicEmbedding.lean
- PL1/ALFragments.lean
- PL1/ALOrder.lean
- PL1/ALRenorming.lean
- PL1/AtomicBandDecomposition.lean
- PL1/BalancedFragmentTree.lean
- PL1/BochnerResolvents.lean
- PL1/BonamiHaarBridge.lean
- PL1/BonamiTensorization.lean
- PL1/BonamiTwoPoint.lean
- PL1/CarrierAsymptotics.lean
- PL1/CompactRestriction.lean
- PL1/CompactWalshMultiplier.lean
- PL1/ComplementedLatticeBandEstimates.lean
- PL1/ComplementedLatticeRealAmbient.lean
- PL1/ComplementedLatticeRealTrace.lean
- PL1/ComplementedLatticeReduction.lean
- PL1/ComplementedLatticeSumming.lean
- PL1/ConcreteResolvents.lean
- PL1/ConstantNoiseTrace.lean
- PL1/ConstantTailSpikes.lean
- PL1/ConvolutionHypercontractivity.lean
- PL1/ConvolutionL1.lean
- PL1/DaugavetAveraging.lean
- PL1/DaugavetCriterion.lean
- PL1/DaugavetDiameter.lean
- PL1/DaugavetIntrinsicFramework.lean
- PL1/DaugavetRealification.lean
- PL1/DecompositionRNP.lean
- PL1/Definitions.lean
- PL1/DiscreteInterpolation.lean
- PL1/DisjointNormingFunctionals.lean
- PL1/DunfordPettis.lean
- PL1/DyadicCellMeasure.lean
- PL1/DyadicCoordinateDomination.lean
- PL1/DyadicInterpolationIntegral.lean
- PL1/DyadicInterpolationNormComparison.lean
- PL1/DyadicL1Coordinates.lean
- PL1/DyadicProjection.lean
- PL1/DyadicSchur.lean
- PL1/DyadicTrace.lean
- PL1/EigenvectorEmbedding.lean
- PL1/Ell1RNP.lean
- PL1/Ell2Schur.lean
- PL1/EnfloBush.lean
- PL1/EnfloCopyExclusion.lean
- PL1/EnfloDyadicDecay.lean
- PL1/EnfloHypercontractive.lean
- PL1/EnfloIntrinsic.lean
- PL1/EnfloMajorant.lean
- PL1/EnfloMaxMass.lean
- PL1/EnfloNoL1.lean
- PL1/EnfloSmoothing.lean
- PL1/EnfloStarbirdDyadic.lean
- PL1/EnfloStarbirdProjection.lean
- PL1/EnfloSum.lean
- PL1/EnfloTruncation.lean
- PL1/EnfloTwoMaps.lean
- PL1/EnfloVanishing.lean
- PL1/ExplicitMartingale.lean
- PL1/ExplicitMartingaleFiltration.lean
- PL1/ExplicitMartingaleWeak.lean
- PL1/ExponentialTail.lean
- PL1/ExponentialTime.lean
- PL1/ExtendedDiscreteInterpolation.lean
- PL1/FiniteCoordinateKernels.lean
- PL1/FiniteDimensionalRNP.lean
- PL1/FiniteDualDisjointization.lean
- PL1/FiniteGrothendieck.lean
- PL1/FiniteGrothendieckNormalization.lean
- PL1/FiniteRademacherClipping.lean
- PL1/FiniteSummingFromMatrix.lean
- PL1/GeneratorGraphBanach.lean
- PL1/HeadTail.lean
- PL1/HeadTailNoise.lean
- PL1/HeadTailNorms.lean
- PL1/HilbertDyadicTrace.lean
- PL1/HilbertTraceBounds.lean
- PL1/InputCompression.lean
- PL1/InterpolationBochner.lean
- PL1/InterpolationNorm.lean
- PL1/IntervalDyadicApproximation.lean
- PL1/IntervalEll1Obstruction.lean
- PL1/IntervalModel.lean
- PL1/IntervalRetraction.lean
- PL1/IntervalSubtype.lean
- PL1/IntervalSumming.lean
- PL1/IntervalWalsh.lean
- PL1/IntrinsicApproximations.lean
- PL1/IntrinsicExposedPoint.lean
- PL1/IntrinsicGraph.lean
- PL1/IntrinsicHeadRepresentatives.lean
- PL1/IntrinsicNonBoundedComplete.lean
- PL1/IntrinsicRealParts.lean
- PL1/IntrinsicSpikeAverages.lean
- PL1/IntrinsicSpikeEstimates.lean
- PL1/IntrinsicSpikeFamilies.lean
- PL1/IntrinsicSpikes.lean
- PL1/IntrinsicTailNorm.lean
- PL1/IntrinsicWalsh.lean
- PL1/IntrinsicWalshBlocks.lean
- PL1/KernelL1.lean
- PL1/KernelTranslations.lean
- PL1/KFunctional.lean
- PL1/KFunctionalIntegral.lean
- PL1/KFunctionalIntegralMeasurable.lean
- PL1/KFunctionalNormLaws.lean
- PL1/KFunctionalProperties.lean
- PL1/L1Masks.lean
- PL1/L1Multiplication.lean
- PL1/L1Sum.lean
- PL1/L1Truncation.lean
- PL1/L1UniformIntegrability.lean
- PL1/LatticeAbsoluteContinuity.lean
- PL1/LatticeAtoms.lean
- PL1/LatticeBridge.lean
- PL1/LatticeDefinitions.lean
- PL1/LatticeDisjointCountability.lean
- PL1/LatticeFragments.lean
- PL1/LatticeRademacher.lean
- PL1/LatticeRademacherWeak.lean
- PL1/LatticeReduction.lean
- PL1/LatticeRenorming.lean
- PL1/LatticeStrictPositive.lean
- PL1/LpInclusions.lean
- PL1/LpInterpolation.lean
- PL1/LpOperatorLift.lean
- PL1/MainDaugavet.lean
- PL1/MainInterpolation.lean
- PL1/MainTheoremA.lean
- PL1/MainTheoremB.lean
- PL1/MatrixSmoothing.lean
- PL1/MatrixTrace.lean
- PL1/MatrixTraceLimit.lean
- PL1/MetricApproximation.lean
- PL1/NoiseGenerator.lean
- PL1/NoiseGeneratorCore.lean
- PL1/NoiseHypercontractivity.lean
- PL1/NoiseMeasures.lean
- PL1/NoiseSemigroup.lean
- PL1/NoiseTraceObstruction.lean
- PL1/NonSchurExample.lean
- PL1/OperatorDomination.lean
- PL1/OutputCompression.lean
- PL1/PartialMainTheorems.lean
- PL1/PartitionAverages.lean
- PL1/PositiveLowerOneBridge.lean
- PL1/PrincipalIdealDual.lean
- PL1/ProjectionRetract.lean
- PL1/ProjectionTransport.lean
- PL1/ProofReview.lean
- PL1/RademacherEmbedding.lean
- PL1/RealSchur.lean
- PL1/ResolventAlmostInvariant.lean
- PL1/ResolventEstimates.lean
- PL1/ResolventGeneratorGraph.lean
- PL1/ResolventMultiplication.lean
- PL1/ResolventNorms.lean
- PL1/Review.lean
- PL1/RNPBridge.lean
- PL1/RNPTransport.lean
- PL1/ScalarDecompositionRNP.lean
- PL1/ScalarRealification.lean
- PL1/ScalarUnconditionalRNP.lean
- PL1/SchurApproximation.lean
- PL1/SchurBoundedCompleteness.lean
- PL1/SchurExample.lean
- PL1/SchurLattice.lean
- PL1/SchurLatticeAtomicity.lean
- PL1/SchurLatticeCompactness.lean
- PL1/SecondProofReview.lean
- PL1/SeparableRange.lean
- PL1/SingularCarrier.lean
- PL1/SingularConvolution.lean
- PL1/SingularResolvents.lean
- PL1/SmoothingApproximation.lean
- PL1/SmoothingTrace.lean
- PL1/SpikeSeparation.lean
- PL1/Statements.lean
- PL1/StrongConvergence.lean
- PL1/SummingTransport.lean
- PL1/TailSpikeEvents.lean
- PL1/TailSpikeMultiplication.lean
- PL1/TailSpikes.lean
- PL1/ThirdProofReview.lean
- PL1/TraceBounds.lean
- PL1/TraceDomination.lean
- PL1/TraceVanishing.lean
- PL1/TruncatedResolventFactorization.lean
- PL1/UnconditionalDecomposition.lean
- PL1/UnconditionalRNP.lean
- PL1/VectorDensityBounds.lean
- PL1/WalshBlocks.lean
- PL1/WalshExpectations.lean
- PL1/WalshModel.lean
- PL1/WeakSchur.lean
- PL1/WeakSequentialCompleteness.lean
- PL1/WeightedL1.lean
- PL1.lean