OAI/MeasureTheory/Falconer/Geometry/ScalarForkGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A witnessed pair of regularized child centers separates their entire descendant fibers. This supplies the nonporous binary fork geometry.

  1. theorem OAI.Falconer.Regularization.scalar_prefix_leaf_center_dist line 9
  2. theorem OAI.Falconer.Regularization.scalar_fork_leaf_bounds line 20