OAI/MeasureTheory/Falconer/Shells/PartitionEndpointDistance.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact distance law for class-dependent endpoint masks

  1. def OAI.Falconer.endpointPairMask line 13
  2. theorem OAI.Falconer.endpointPairMask_measurable line 17
  3. def OAI.Falconer.partitionEndpointDistance line 25
  4. theorem OAI.Falconer.partitionEndpointDistance_eq_sum line 33
  5. theorem OAI.Falconer.partitionEndpointDistance_product_sum line 56