OAI/Analysis/DiamondDistortion/
1113 declarations, 0 contain sorry, 0 declared as axioms; 38 files
Files
- AMUC.lean 9 declarations
- Ancestry.lean 63 declarations
- Backward.lean 10 declarations
- CoordinateDual.lean 29 declarations
- CoordinateSpace.lean 33 declarations
- Descent.lean 11 declarations
- DiamondGraph.lean 39 declarations
- DirectEnergy.lean 23 declarations
- EquivalentNorm.lean 55 declarations
- FiniteAverage.lean 7 declarations
- ForestModels.lean 19 declarations
- FullDual.lean 28 declarations
- GraphBounds.lean 15 declarations
- HeadProjections.lean 17 declarations
- Incomparable.lean 24 declarations
- InfimalCost.lean 7 declarations
- IntrinsicTail.lean 3 declarations
- LpDual.lean 16 declarations
- Main.lean 1 import, no declarations
- MidpointHeads.lean 17 declarations
- ModelMaps.lean 40 declarations
- Orthogonality.lean 14 declarations
- PathBounds.lean 12 declarations
- PathLenses.lean 29 declarations
- PathModels.lean 61 declarations
- RecursiveBounds.lean 42 declarations
- RecursiveLenses.lean 22 declarations
- RecursiveModels.lean 133 declarations
- Relations.lean 7 declarations
- SegmentNorm.lean 128 declarations
- SignCube.lean 48 declarations
- StartBounds.lean 41 declarations
- StartModels.lean 26 declarations
- Stretch.lean 16 declarations
- Transfers.lean 16 declarations
- UpperFunction.lean 34 declarations
- Vanishing.lean 5 declarations
- WeakLenses.lean 14 declarations