OAI/Combinatorics/UniformKServer/FourierMotzkin.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniformKServer.FourierMotzkin.Row line 7
  2. def OAI.UniformKServer.FourierMotzkin.Row.eval line 14
  3. def OAI.UniformKServer.FourierMotzkin.Row.tail line 17
  4. def OAI.UniformKServer.FourierMotzkin.Row.scale line 20
  5. def OAI.UniformKServer.FourierMotzkin.Row.sub line 23
  6. def OAI.UniformKServer.FourierMotzkin.Row.bound line 26
  7. theorem OAI.UniformKServer.FourierMotzkin.Row.eval_scale line 32
  8. theorem OAI.UniformKServer.FourierMotzkin.Row.eval_sub line 40
  9. theorem OAI.UniformKServer.FourierMotzkin.Row.eval_cons line 46
  10. theorem OAI.UniformKServer.FourierMotzkin.Row.eval_bound line 51
  11. theorem OAI.UniformKServer.FourierMotzkin.Row.eval_rat_cast line 58
  12. theorem OAI.UniformKServer.FourierMotzkin.Row.negative_iff line 64
  13. theorem OAI.UniformKServer.FourierMotzkin.Row.positive_iff line 71
  14. theorem OAI.UniformKServer.FourierMotzkin.Row.zero_iff line 79
  15. def OAI.UniformKServer.FourierMotzkin.lower line 86
  16. def OAI.UniformKServer.FourierMotzkin.upper line 89
  17. def OAI.UniformKServer.FourierMotzkin.independent line 92
  18. def OAI.UniformKServer.FourierMotzkin.project line 95
  19. def OAI.UniformKServer.FourierMotzkin.Satisfies line 98
  20. theorem OAI.UniformKServer.FourierMotzkin.satisfies_cons_iff line 104
  21. theorem OAI.UniformKServer.FourierMotzkin.satisfies_project_iff line 138
  22. theorem OAI.UniformKServer.FourierMotzkin.project_of_satisfies line 157
  23. def OAI.UniformKServer.FourierMotzkin.high line 166
  24. def OAI.UniformKServer.FourierMotzkin.low line 168
  25. theorem OAI.UniformKServer.FourierMotzkin.high_le_iff line 170
  26. theorem OAI.UniformKServer.FourierMotzkin.le_low_iff line 181
  27. def OAI.UniformKServer.FourierMotzkin.intervalPivot line 192
  28. def OAI.UniformKServer.FourierMotzkin.pivot line 201

    Source documentation

    Reversing one elimination. With no lower bound choose the least upper bound; with no bounds choose zero, exactly as in the source.

    def pivot {n : ℕ} {K : Type*} [Field K] [LinearOrder K]
    (R : List (Row (n+1))) (x : Fin n → K) : K :=
…

    Mentions: OAI.UniformKServer.FourierMotzkin.Row

  29. theorem OAI.UniformKServer.FourierMotzkin.pivot_bounds line 206
  30. theorem OAI.UniformKServer.FourierMotzkin.satisfies_pivot line 225
  31. theorem OAI.UniformKServer.FourierMotzkin.project_iff_exists line 243

    Source documentation

    Exact existential projection over either ℚ or ℝ; no strict-inequality relaxation and no compactness or attainment assumption.

     theorem project_iff_exists {n : ℕ} {K : Type*}
    [Field K] [LinearOrder K] [IsStrictOrderedRing K]
    (R : List (Row (n+1))) (x : Fin n → K) :
    Satisfies (project R) x ↔ ∃ z, Satisfies R (Fin.cons z x) := by
…

    Mentions: OAI.UniformKServer.FourierMotzkin.Row, OAI.UniformKServer.FourierMotzkin.Satisfies, OAI.UniformKServer.FourierMotzkin.project

  32. def OAI.UniformKServer.FourierMotzkin.objective line 254

    Source documentation

    The objective is the final coordinate, retained through every projection.

    def objective {n : ℕ} {K : Type*} (x : Fin (n+1) → K) : K := x (Fin.last n)
  33. def OAI.UniformKServer.FourierMotzkin.baseValue line 256
  34. def OAI.UniformKServer.FourierMotzkin.optimize line 261

    Source documentation

    Exact rational arithmetic and comparisons only. The nonnegative objective constraint is imposed by the base case even if not listed among the rows.

    def optimize : (n : ℕ) → List (Row (n+1)) → Option (Fin (n+1) → ℚ)
  | 0, R =>
    let x := Fin.cons (baseValue R) Fin.elim0
…

    Mentions: OAI.UniformKServer.FourierMotzkin.Row, OAI.UniformKServer.FourierMotzkin.baseValue

  35. theorem OAI.UniformKServer.FourierMotzkin.high_rat_cast line 267
  36. theorem OAI.UniformKServer.FourierMotzkin.eval_empty line 273
  37. theorem OAI.UniformKServer.FourierMotzkin.one_cons line 276
  38. theorem OAI.UniformKServer.FourierMotzkin.baseValue_nonneg line 282
  39. theorem OAI.UniformKServer.FourierMotzkin.baseValue_minimal line 285
  40. theorem OAI.UniformKServer.FourierMotzkin.baseValue_feasible line 296
  41. theorem OAI.UniformKServer.FourierMotzkin.objective_cons line 316
  42. theorem OAI.UniformKServer.FourierMotzkin.objective_tail line 319
  43. theorem OAI.UniformKServer.FourierMotzkin.optimize_rational_attainment line 325

    Source documentation

    The exact finite rational optimizer succeeds whenever the rational rows have a real feasible point with nonnegative objective; its rational output is feasible and minimizes the objective against every such real point.

    theorem optimize_rational_attainment (n : ℕ) (R : List (Row (n+1)))
    (H : ∃ y : Fin (n+1) → ℝ, 0 ≤ objective y ∧ Satisfies R y) :
    ∃ x : Fin (n+1) → ℚ, optimize n R = some x ∧
      0 ≤ objective x ∧ Satisfies R x ∧
      ∀ y : Fin (n+1) → ℝ, 0 ≤ objective y → Satisfies R y →
        ((objective x : ℚ) : ℝ) ≤ objective y := by
…

    Mentions: OAI.UniformKServer.FourierMotzkin.Row, OAI.UniformKServer.FourierMotzkin.objective, OAI.UniformKServer.FourierMotzkin.Satisfies, OAI.UniformKServer.FourierMotzkin.optimize