OAI/MeasureTheory/FalconerCompletion/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Conditional starting-pair completion for Euclidean distance sets.
This file declares nothing itself. It gathers the 8 imports below, so a file that imports it gets all of them.
Imports
- OAI.MeasureTheory.FalconerCompletion.Estimates.EuclideanSourceFarRegion
- OAI.MeasureTheory.FalconerCompletion.Estimates.SourceFullFar
- OAI.MeasureTheory.FalconerCompletion.Graphs.GraphHFFiniteJetEstimate
- OAI.MeasureTheory.FalconerCompletion.Graphs.LiteralDyadicPaths
- OAI.MeasureTheory.FalconerCompletion.Measures.StartingPairCompletion
- OAI.MeasureTheory.FalconerCompletion.Recursion.OccupiedFarCountTerminal
- OAI.MeasureTheory.FalconerCompletion.Recursion.PrefixShellLeSourceShellSuccessor
- OAI.MeasureTheory.FalconerCompletion.Shells.PrefixPhasedGlobalBound