OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedCellGroup.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BinaryFraction.preparedCellGroupWithWork line 22
2. theorem OAI.EditApproximation.BinaryFraction.preparedCellGroupWithWork_reference line 33
3. theorem OAI.EditApproximation.BinaryFraction.preparedCellGroupWithWork_value line 63

   Source documentation

   The rational cell-group program at the exact natural parameter. Transport preserves its values and changes only proof indices.

   theorem preparedCellGroupWithWork_value (cell : ℕ × ℕ) (hP : 0 < P) :
       ((preparedCellGroupWithWork source target parent b P F exponent Q hb tau a parentInitial child initial current
         raw hraw draw hP cell).1.map BinaryBellmanAction.decode) =
         chooseCellGroupAction source target parent b P F exponent Q tau.value a.value
           (fun q => (parentInitial q).value) (fun i q => (child i q).value)
           (fun i q => (initial i q).value) (fun i q => (current i q).value) cell
           (Eq.mp (congrArg (cellScaleDraw M b Q) (nat_value F)) draw) := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction.preparedCellGroupWithWork, OAI.EditApproximation.BinaryBellmanAction.decode, OAI.EditApproximation.chooseCellGroupAction, OAI.EditApproximation.BinaryFraction.value, OAI.EditApproximation.BinaryFraction.cellScaleDraw, OAI.EditApproximation.BinaryFraction.nat_value