OAI/Combinatorics/EditApproximation/Refinement/ComputedSourceAddressBits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual uniform source-range address fits in one logarithmic input word eventually. The coefficient can be any fixed natural number.

  1. theorem OAI.EditApproximation.computed_sourceAddressBits_div_height_tendsto line 14
  2. theorem OAI.EditApproximation.computed_sourceAddressBits_le_height line 41
  3. theorem OAI.EditApproximation.computed_localOnlineMassBound_word line 51