OAI/MeasureTheory/FalconerCompletion/Measures/PairDistanceContinuous.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. lemma OAI.CurrentFalconer.AssemblyLimit.pairDistance_continuous line 14
  2. lemma OAI.CurrentFalconer.AssemblyLimit.pairWeight_measurable line 15
  3. def OAI.CurrentFalconer.AssemblyLimit.weightedOriginalPair line 17
  4. lemma OAI.CurrentFalconer.AssemblyLimit.filteredDistanceMeasure_eq line 19
  5. lemma OAI.CurrentFalconer.AssemblyLimit.original_pair_ae line 29
  6. lemma OAI.CurrentFalconer.AssemblyLimit.weightedOriginalPair_finite line 35
  7. lemma OAI.CurrentFalconer.AssemblyLimit.originalPair_ac_weighted line 52
  8. lemma OAI.CurrentFalconer.AssemblyLimit.distanceSet_compact line 59
  9. lemma OAI.CurrentFalconer.AssemblyLimit.filteredDistanceMeasure_carried line 69