OAI/Combinatorics/UniformKServer/SideTracker.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.SideTracker.domain line 15
2. def OAI.UniformKServer.SideTracker.coordinate line 17
3. def OAI.UniformKServer.SideTracker.potential line 21
4. def OAI.UniformKServer.SideTracker.movement line 24
5. theorem OAI.UniformKServer.SideTracker.right_derivative_nonneg line 27

   Source comment

   CANDIDATE PROOFS

   theorem right_derivative_nonneg {f : ℝ → ℝ} {d δ : ℝ} (hδ : 0 < δ)
       (hf : HasDerivAt f d 0) (hmin : ∀ s, 0 < s → s < δ → f 0 ≤ f s) : 0 ≤ d := by
   …

6. theorem OAI.UniformKServer.SideTracker.domain_compact line 37
7. theorem OAI.UniformKServer.SideTracker.coordinate_continuous line 47
8. theorem OAI.UniformKServer.SideTracker.coordinate_deriv line 56
9. theorem OAI.UniformKServer.SideTracker.sum_update line 72
10. theorem OAI.UniformKServer.SideTracker.potential_update line 78
11. theorem OAI.UniformKServer.SideTracker.movement_update_le line 90
12. theorem OAI.UniformKServer.SideTracker.gradient_upper line 99
13. theorem OAI.UniformKServer.SideTracker.gradient_lower line 125
14. theorem OAI.UniformKServer.SideTracker.upper_violation line 151
15. theorem OAI.UniformKServer.SideTracker.lower_violation line 175
16. theorem OAI.UniformKServer.SideTracker.side_update line 198