OAI/Combinatorics/EditApproximation/Geometry/RefinementBandSupport.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Band-table congruence uses proof-free data. Equality of these data preserves the ordered minimization and its tie decisions, even though the guard records have different table-indexed types.

  1. abbrev OAI.EditApproximation.UnskippedBandData line 13
  2. def OAI.EditApproximation.UnskippedBand.data line 16
  3. def OAI.EditApproximation.UnskippedBandData.action line 23
  4. def OAI.EditApproximation.UnskippedBandData.estimate line 27
  5. theorem OAI.EditApproximation.rational_argmax_map line 36
  6. theorem OAI.EditApproximation.testUnskippedBand_center_of_some line 50
  7. theorem OAI.EditApproximation.unskippedBand_data_congr line 60
  8. theorem OAI.EditApproximation.testUnskippedBand_data_congr line 98
  9. theorem OAI.EditApproximation.unskippedBandList_data_congr line 125
  10. theorem OAI.EditApproximation.chooseCellGroupAction_data line 141
  11. theorem OAI.EditApproximation.chooseCellGroupAction_congr_bandTables line 164
  12. def OAI.EditApproximation.bandDataOnlineCandidate line 189

    Source documentation

    Keep the optimizer opaque while transporting the finite band data.

    def bandDataOnlineCandidate {M ny : ℕ} (band : List (Fin M → TargetInterval ny))
    (envelope : Fin M → ℚ) (H : ℕ) (eta kappa : ℚ)
    (children : PhysicalChildTables M ny) (t : ℕ) (r : TargetInterval ny)
    (integer : ℕ) (accepted : Bool) : Option (PhysicalRationalAction M ny) :=
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.PhysicalRationalAction

  13. theorem OAI.EditApproximation.keyedOnlineCandidate_test_form line 205
  14. theorem OAI.EditApproximation.keyedOnlineCandidate_congr_bandTables line 226
  15. theorem OAI.EditApproximation.wideWarmupInputs_pair line 248
  16. theorem OAI.EditApproximation.localOnlineCandidates_congr_bandTables line 278
  17. theorem OAI.EditApproximation.localCellGroupActions_congr_bandTables line 298