OAI/Combinatorics/EditApproximation/Binary/BinaryCellGroupKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

One complete whole-cell group: enumerate its eligible centers, execute every band guard, estimate all surviving members with the original finite draws, and select the same ordered minimum.

  1. abbrev OAI.EditApproximation.BinaryFraction.cellScaleDraw line 14
  2. def OAI.EditApproximation.BinaryFraction.cellReferenceAction line 18
  3. theorem OAI.EditApproximation.BinaryFraction.cellReferenceAction_transport line 27
  4. def OAI.EditApproximation.BinaryFraction.cellGroupWithWork line 49
  5. theorem OAI.EditApproximation.BinaryFraction.cellGroupWithWork_reference line 60
  6. theorem OAI.EditApproximation.BinaryFraction.cellGroupWithWork_value line 90

    Source documentation

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

    theorem cellGroupWithWork_value (cell : ℕ × ℕ) (hP : 0 < P) :
    ((cellGroupWithWork source target parent b P F exponent Q hb tau a parentInitial child initial current
      raw hraw draw 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.cellGroupWithWork, OAI.EditApproximation.BinaryBellmanAction.decode, OAI.EditApproximation.chooseCellGroupAction, OAI.EditApproximation.BinaryFraction.value, OAI.EditApproximation.BinaryFraction.cellScaleDraw, OAI.EditApproximation.BinaryFraction.nat_value