OAI/MeasureTheory/Falconer/Angular/FourPointCaps.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact cap expansion of an endpoint cross term

Each cap weight stays inside the original four-point amplitude. The only factor removed from the integral is the product of the four model-mass normalizations. The measures are the original restricted endpoint laws.

  1. def OAI.Falconer.capPairAmplitude line 18
  2. def OAI.Falconer.endpointCapCrossTerm line 22
  3. theorem OAI.Falconer.endpointCapCrossTerm_four_point line 32
  4. theorem OAI.Falconer.capPairAmplitude_measurable line 67
  5. theorem OAI.Falconer.capPairAmplitude_norm_le line 77