OAI/Geometry/BallPacking/Necessity/
1044 declarations, 0 contain sorry, 0 declared as axioms; 38 files
Files
- AffineBubble.lean 30 declarations
- AffineEnergy.lean 28 declarations
- AffineSlopes.lean 24 declarations
- C1Energy.lean 18 declarations
- CauchyDuality.lean 33 declarations
- CompactContinuation.lean 11 declarations
- DensityBounds.lean 20 declarations
- DensityExistence.lean 12 declarations
- DensityLimits.lean 29 declarations
- DensityMaps.lean 21 declarations
- DensityResidual.lean 25 declarations
- EqualDimension.lean 3 declarations
- FiniteContinuation.lean 21 declarations
- FiniteReduction.lean 13 declarations
- FrameFredholm.lean 55 declarations
- FramedCompactness.lean 19 declarations
- FreezeJ.lean 7 declarations
- FrozenInverse.lean 34 declarations
- FrozenOperators.lean 13 declarations
- FrozenResponse.lean 17 declarations
- GlobalArea.lean 18 declarations
- GradientLimits.lean 25 declarations
- HolderCalculus.lean 41 declarations
- HolderCompactness.lean 48 declarations
- HolderCompletion.lean 31 declarations
- KernelMoments.lean 46 declarations
- LocalCharts.lean 28 declarations
- Main.lean 1 import, no declarations
- MarkedInverse.lean 51 declarations
- MarkedProfiles.lean 29 declarations
- NonlinearCR.lean 57 declarations
- OrbitRegularity.lean 34 declarations
- PackingNecessity.lean 23 declarations
- PlanarEnergy.lean 36 declarations
- Properness.lean 30 declarations
- SchauderBounds.lean 29 declarations
- SquareBounds.lean 57 declarations
- TangentLimits.lean 28 declarations