OAI/Combinatorics/UniformKServer/ComputedInstance.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.ComputedInstance.allDistances line 12
2. def OAI.UniformKServer.ComputedInstance.positiveDistances line 15
3. theorem OAI.UniformKServer.ComputedInstance.allDistances_nonempty line 18
4. theorem OAI.UniformKServer.ComputedInstance.positiveDistances_nonempty line 23
5. def OAI.UniformKServer.ComputedInstance.diameter line 33
6. def OAI.UniformKServer.ComputedInstance.separation line 36
7. def OAI.UniformKServer.ComputedInstance.canonical line 39
8. def OAI.UniformKServer.ComputedInstance.restart line 42
9. def OAI.UniformKServer.ComputedInstance.cap line 45
10. theorem OAI.UniformKServer.ComputedInstance.parameters line 49

    Source documentation

    Exact instance parameters and canonical start in the manuscript.

    theorem parameters (hn : 2 ≤ n) (hk : 0 < k) (d : RationalMetric n) :
        0 ≤ (diameter hn d : ℝ) ∧ 0 < (separation hn d : ℝ) ∧
        (∀ x y, (d.distance x y : ℝ) ≤ diameter hn d) ∧
        (∀ x y, x ≠ y → (separation hn d : ℝ) ≤ d.distance x y) ∧
        0 < restart hn d k ∧
        (k:ℝ)*diameter hn d ≤ (restart hn d k : ℝ)*separation hn d ∧
        (restart hn d k : ℝ)*(k+1)*diameter hn d ≤
          ((cap hn d k : ℝ)+1)*separation hn d := by
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.ComputedInstance.diameter, OAI.UniformKServer.ComputedInstance.separation, OAI.UniformKServer.ComputedInstance.restart, OAI.UniformKServer.ComputedInstance.cap

11. def OAI.UniformKServer.ComputedInstance.prefixTrace line 99

    Source documentation

    Prefix requests before deterministic activation use source label 1 (zero in Fin k); the raw suffix then uses the computed exact-bit epochs.

    def prefixTrace [NeZero k] (w : List (Fin n)) : History n k :=
    …

    Mentions: OAI.UniformKServer.History

12. def OAI.UniformKServer.ComputedInstance.expected line 102
13. def OAI.UniformKServer.ComputedInstance.coefficient line 112
14. theorem OAI.UniformKServer.ComputedInstance.full_movement line 117

    Source documentation

    The source full-movement estimate with the actually computed coefficient; no unknown existence result or competitive coefficient is supplied as input.

    theorem full_movement [NeZero k] (hn : 2 ≤ n) (hk : 2 ≤ k) (hkn : k ≤ n)
        (d : RationalMetric n) (s : Configuration n k) (activation : ℕ)
        (w : List (Fin n)) :
        expected hn (by omega) hkn d s activation w ≤
          (4*(coefficient hn hkn d : ℝ)+2)*offlineCost d s w +
          (activation-1 : ℕ)*(diameter hn d : ℝ) +
          (2*(coefficient hn hkn d : ℝ)+2)*k*(diameter hn d : ℝ) := by
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration, OAI.UniformKServer.ComputedInstance.expected, OAI.UniformKServer.ComputedInstance.coefficient, OAI.UniformKServer.offlineCost, OAI.UniformKServer.ComputedInstance.diameter