OAI/MeasureTheory/FalconerCompletion/Measures/MaskedPushforwardDeficit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. theorem OAI.CurrentFalconer.AssemblyRetention.masked_pushforward_deficit line 15
  2. abbrev OAI.CurrentFalconer.AssemblyLimit.Ambient line 68
  3. def OAI.CurrentFalconer.AssemblyLimit.distanceSet line 69
  4. def OAI.CurrentFalconer.AssemblyLimit.pairDistance line 71
  5. def OAI.CurrentFalconer.AssemblyLimit.pairWeight line 72
  6. def OAI.CurrentFalconer.AssemblyLimit.filteredDistanceMeasure line 75