OAI/MeasureTheory/Falconer/Recursion/ParallelProfile.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The inverse-power sum for actual parallel-test centers

The critical kernel exponent is arbitrary here so the application can use d/2. Every counted center belongs to the original normalized class.

  1. def OAI.Falconer.Regularization.parallelTestCells line 19
  2. def OAI.Falconer.Regularization.parallelTestCount line 23
  3. theorem OAI.Falconer.Regularization.parallel_inverse_power_sum line 28
  4. def OAI.Falconer.Regularization.parallelPackingConstant line 63
  5. theorem OAI.Falconer.Regularization.sourceClass_parallel_inverse_power line 67