OAI/Combinatorics/EditApproximation/Specification/RawBand.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.UnskippedBand.raw line 10

   Source documentation

   The finite data used after accepting an unskipped band.

   def UnskippedBand.raw {α : Type*} {source target : List α} {M : ℕ}
       {parent : TargetInterval source.length} {b P exponent : ℕ}
       {tau F : ℚ} {child initial : Fin M → TargetInterval target.length → ℚ}
       (member : UnskippedBand source target parent b P exponent tau F child initial) :
       RawUnskippedBand M target.length :=
   …

   Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.UnskippedBand, OAI.EditApproximation.RawUnskippedBand

2. theorem OAI.EditApproximation.BinaryFraction.preparedUnskippedReadWithWorkRaw_eq line 21