OAI/Combinatorics/SharpThreshold/
507 declarations, 0 contain sorry, 0 declared as axioms; 78 files
Files
- BlockAverage.lean 8 declarations
- BlockCapture.lean 4 declarations
- BlockCounting.lean 20 declarations
- BlockIncidence.lean 6 declarations
- BlockInfluence.lean 4 declarations
- BlockLowDegree.lean 6 declarations
- BlockOrbit.lean 14 declarations
- BlockOrbitSubtype.lean 2 declarations
- BlockOrbits.lean 12 declarations
- BlockParameters.lean 11 declarations
- BlockRestrictionSymmetry.lean 13 declarations
- BlockSize.lean 8 declarations
- BlockSymmetry.lean 6 declarations
- BooleanDerivative.lean 8 declarations
- BooleanProjection.lean 2 declarations
- DirichletEnergy.lean 4 declarations
- ExpQuadratic.lean 4 declarations
- FiniteParseval.lean 9 declarations
- FourierAnalysis.lean 7 imports, no declarations
- FourierBasis.lean 20 declarations
- FourierDerivative.lean 13 declarations
- FourierDirichlet.lean 7 declarations
- FourierHypercontractive.lean 5 declarations
- FourierNoise.lean 10 declarations
- FourierOption.lean 6 declarations
- FourierOptionExpectation.lean 3 declarations
- FourierOrthogonality.lean 8 declarations
- FourierProjection.lean 6 declarations
- FourierReindex.lean 10 declarations
- FourierRestriction.lean 3 declarations
- FourierRestrictionMass.lean 3 declarations
- FourierSupportSplit.lean 3 declarations
- FourierVariance.lean 16 declarations
- GraphBlockAverage.lean 3 declarations
- GraphBlockCapture.lean 11 declarations
- GraphQuantile.lean 4 declarations
- GraphRestrictionInfluence.lean 7 declarations
- GraphSupport.lean 5 imports, no declarations
- GraphSymmetry.lean 10 imports, no declarations
- GraphVarianceBound.lean 4 declarations
- HypercontractiveTensor.lean 4 declarations
- InfluenceReindex.lean 12 declarations
- LowDegree.lean 4 declarations
- LowDegreeBounds.lean 5 declarations
- LowDegreeConstants.lean 5 declarations
- LowDegreeCounting.lean 2 declarations
- LowDegreeInfluence.lean 5 declarations
- LowDegreeL4.lean 2 declarations
- LowDegreeNumerical.lean 3 declarations
- LowDegreeSupport.lean 4 imports, no declarations
- Main.lean 2 declarations
- MeanEndpoints.lean 10 declarations
- Model.lean 15 declarations
- NoiseKernel.lean 2 declarations
- OrbitInfluence.lean 2 declarations
- Permutation.lean 16 declarations
- Probability.lean 19 declarations
- ProductReindex.lean 4 declarations
- ProductRestriction.lean 7 imports, no declarations
- ProjectionIdentities.lean 6 declarations
- ProjectionNorm.lean 5 declarations
- Quantile.lean 8 declarations
- QuantileAnalysis.lean 3 declarations
- RestrictionInfluence.lean 10 declarations
- RestrictionMass.lean 3 declarations
- RestrictionMassSubtype.lean 12 declarations
- Russo.lean 9 declarations
- RussoReindex.lean 11 declarations
- SharpThreshold.lean 2 declarations
- SpectralBounds.lean 10 declarations
- SupportDegree.lean 8 declarations
- SupportDegreeGraph.lean 3 declarations
- SupportIncidence.lean 6 declarations
- ThresholdConstants.lean 3 declarations
- ThresholdODE.lean 3 declarations
- TwoPoint.lean 5 declarations
- VarianceConstants.lean 3 declarations
- VarianceReduction.lean 2 declarations