OAI/MeasureTheory/Falconer/Estimates/PacketSamplingBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual retained point fraction supplies the projection-sampling budget; it is not an additional regularity assumption.

  1. theorem OAI.Falconer.packet_sampling_budget line 10