OAI/MeasureTheory/Falconer/Angular/LongitudinalCapTerm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The longitudinal discarded cap term

The failed test is imposed on the two fixed cap centers and cell-center displacements. Cap support and point-replacement errors transfer it to the actual phase. Radial Fubini then applies Schwartz decay before any absolute values are taken in the cell expansion.

  1. theorem OAI.Falconer.longitudinal_discarded_cap_term_bound line 19