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
ComplementedSubspace.lean
ComplementedSubspace/ActualProjectionBidualDPR.lean
ComplementedSubspace/ActualProjectionDPR.lean
ComplementedSubspace/ActualProjectionDualDPR.lean
ComplementedSubspace/Ambient.lean
ComplementedSubspace/AmbientBasis.lean
ComplementedSubspace/AmbientFiniteApproximation.lean
ComplementedSubspace/AmbientLattice.lean
ComplementedSubspace/AmbientProjection.lean
ComplementedSubspace/AmbientSchauder.lean
ComplementedSubspace/AmbientSeparable.lean
ComplementedSubspace/AmbientUniformConvex.lean
ComplementedSubspace/BasisBounds.lean
ComplementedSubspace/BasisRestriction.lean
ComplementedSubspace/BasisTransport.lean
ComplementedSubspace/ComplexAmbient.lean
ComplementedSubspace/ComplexAmbientSchauder.lean
ComplementedSubspace/ComplexCorollary.lean
ComplementedSubspace/ComplexCorollaryAssembly.lean
ComplementedSubspace/ComplexFrameCoefficient.lean
ComplementedSubspace/ComplexFrameCoefficientRange.lean
ComplementedSubspace/ComplexFrameProjection.lean
ComplementedSubspace/ComplexFrameRealification.lean
ComplementedSubspace/ComplexProjectionEnergy.lean
ComplementedSubspace/ComplexProjectionRealEquiv.lean
ComplementedSubspace/ComplexRealDPR.lean
ComplementedSubspace/ComplexRecursiveProjection.lean
ComplementedSubspace/ComplexReindexedFrameProjection.lean
ComplementedSubspace/ComplexTensorProjection.lean
ComplementedSubspace/CorollaryStatement.lean
ComplementedSubspace/DenseContractions.lean
ComplementedSubspace/DenseContractionsScalar.lean
ComplementedSubspace/DiagonalFrameProduct.lean
ComplementedSubspace/DiagonalFrameSummand.lean
ComplementedSubspace/DPRIsomorphism.lean
ComplementedSubspace/DPRObstruction.lean
ComplementedSubspace/DPRPredicates.lean
ComplementedSubspace/DPRtoGL.lean
ComplementedSubspace/FiniteApproximation.lean
ComplementedSubspace/FiniteBasisTraceBound.lean
ComplementedSubspace/FiniteBidual.lean
ComplementedSubspace/FiniteBidualDPRLower.lean
ComplementedSubspace/FiniteBlockDPRLower.lean
ComplementedSubspace/FiniteBlockObstruction.lean
ComplementedSubspace/FiniteCoordinateSelection.lean
ComplementedSubspace/FiniteCorrection.lean
ComplementedSubspace/FiniteCubeBound.lean
ComplementedSubspace/FiniteDualBasis.lean
ComplementedSubspace/FiniteDualDPRLower.lean
ComplementedSubspace/FiniteDualSuperspace.lean
ComplementedSubspace/FiniteFrame.lean
ComplementedSubspace/FiniteHeadHilbert.lean
ComplementedSubspace/FiniteHilbertAverage.lean
ComplementedSubspace/FiniteLpGeometry.lean
ComplementedSubspace/FiniteOverlapBasisColumns.lean
ComplementedSubspace/FiniteOverlapBound.lean
ComplementedSubspace/FiniteOverlapConclusion.lean
ComplementedSubspace/FiniteOverlapDualScale.lean
ComplementedSubspace/FiniteOverlapGoodSecond.lean
ComplementedSubspace/FiniteOverlapLp.lean
ComplementedSubspace/FiniteOverlapMatrixNorms.lean
ComplementedSubspace/FiniteOverlapMoments.lean
ComplementedSubspace/FiniteOverlapObstruction.lean
ComplementedSubspace/FiniteOverlapRandomization.lean
ComplementedSubspace/FiniteOverlapScale.lean
ComplementedSubspace/FiniteOverlapUpper.lean
ComplementedSubspace/FiniteParameterBounds.lean
ComplementedSubspace/FiniteParameterGap.lean
ComplementedSubspace/FiniteProductObstruction.lean
ComplementedSubspace/FiniteProjectionTrace.lean
ComplementedSubspace/FiniteSelectedHilbertModel.lean
ComplementedSubspace/FiniteSelectionCoordinates.lean
ComplementedSubspace/FiniteSigns.lean
ComplementedSubspace/FiniteSignsComplex.lean
ComplementedSubspace/FiniteSignsInterpolation.lean
ComplementedSubspace/FiniteSuperspaceSplitting.lean
ComplementedSubspace/FiniteTraceOverlap.lean
ComplementedSubspace/FiniteTraceSelection.lean
ComplementedSubspace/FrameCoefficient.lean
ComplementedSubspace/FrameCoefficientHilbert.lean
ComplementedSubspace/FrameCoefficientNorm.lean
ComplementedSubspace/FrameCoefficientRange.lean
ComplementedSubspace/FrameCoefficientReindexedRange.lean
ComplementedSubspace/FrameProjectionNorm.lean
ComplementedSubspace/FrameProjectionRange.lean
ComplementedSubspace/GLDualRetraction.lean
ComplementedSubspace/GLRetraction.lean
ComplementedSubspace/HilbertComplement.lean
ComplementedSubspace/HilbertOverlap.lean
ComplementedSubspace/HilbertTraceTransfer.lean
ComplementedSubspace/InfiniteFrameObstruction.lean
ComplementedSubspace/IsometricProductDPRLower.lean
ComplementedSubspace/IsometricProductSplitting.lean
ComplementedSubspace/LatticeApproximation.lean
ComplementedSubspace/LatticeBasis.lean
ComplementedSubspace/LatticeNonisomorphism.lean
ComplementedSubspace/LatticeSpectral.lean
ComplementedSubspace/LocalHilbert.lean
ComplementedSubspace/LocalHilbertCompactness.lean
ComplementedSubspace/LocalHilbertCoordinates.lean
ComplementedSubspace/LocalHilbertDual.lean
ComplementedSubspace/LocalHilbertDualTop.lean
ComplementedSubspace/LocalHilbertEmbeddedRenorm.lean
ComplementedSubspace/LocalHilbertFactorization.lean
ComplementedSubspace/LocalHilbertHeadRenorm.lean
ComplementedSubspace/LocalHilbertProjection.lean
ComplementedSubspace/LocalHilbertProperty.lean
ComplementedSubspace/LocalHilbertQuotient.lean
ComplementedSubspace/LocalHilbertRecursiveKernelDual.lean
ComplementedSubspace/LocalHilbertSum.lean
ComplementedSubspace/LocalHilbertSumDual.lean
ComplementedSubspace/LocalHilbertTransport.lean
ComplementedSubspace/LocalUnconditional.lean
ComplementedSubspace/LpHeadTail.lean
ComplementedSubspace/LpSubmodule.lean
ComplementedSubspace/LpSubmoduleScalar.lean
ComplementedSubspace/LpTwoParallelogram.lean
ComplementedSubspace/LpTwoUniformConvex.lean
ComplementedSubspace/LpUniformEquiv.lean
ComplementedSubspace/NormalizedHilbertSynthesis.lean
ComplementedSubspace/NormSqSplitting.lean
ComplementedSubspace/Parameters.lean
ComplementedSubspace/ProductFrame.lean
ComplementedSubspace/ProductFrameIndex.lean
ComplementedSubspace/ProductFrameLp.lean
ComplementedSubspace/ProductFrameMoments.lean
ComplementedSubspace/ProductFrameRowWitness.lean
ComplementedSubspace/ProductFrameSignContraction.lean
ComplementedSubspace/ProductFrameSignSample.lean
ComplementedSubspace/ProductFrameSymmetry.lean
ComplementedSubspace/ProductFrameTrace.lean
ComplementedSubspace/ProductFrameTraceBound.lean
ComplementedSubspace/ProductFrameWitness.lean
ComplementedSubspace/ProjectionCorollaries.lean
ComplementedSubspace/ProjectionOverlapLower.lean
ComplementedSubspace/ProjectionPerturbation.lean
ComplementedSubspace/PureFrameDPR.lean
ComplementedSubspace/RealMainConsequences.lean
ComplementedSubspace/RealMainTheorem.lean
ComplementedSubspace/RecursiveDiagonalBidualDPR.lean
ComplementedSubspace/RecursiveDiagonalDPR.lean
ComplementedSubspace/RecursiveDiagonalDualDPR.lean
ComplementedSubspace/RecursiveHeadHilbert.lean
ComplementedSubspace/RecursiveKernelHilbert.lean
ComplementedSubspace/RecursiveParameters.lean
ComplementedSubspace/RecursiveProjection.lean
ComplementedSubspace/RecursiveTailHilbert.lean
ComplementedSubspace/ReindexedFrameProjection.lean
ComplementedSubspace/SchauderDPR.lean
ComplementedSubspace/SelectedCoefficientHilbert.lean
ComplementedSubspace/SelectedHilbertReplacement.lean
ComplementedSubspace/SelectedProjectionSetup.lean
ComplementedSubspace/TensorMoment.lean
ComplementedSubspace/TensorProjection.lean
ComplementedSubspace/TheoremStatement.lean
ComplementedSubspace/UnconditionalHilbertSynthesis.lean
