OAI/MeasureTheory/Falconer/Estimates/ParallelNumerics.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Scale cancellation and absorption for the parallel-test average

  1. theorem OAI.Falconer.Regularization.parallel_mean_scale_identity line 9
  2. theorem OAI.Falconer.Regularization.parallel_coefficient_bound line 27
  3. theorem OAI.Falconer.Regularization.one_add_power_absorb line 37