OAI/MeasureTheory/Falconer/Angular/SphereInverse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual outgoing inverse expansion on the prepared patch

The finite inverse amplitudes remove the outgoing coefficient series. Their fixed patch support removes every incoming coefficient. All errors have the same total frequency order and the same derivative budget.

  1. theorem OAI.Falconer.stationary_weight_eq line 18
  2. theorem OAI.Falconer.stationary_weight_mul line 23
  3. def OAI.Falconer.inverseSphereSum line 27
  4. theorem OAI.Falconer.inverse_direct_sum line 32
  5. theorem OAI.Falconer.sphere_inverse_expansion line 40