OAI/MeasureTheory/Falconer/Incidence/IncidenceProductChain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite composition of the actual pencil-normalized scale ratios. The terminal estimate needs only a single nonempty pencil.

  1. theorem OAI.Falconer.pencil_union_ratio_one_le line 10
  2. theorem OAI.Falconer.finite_scale_ratio_product line 20
  3. theorem OAI.Falconer.finite_scale_power_ratio line 40
  4. theorem OAI.Falconer.finite_scale_power_gain line 48