OAI/MeasureTheory/Falconer/Estimates/ScalarCorrelatedWeights.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The same coefficient is used at every porous scale. The following finite Jensen estimate averages products without any independence assumption on the exceptional sets.

  1. theorem OAI.Falconer.finite_correlated_product_mean line 12
  2. def OAI.Falconer.scalarCollisionWeight line 53
  3. theorem OAI.Falconer.scalarCollisionWeight_pos line 56
  4. theorem OAI.Falconer.scalarCollisionWeight_log_sum line 61
  5. theorem OAI.Falconer.scalarCollisionWeight_log_bound line 73