OAI/MeasureTheory/FalconerCompletion/Measures/StartingPairCompletion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. theorem OAI.CurrentFalconer.AssemblyCompletion.starting_pair_completion line 15
  2. abbrev OAI.Falconer.Space line 112

    Also declared: OAI/MeasureTheory/Falconer/Estimates/AllDimensions.lean:26 (same declaration text).

  3. def OAI.Falconer.distanceSet line 114

    Distinct definitions of this name: OAI/MeasureTheory/Falconer/Estimates/AllDimensions.lean:29 (different declaration text). Qualify references as OAI.Falconer.distanceSet@path.

  4. theorem OAI.Falconer.distanceSet_eq_norm_sub line 117
  5. theorem OAI.Falconer.distanceSet_eq_image line 121

    Distinct definitions of this name: OAI/MeasureTheory/Falconer/Estimates/AllDimensions.lean:40 (different declaration text). Qualify references as OAI.Falconer.distanceSet_eq_image@path.

  6. theorem OAI.Falconer.distanceSet_isCompact line 130

    Distinct definitions of this name: OAI/MeasureTheory/Falconer/Estimates/AllDimensions.lean:49 (different declaration text). Qualify references as OAI.Falconer.distanceSet_isCompact@path.

  7. theorem OAI.Falconer.distanceSet_measurable line 135
  8. theorem OAI.Falconer.distanceSet_positive_of_carried_ac_measure line 138
  9. theorem OAI.Falconer.distanceSet_eq_assembly line 155
  10. theorem OAI.Falconer.distanceSet_positive_of_starting_pair line 158