OAI/MeasureTheory/Falconer/Estimates/ScalarPrefixTruncation.lean
6 declarations, 0 contain sorry, 0 declared as axioms
Truncation retains all prefix fibers above the truncation depth.
- theorem
OAI.Falconer.Regularization.prefixFiber_image_takeline 8 - theorem
OAI.Falconer.Regularization.prefixChildren_image_takeline 24 - theorem
OAI.Falconer.Regularization.prefix_image_take_takeline 31 - theorem
OAI.Falconer.Regularization.prefix_image_take_cubePathsline 36 - theorem
OAI.Falconer.Regularization.prefixChildren_sameline 45 - theorem
OAI.Falconer.Regularization.prefixChildren_card_composeline 59