OAI/Combinatorics/EditApproximation/Refinement/PhysicalLocalDenominator.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Denominator and bit bounds for the local evaluator on every incoming seed. The proofs use the literal local candidates and do not pass through the good-seed equality with the complete evaluator.

  1. theorem OAI.EditApproximation.physicalLocalWarmup_den_one line 14
  2. theorem OAI.EditApproximation.rationalLocalWideStep_den_dvd line 35
  3. theorem OAI.EditApproximation.keyedOnlineCandidate_connection_den line 74
  4. theorem OAI.EditApproximation.localOnlineCandidates_connection_den line 89
  5. theorem OAI.EditApproximation.physicalLocalOnline_connection_den line 104
  6. theorem OAI.EditApproximation.physicalLocalRefinement_den_dvd line 118
  7. theorem OAI.EditApproximation.physicalLocalRefinement_encoding_bits line 166
  8. theorem OAI.EditApproximation.physicalLocalOnlineRefinement_den_dvd line 195
  9. theorem OAI.EditApproximation.physicalLocalWarmup_encoding_bits line 207
  10. theorem OAI.EditApproximation.physicalLocalOnlineRefinement_encoding_bits line 224