OAI/MeasureTheory/Falconer/Shells/EndpointWeightedDistance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The weighted distance law for two different endpoint profiles

Both original marginal laws and their separate normalizations are retained. The endpoint factors may be the actual descriptor products of different regularized classes. No common probability law is introduced.

  1. def OAI.Falconer.endpointDistanceWeight line 17
  2. def OAI.Falconer.endpointWeightedDistance line 22
  3. theorem OAI.Falconer.endpointDistanceWeight_measurable line 27
  4. theorem OAI.Falconer.endpointDistanceWeight_nonneg line 37
  5. theorem OAI.Falconer.endpointDistanceWeight_bound line 43
  6. theorem OAI.Falconer.endpointWeightedDistance_finite line 54
  7. theorem OAI.Falconer.endpointWeightedDistance_fourier line 71