OAI/MeasureTheory/FalconerCompletion/Shells/PrefixHighShell.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actual_prefix_high_shell line 25
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixHighIndices_spec line 144
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixHighIndices_card_bound line 149
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixHigh_sum_bound line 155
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixHigh_error_absorption line 163
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefix_high_accumulation line 187
  7. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actual_prefix_reduction line 205