OAI/Analysis/LpDimension/
443 declarations, 0 contain sorry, 0 declared as axioms; 45 files
Files
- AboveParameters.lean 2 declarations
- AboveTwo.lean 1 declarations
- BelowTwo.lean 1 declarations
- ClippedMoments.lean 15 declarations
- CompoundPoisson.lean 16 declarations
- ConvexRepresentation.lean 4 declarations
- ConvexSelection.lean 9 declarations
- ConvolutionError.lean 5 declarations
- CoordinateLaws.lean 13 declarations
- CutoffEnvelope.lean 2 declarations
- Discretization.lean 21 declarations
- DyadicInterpolation.lean 4 declarations
- DyadicRamps.lean 28 declarations
- ElectricalProjection.lean 12 declarations
- Entropy.lean 29 declarations
- ExactDiscretization.lean 3 declarations
- FourierTails.lean 17 declarations
- GlobalCutoff.lean 8 declarations
- GradientLaws.lean 7 declarations
- GradientSampling.lean 12 declarations
- GridObstruction.lean 19 declarations
- HeatKernel.lean 26 declarations
- HeatLocalization.lean 6 declarations
- LogLimits.lean 1 declarations
- Main.lean 1 declarations
- Model.lean 4 declarations
- Packing.lean 13 declarations
- Parallelogram.lean 18 declarations
- Pareto.lean 7 declarations
- PowerEstimates.lean 3 declarations
- ProjectedRamps.lean 8 declarations
- RampError.lean 3 declarations
- RampLaws.lean 10 declarations
- RampRetraction.lean 4 declarations
- RampSum.lean 1 declarations
- RetractionIntegrals.lean 8 declarations
- Retractions.lean 16 declarations
- Sampling.lean 4 declarations
- SamplingBounds.lean 7 declarations
- SpectralProjection.lean 15 declarations
- StableIntensity.lean 12 declarations
- StableLaw.lean 13 declarations
- StableRetractions.lean 9 declarations
- SymmetricLaws.lean 10 declarations
- SymmetricMoments.lean 16 declarations