OAI/MeasureTheory/Falconer/Geometry/RegularSmallProjections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strict small-projection obstruction for an actual regular planar set and a nonconcentrated family of directions, with all weak losses chosen.

  1. theorem OAI.Falconer.base_radius_identity line 11
  2. theorem OAI.Falconer.regular_small_projection_obstruction line 18