OAI/MeasureTheory/Falconer/Fourier/FarCollisionIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The stationary far kernel on the original collision laws

The original four-point law is reassembled before the comparable-depth partition. Only two free cell labels remain in the resulting collision bound.

  1. theorem OAI.Falconer.originalFourPoint_far_tested_bound line 18
  2. theorem OAI.Falconer.exists_jetState_far_collision_integral line 69