OAI/MeasureTheory/Falconer/Angular/CapScaleGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The cap and cell replacement error at the graph scales

The geometric constant is explicit. The fixed gap between 10σ and 30σ makes the point-replacement and cap-replacement errors less than half the failed-test threshold once the displayed power inequality holds.

  1. theorem OAI.Falconer.graph_cap_replacement_scale line 15
  2. theorem OAI.Falconer.graph_cap_replacement_small line 31