OAI/Combinatorics/EditApproximation/Binary/BinaryEnvelopeSpace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Scratch replay for the bounded dyadic scan and the actual band initial-value reads used to form each child envelope.

  1. theorem OAI.EditApproximation.BinaryFraction.dyadicScanAllocation_le_work line 16
  2. theorem OAI.EditApproximation.BinaryFraction.dyadicCeilingAllocation_le_work line 32
  3. theorem OAI.EditApproximation.BinaryFraction.bandEnvelopeReadAllocation_le_work line 41
  4. theorem OAI.EditApproximation.BinaryFraction.envelopeVectorReadAllocation_le_work line 61
  5. def OAI.EditApproximation.BinaryFraction.dyadicScanInvocations line 68
  6. theorem OAI.EditApproximation.BinaryFraction.dyadicScanInvocations_le_work line 74
  7. def OAI.EditApproximation.BinaryFraction.dyadicCeilingInvocations line 85
  8. theorem OAI.EditApproximation.BinaryFraction.dyadicCeilingInvocations_le_work line 88
  9. def OAI.EditApproximation.BinaryFraction.bandEnvelopeReadInvocations line 95
  10. theorem OAI.EditApproximation.BinaryFraction.bandEnvelopeReadInvocations_le_work line 105
  11. def OAI.EditApproximation.BinaryFraction.envelopeVectorReadInvocations line 123
  12. theorem OAI.EditApproximation.BinaryFraction.envelopeVectorReadInvocations_le_work_add_one line 128