OAI/MeasureTheory/Falconer/Recursion/ScalarBinaryBranch.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A nonporous binary state produces many separated children in a fixed-fold sumset. Only actual bit updates of original words are used.

  1. def OAI.Falconer.ScalarBinaryTail line 11
  2. def OAI.Falconer.scalarBinaryStep line 14
  3. def OAI.Falconer.scalarBinarySum line 18
  4. theorem OAI.Falconer.scalar_binary_step_tail line 21
  5. theorem OAI.Falconer.scalar_binary_step_sum line 32
  6. theorem OAI.Falconer.scalar_binary_sum_mem line 42
  7. theorem OAI.Falconer.scalar_binary_branch line 48