OAI/Combinatorics/UniformKServer/ExactOptimum.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.EffectiveLP.labels_inhabited line 10
2. def OAI.UniformKServer.EffectiveLP.chosen line 17
3. def OAI.UniformKServer.EffectiveLP.lazyRun line 20
4. theorem OAI.UniformKServer.EffectiveLP.lazyRun_nil line 23
5. theorem OAI.UniformKServer.EffectiveLP.lazyRun_append line 25
6. def OAI.UniformKServer.EffectiveLP.pureFlow line 29
7. theorem OAI.UniformKServer.EffectiveLP.pure_nonneg line 33
8. theorem OAI.UniformKServer.EffectiveLP.pure_total line 40
9. theorem OAI.UniformKServer.EffectiveLP.pure_outflow line 45
10. theorem OAI.UniformKServer.EffectiveLP.pure_inflow line 50
11. theorem OAI.UniformKServer.EffectiveLP.history_nonneg line 75
12. theorem OAI.UniformKServer.EffectiveLP.opt_nonneg line 81
13. theorem OAI.UniformKServer.EffectiveLP.zero_history_covered line 88
14. theorem OAI.UniformKServer.EffectiveLP.zero_opt_covered line 112
15. theorem OAI.UniformKServer.EffectiveLP.chosen_hit line 119
16. theorem OAI.UniformKServer.EffectiveLP.step_hit line 125
17. theorem OAI.UniformKServer.EffectiveLP.lazyRun_covered line 133
18. def OAI.UniformKServer.EffectiveLP.pureCost line 143
19. theorem OAI.UniformKServer.EffectiveLP.pureCost_nonneg line 147
20. theorem OAI.UniformKServer.EffectiveLP.pureCost_zero line 153
21. theorem OAI.UniformKServer.EffectiveLP.pure_cost_eq line 165
22. def OAI.UniformKServer.EffectiveLP.crudeCoefficient line 176
23. theorem OAI.UniformKServer.EffectiveLP.crude_nonneg line 179
24. theorem OAI.UniformKServer.EffectiveLP.crude_competitive line 184
25. theorem OAI.UniformKServer.EffectiveLP.pure_valid line 193
26. theorem OAI.UniformKServer.EffectiveLP.unconditional_optimization line 205

    Source documentation

    Unconditional termination, feasibility and exact rational optimality.

    theorem unconditional_optimization {n k H : ℕ} [NeZero k]
        (d : RationalMetric n) (u : Config n k) :
        ∃ x : Fin (Fintype.card (Variable n k H)+1) → ℚ,
          FourierMotzkin.optimize (Fintype.card (Variable n k H)) (constraints d u) = some x ∧
          Valid d u (ofAssignment (Form.recover x)) (FourierMotzkin.objective x) ∧
          ∀ (F : BoundedFlow n k H ℝ) (a : ℝ), Valid d u F a →
            ((FourierMotzkin.objective x : ℚ) : ℝ) ≤ a := by
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.EffectiveLP.Config, OAI.UniformKServer.EffectiveLP.Variable, OAI.UniformKServer.FourierMotzkin.optimize, OAI.UniformKServer.EffectiveLP.constraints, OAI.UniformKServer.EffectiveLP.Valid, OAI.UniformKServer.EffectiveLP.ofAssignment, OAI.UniformKServer.EffectiveLP.Form.recover, OAI.UniformKServer.FourierMotzkin.objective, OAI.UniformKServer.EffectiveLP.BoundedFlow