OAI/MeasureTheory/Falconer/Measures/PreparedMeasure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The fixed positive weighted source of the shell reconstruction

All weights and distances use the original ambient space. The coarse filters may vary with scale; the source measure does not.

  1. def OAI.Falconer.PreparedOriginalPair.source line 18
  2. theorem OAI.Falconer.PreparedOriginalPair.weight_bounds line 22
  3. theorem OAI.Falconer.PreparedOriginalPair.source_finite line 39
  4. theorem OAI.Falconer.PreparedOriginalPair.source_positive line 43
  5. theorem OAI.Falconer.PreparedOriginalPair.source_carried line 50