OAI/MeasureTheory/Falconer/Estimates/LocalInverse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite inverse amplitudes built from the actual local jets

Each recursive amplitude is globally smooth and supported in the same fixed pole patch. The diagonal cancellation is pointwise on the prepared inner patch and does not assume a spherical differential-operator identity.

  1. def OAI.Falconer.localInverseAmplitude line 16
  2. theorem OAI.Falconer.localInverseAmplitude_contDiff line 25
  3. theorem OAI.Falconer.localInverseAmplitude_zero_of_mask_zero line 40
  4. theorem OAI.Falconer.localInverseAmplitude_tsupport line 49
  5. theorem OAI.Falconer.localInverseAmplitude_cancellation line 55
  6. theorem OAI.Falconer.localInverseAmplitude_cancellation_reverse line 74
  7. theorem OAI.Falconer.localInverseAmplitude_triangle line 86