OAI/MeasureTheory/Falconer/Estimates/ScalarBunchingSuffix.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Minimal heavy suffixes for the porous level-bunching construction. Trimming a short terminal segment has a controlled entropy cost.

  1. theorem OAI.Falconer.scalar_minimal_heavy_suffix line 10
  2. theorem OAI.Falconer.scalar_heavy_suffix_trim line 31
  3. def OAI.Falconer.scalarBunchTrim line 44
  4. theorem OAI.Falconer.scalarBunchTrim_lt line 46
  5. theorem OAI.Falconer.scalarBunchTrim_budget line 52
  6. theorem OAI.Falconer.scalarBunchTrim_lower line 59
  7. theorem OAI.Falconer.scalar_bunch_retained_weight line 66