BoundedFilter.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniformKServer.finish line 8
Source documentation
Final labeled positions after the specified legal one-label service.
```
def finish {n k : ℕ} : Configuration n k → History n k → Configuration n k
  | s, [] => s
  | s, (r,j) :: h => finish (serve s r j) h

/-- Same-label mismatch, not a minimum matching; repetitions are allowed. -/
```
Mentions: OAI.UniformKServer.Configuration, OAI.UniformKServer.History, OAI.UniformKServer.serve, OAI.UniformKServer.mismatch
def OAI.UniformKServer.mismatch line 13
Source documentation
Same-label mismatch, not a minimum matching; repetitions are allowed.
```
def mismatch {n k : ℕ} (d : RationalMetric n) (u s : Configuration n k) : ℝ :=
…
```
Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration
theorem OAI.UniformKServer.distance_nonneg line 16
theorem OAI.UniformKServer.distance_triangle line 19
theorem OAI.UniformKServer.distance_self line 23
theorem OAI.UniformKServer.mismatch_nonneg line 27
theorem OAI.UniformKServer.mismatch_le_diameter line 31
theorem OAI.UniformKServer.mismatch_skip line 38
theorem OAI.UniformKServer.mismatch_keep line 56
theorem OAI.UniformKServer.sublist_potential line 78
Source documentation
Skipped virtual visits are paid by triangle inequality; retained visits synchronize the relevant actual and virtual labels.
```
theorem sublist_potential {n k : ℕ} (d : RationalMetric n)
    {g h : History n k} (hsub : g.Sublist h) (u s : Configuration n k) :
    costAlong d u g + mismatch d (finish u g) (finish s h) ≤
      costAlong d s h + mismatch d u s := by
…
```
Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.History, OAI.UniformKServer.Configuration, OAI.UniformKServer.costAlong, OAI.UniformKServer.mismatch, OAI.UniformKServer.finish
theorem OAI.UniformKServer.costAlong_nonneg line 97
theorem OAI.UniformKServer.offlineCost_le_history line 107
Source documentation
The infimum definition of OPT is bounded below even before selecting a minimizer. Every explicit legal label history gives an upper bound.
```
theorem offlineCost_le_history {n k : ℕ} (d : RationalMetric n)
    (s : Configuration n k) (h : History n k) :
    offlineCost d s (h.map Prod.fst) ≤ costAlong d s h := by
…
```
Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration, OAI.UniformKServer.History, OAI.UniformKServer.offlineCost, OAI.UniformKServer.costAlong

theorem OAI.subsequence_cost_transfer line 120

Source documentation

Exact pathwise transfer needed at every restart and for deleting requests. Source: Section 03, equations actual-virtual and subsequence-comparison.

theorem subsequence_cost_transfer {n k : ℕ} (d : UniformKServer.RationalMetric n)
    (u s : UniformKServer.Configuration n k) (g h : UniformKServer.History n k)
    (hsub : g.Sublist h) (D : ℝ)
    (hdiam : ∀ x y, (d.distance x y : ℝ) ≤ D) :
    UniformKServer.costAlong d u g +
      UniformKServer.mismatch d (UniformKServer.finish u g) (UniformKServer.finish s h) ≤
      UniformKServer.costAlong d s h + UniformKServer.mismatch d u s ∧
    UniformKServer.costAlong d u g ≤ UniformKServer.costAlong d s h + k * D ∧
    UniformKServer.offlineCost d u (g.map Prod.fst) ≤
      UniformKServer.costAlong d s h + k * D := by
…

Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration, OAI.UniformKServer.History, OAI.UniformKServer.costAlong, OAI.UniformKServer.mismatch, OAI.UniformKServer.finish, OAI.UniformKServer.offlineCost