OAI/Analysis/TreePotential/
1292 declarations, 0 contain sorry, 0 declared as axioms; 46 files
Files
- Clipping.lean 56 declarations
- Completion.lean 13 declarations
- Coordinates.lean 24 declarations
- CostCompletion.lean 24 declarations
- CostGeometry.lean 30 declarations
- CostObstruction.lean 24 declarations
- DualCoordinates.lean 16 declarations
- Dyadic.lean 21 declarations
- EndpointTransfer.lean 23 declarations
- FiniteHeads.lean 30 declarations
- FiniteTree.lean 57 declarations
- FreeRoot.lean 24 declarations
- HilbertCompletion.lean 27 declarations
- HilbertSum.lean 23 declarations
- Inward.lean 45 declarations
- Leakage.lean 21 declarations
- LinearCost.lean 26 declarations
- Main.lean 1 declarations
- Moduli.lean 15 declarations
- NormIdentities.lean 24 declarations
- Normalization.lean 6 declarations
- QuadraticCost.lean 59 declarations
- RealModuli.lean 18 declarations
- SegmentBasic.lean 49 declarations
- SegmentCancellation.lean 22 declarations
- SegmentComponents.lean 42 declarations
- SegmentDual.lean 38 declarations
- SegmentEndpoints.lean 9 declarations
- SegmentHeads.lean 27 declarations
- SegmentMidpoint.lean 18 declarations
- SegmentMixtures.lean 35 declarations
- SegmentPolar.lean 32 declarations
- StartComponent.lean 48 declarations
- StartEnergy.lean 47 declarations
- StartMass.lean 23 declarations
- StartModulus.lean 29 declarations
- StartPolar.lean 27 declarations
- StartQuotient.lean 25 declarations
- StartRepresentation.lean 29 declarations
- TailEstimates.lean 44 declarations
- TestNorm.lean 27 declarations
- TreeObstruction.lean 35 declarations
- TreeTests.lean 50 declarations
- UniformAverages.lean 6 declarations
- UniformProtocols.lean 7 declarations
- WeakNull.lean 16 declarations