OAI/MeasureTheory/Falconer/Estimates/ScalarPorousEndpoints.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ordered endpoints selected from the actual porous levels, extended monotonically beyond the final endpoint without altering selected data.

  1. theorem OAI.Falconer.Regularization.scalar_porous_endpoint_enumeration line 9