OAI/MeasureTheory/Falconer/Estimates/DirectedSampledRows.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous row construction from the actual large subsets of the coarse cells. Cardinality and regularity use a common explicit budget.

  1. theorem OAI.Falconer.directed_sampled_packet_rows line 10