OAI/MeasureTheory/Falconer/Estimates/ProjectedSubsetRegularity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded projected energy controls every large original subset. After discarding at most half its labels, its projected counting law has an explicit Frostman bound. Repeated projected coordinates are retained.

  1. theorem OAI.Falconer.projected_subset_weighted_regular line 12