OAI/Combinatorics/EditApproximation/Geometry/BandOptimizerWork.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Reindexing the exact finite optimizer onto an explicit, duplicate-free coordinate array. The array order is retained throughout the evaluation.

  1. def OAI.EditApproximation.restrictOptimizerVector line 15
  2. theorem OAI.EditApproximation.restrictOptimizerVector_get line 19
  3. theorem OAI.EditApproximation.coordinateVector_sum line 24
  4. theorem OAI.EditApproximation.rationalLinearizationMaximizer_restrict line 35
  5. theorem OAI.EditApproximation.finiteRationalOptimizer_restrict line 54
  6. theorem OAI.EditApproximation.materializedOptimizerWithWork_restrict_value line 78
  7. theorem OAI.EditApproximation.listedBandCoordinates_nodup line 101

    Source documentation

    Concrete ordered coordinates; no enumeration of the ambient state type and no choice of an equivalence is used by the evaluator.

    theorem listedBandCoordinates_nodup {M : ℕ} {σ : Type*} [DecidableEq σ]
    (band : List (Fin M → σ)) : (listedBandCoordinates band).Nodup :=
…

    Mentions: OAI.EditApproximation.listedBandCoordinates

  8. theorem OAI.EditApproximation.listedBandCoordinates_toFinset line 105
  9. def OAI.EditApproximation.listedBandCoordinateVector line 124
  10. theorem OAI.EditApproximation.listedBandCoordinateVector_toList line 128
  11. theorem OAI.EditApproximation.listedBandCoordinates_length line 133
  12. def OAI.EditApproximation.materializedBandActionWithWork line 139
  13. theorem OAI.EditApproximation.materializedBandActionWithWork_value line 149

    Source documentation

    Materializing coordinates and vertices preserves the actual action label selected by the complete finite optimizer, including all ties.

    theorem materializedBandActionWithWork_value {M : ℕ} {σ : Type*} [DecidableEq σ]
    (band : List (Fin M → σ)) (hband : band ≠ []) (mass : Fin M → ℚ)
    (linear : Fin M × σ → ℚ) (G j : ℕ) :
    (materializedBandActionWithWork band mass linear G j).1.getD (band.head hband) =
      finiteOptimizerAction band hband mass linear G j := by
…

    Mentions: OAI.EditApproximation.materializedBandActionWithWork, OAI.EditApproximation.finiteOptimizerAction

  14. theorem OAI.EditApproximation.materializedBandActionWithWork_optimizer_cost line 207

    Source documentation

    Work of the optimizer after preparing its coordinate/vertex arrays. The finite preparation loops are charged separately.

    theorem materializedBandActionWithWork_optimizer_cost {M : ℕ} {σ : Type*} [DecidableEq σ]
    (band : List (Fin M → σ)) (mass : Fin M → ℚ)
    (linear : Fin M × σ → ℚ) (G j : ℕ) (hj : j ≤ G ^ 80) :
    (materializedBandActionWithWork band mass linear G j).2 ≤
      (band.length + 1) * ((bandCoordinates band.toFinset).card + 1) * (G + 2) ^ 210 := by
…

    Mentions: OAI.EditApproximation.materializedBandActionWithWork, OAI.EditApproximation.bandCoordinates