OAI/Analysis/Cotype/
911 declarations, 0 contain sorry, 0 declared as axioms; 125 files
Files
- APNontrivialType.lean 2 declarations
- Approximation.lean 2 declarations
- BConvexBlocking.lean 4 declarations
- BConvexQuantitative.lean 4 declarations
- BConvexity.lean 6 declarations
- BiasedFourier.lean 12 declarations
- BinaryCoordinates.lean 14 declarations
- BinaryRank.lean 6 declarations
- BivariateSplit.lean 21 declarations
- ChebyshevBounds.lean 11 declarations
- ChebyshevTruncation.lean 4 declarations
- CoefficientArithmetic.lean 1 declarations
- CoefficientBounds.lean 3 declarations
- CoefficientCompactness.lean 10 declarations
- CoefficientPowerGap.lean 1 declarations
- CoefficientTarget.lean 4 declarations
- CompactDomain.lean 4 declarations
- CompactDomainSource.lean 3 declarations
- CompactMomentAssembly.lean 2 declarations
- CompactQuotient.lean 11 declarations
- ComplexDualLift.lean 21 declarations
- ComplexPowerGapInverse.lean 1 declarations
- ComplexProjectionPolynomial.lean 10 declarations
- ComplexProjectionSpectrum.lean 9 declarations
- CotypeAmplification.lean 2 declarations
- Cube.lean 12 declarations
- CubeCoordinateProjections.lean 11 declarations
- CubeFirstChaos.lean 6 declarations
- CubeNoise.lean 11 declarations
- DampedPolynomial.lean 10 declarations
- Damping.lean 17 declarations
- DeletedTail.lean 8 declarations
- DualAction.lean 4 declarations
- DualCotypeFromLifts.lean 1 declarations
- DualMomentLifts.lean 10 declarations
- EquivariantLifts.lean 8 declarations
- EquivariantPairing.lean 12 declarations
- ExponentialIntegral.lean 4 declarations
- FiniteContour.lean 28 declarations
- FiniteCotypeBounds.lean 3 declarations
- FiniteL2Dual.lean 10 declarations
- FiniteL2DualNorm.lean 3 declarations
- FiniteLevelLift.lean 2 declarations
- FiniteLevelTower.lean 2 declarations
- FiniteRankWalsh.lean 7 declarations
- FiniteSupDual.lean 6 declarations
- FixedTypeImprovement.lean 5 declarations
- Fourier.lean 15 declarations
- FrameFeasibility.lean 3 declarations
- FrameLifts.lean 7 declarations
- FrameOrbit.lean 4 declarations
- GeometricTypeLevels.lean 5 declarations
- GroupedPolynomial.lean 5 declarations
- GrowthCoefficient.lean 6 declarations
- GrowthScalarData.lean 9 declarations
- GrowthTheorem.lean 1 declarations
- GrowthTuplePairing.lean 11 declarations
- IdentityWalshDecay.lean 2 declarations
- IndependentSigns.lean 7 declarations
- KConvexCoordinateCriterion.lean 1 declarations
- KConvexDuality.lean 6 declarations
- KConvexUniformL1.lean 5 declarations
- L2MomentLifts.lean 9 declarations
- L2Sequence.lean 5 declarations
- Main.lean 3 declarations
- MainConstruction.lean 2 declarations
- MixedDerivative.lean 11 declarations
- Model.lean 12 declarations
- Moments.lean 10 declarations
- NoiseHypercontractivity.lean 4 declarations
- OddPatternBounds.lean 9 declarations
- PairedExtension.lean 4 declarations
- ParameterChoice.lean 5 declarations
- PatternNormalization.lean 16 declarations
- PatternPairing.lean 12 declarations
- PatternProjections.lean 9 declarations
- PowerGapInverse.lean 2 declarations
- PowerGapScaling.lean 2 declarations
- PrimalMomentLifts.lean 14 declarations
- ProjectionAverages.lean 5 declarations
- ProjectionCoefficientDerivative.lean 2 declarations
- ProjectionCoefficients.lean 26 declarations
- ProjectionDeficit.lean 5 declarations
- ProjectionDerivatives.lean 15 declarations
- ProjectionEigenvectors.lean 3 declarations
- ProjectionGenerator.lean 8 declarations
- ProjectionL2Gap.lean 3 declarations
- ProjectionProducts.lean 10 declarations
- ProjectionResolvent.lean 5 declarations
- ProjectionSemigroup.lean 10 declarations
- ProjectionSemigroupBasics.lean 7 declarations
- ProjectionSpectrum.lean 7 declarations
- QuadraticTypeTensor.lean 10 declarations
- QuotientLifts.lean 2 declarations
- RademacherComparison.lean 4 declarations
- RankFactors.lean 3 declarations
- RankWalsh.lean 6 declarations
- Rectangles.lean 7 declarations
- ScalarWalsh.lean 8 declarations
- SectorResolvent.lean 5 declarations
- SlowDrop.lean 3 declarations
- TaggedCoefficient.lean 8 declarations
- TaggedFrames.lean 9 declarations
- Target.lean 2 declarations
- TimedShiftScalars.lean 7 declarations
- TypeCotypeDuality.lean 8 declarations
- TypeExtrapolation.lean 6 declarations
- TypeExtrapolationParameters.lean 3 declarations
- TypeL2Amplification.lean 3 declarations
- TypeUniformL1.lean 3 declarations
- UniformDecay.lean 4 declarations
- UniformL1.lean 7 declarations
- VectorWalsh.lean 19 declarations
- VerticalTimeCoefficient.lean 3 declarations
- WalshAmplification.lean 11 declarations
- WalshCoordinates.lean 10 declarations
- WalshDuality.lean 13 declarations
- WalshExactPairing.lean 14 declarations
- WalshFrameOrbit.lean 5 declarations
- WalshLower.lean 5 declarations
- WalshMainEstimates.lean 7 declarations
- WalshMonotonicity.lean 4 declarations
- WalshNorm.lean 15 declarations
- WalshSymmetry.lean 14 declarations
- WeightedCompact.lean 13 declarations