OAI/MeasureTheory/Falconer/Geometry/ScalarClosureProjections.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Small scalar projections are preserved through each finite additive/multiplicative closure stage with the explicit saved budget.

  1. theorem OAI.Falconer.scalar_closure_projections line 10