OAI/MeasureTheory/Falconer/Measures/InverseSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The inverse amplitudes have no incoming-pole contribution

Their fixed patch support places the opposite prepared direction outside their support. Locality of the actual stationary coefficients then removes all incoming coefficients, without a differential-operator assumption.

  1. theorem OAI.Falconer.prepared_direction_opposite_far line 17
  2. theorem OAI.Falconer.localInverseAmplitude_antipodal_coefficient_zero line 36