OAI/Combinatorics/EditApproximation/Refinement/PhysicalCachedWords.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The cache normalization algorithm applied to the actual all-seed local table invariants. These word bounds require neither a good-seed event nor a bound on the temporary numerator and denominator before normalization.

  1. theorem OAI.EditApproximation.physicalLocalRefinement_cached_word line 12
  2. theorem OAI.EditApproximation.physicalLocalOnlineRefinement_cached_word line 45
  3. theorem OAI.EditApproximation.physicalLocalWarmup_cached_word line 65