DiscardedCapTerm.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The complete angular–radial error for one discarded cap term

Spatial labels remain in their original finite measure. The adapted frame is fixed before these labels are integrated. The phase is the four-point phase after the two displacements have been formed.

theorem OAI.Falconer.discarded_cap_term_bound line 19