OAI/MeasureTheory/FalconerCompletion/Measures/DistanceCollisionKernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. def OAI.GraphLiteralSupport.Attempt4FullFar.distanceCollisionKernelND line 22
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.distanceCollisionKernelND_nonneg line 26
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.distanceCollisionKernelND_le_one line 30
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.distanceCollisionKernelND_measurable line 37
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.distanceCollisionKernelND_integrable line 42
  6. theorem OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistance_kernel_realND line 49
  7. theorem OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistance_supported_integralND line 67
  8. def OAI.GraphLiteralSupport.Attempt4FullFar.farUnitDirectionND line 102
  9. lemma OAI.GraphLiteralSupport.Attempt4FullFar.farUnitDirectionND_norm line 105
  10. theorem OAI.GraphLiteralSupport.Attempt4FullFar.original_far_integratedND line 111