OAI/MeasureTheory/Falconer/Geometry/ScalarNetIteration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Repeated finite sum-product amplification of a power-scale interval net, with its exact error recurrence.

  1. theorem OAI.Falconer.scalarCoefficientClosure_step line 10
  2. theorem OAI.Falconer.scalarCoefficientClosure_sum_product line 15
  3. theorem OAI.Falconer.scalarCoefficientClosure_zero line 25
  4. def OAI.Falconer.scalarNetError line 31
  5. theorem OAI.Falconer.scalarNetError_bounds line 35
  6. theorem OAI.Falconer.scalarNetError_formula line 44
  7. theorem OAI.Falconer.scalar_interval_net_iterate line 52