OAI/Combinatorics/UniformKServer/SimplexTracker.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.SimplexTracker.simplex line 10
2. def OAI.UniformKServer.SimplexTracker.movement line 12
3. def OAI.UniformKServer.SimplexTracker.transfer line 14
4. def OAI.UniformKServer.SimplexTracker.objective line 17
5. structure OAI.UniformKServer.SimplexTracker.AnalyticData line 20
6. theorem OAI.UniformKServer.SimplexTracker.coordinate_le_one line 40
7. theorem OAI.UniformKServer.SimplexTracker.simplex_compact line 45
8. theorem OAI.UniformKServer.SimplexTracker.sum_update line 54
9. theorem OAI.UniformKServer.SimplexTracker.potential_update line 59
10. theorem OAI.UniformKServer.SimplexTracker.transfer_simplex line 69
11. theorem OAI.UniformKServer.SimplexTracker.transfer_potential line 81
12. theorem OAI.UniformKServer.SimplexTracker.transfer_movement line 87
13. theorem OAI.UniformKServer.SimplexTracker.scalar_deficit line 98
14. theorem OAI.UniformKServer.SimplexTracker.multiplier_pos line 109
15. theorem OAI.UniformKServer.SimplexTracker.weighted_deficit line 116
16. theorem OAI.UniformKServer.SimplexTracker.low_coordinate line 158
17. theorem OAI.UniformKServer.SimplexTracker.minimizing_slope line 197
18. theorem OAI.UniformKServer.SimplexTracker.right_derivative_nonneg line 212
19. theorem OAI.UniformKServer.SimplexTracker.minimum_gradient_difference line 221
20. theorem OAI.UniformKServer.SimplexTracker.minimum_excludes_singular line 245
21. theorem OAI.UniformKServer.SimplexTracker.minimum_feasible line 270
22. theorem OAI.UniformKServer.SimplexTracker.update line 298

    Source documentation

    Compact minimizing update, with no convexity assumption on the primitives.

    theorem update (g : ι → ℝ → ℝ) (B h : ι → ℝ)
        (F : ι → ℝ → ℝ) (ell ct C A E : ℝ)
        (H : AnalyticData g B h F ell ct C A E) (a₀ : ι → ℝ) (ha₀ : simplex a₀) :
        ∃ a, simplex a ∧ IsMinOn (objective g (∑ i, B i) a₀) {a | simplex a} a ∧
          (∀ i, (∑ r, B r)*a i ≤ (1+ct*h i/ell)*B i) ∧
          (∑ i, B i)*movement a a₀ ≤ (∑ i, g i (a₀ i))-(∑ i, g i (a i)) := by
    …

    Mentions: OAI.UniformKServer.SimplexTracker.AnalyticData, OAI.UniformKServer.SimplexTracker.simplex, OAI.UniformKServer.SimplexTracker.objective, OAI.UniformKServer.SimplexTracker.movement