ComputedSuffix.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.UniformKServer.ComputedSuffix.Tape line 10
def OAI.UniformKServer.ComputedSuffix.epochTrace line 13
def OAI.UniformKServer.ComputedSuffix.expected line 20
Source documentation
Independent unbiased tapes are sampled at consecutive epochs. The actual entering configuration is retained as random state, never reset to u.
```
noncomputable def expected {n k : ℕ} [NeZero k] (d : RationalMetric n) (u : Config n k)
    (M : ℕ) : Configuration n k → List (List (Fin n)) → ℝ
  | _, [] => 0
  | s, raw::es => BitSampling.mean (fun coins : Tape M (horizon k M) u.val raw =>
      let g := epochTrace d u M raw coins
…
```
Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration, OAI.UniformKServer.BitSampling.mean, OAI.UniformKServer.ComputedSuffix.Tape, OAI.UniformKServer.horizon, OAI.UniformKServer.ComputedSuffix.epochTrace
theorem OAI.UniformKServer.ComputedSuffix.epoch_sum line 27

theorem OAI.UniformKServer.ComputedSuffix.suffix line 70

Source documentation

Complete unbounded-suffix comparison for the actually computed policy. The sharp logarithmic estimate on its coefficient is still the companion existence obligation, not an assumption or a conclusion of this theorem.

theorem suffix {n k : ℕ} [NeZero k] (hk2 : 2 ≤ k)
    (d : RationalMetric n) (u : Config n k) (M R : ℕ) (hR : 0 < R) (D δ : ℝ)
    (hD : 0 ≤ D) (hδ : 0 ≤ δ) (hdiam : ∀ x y, (d.distance x y : ℝ) ≤ D)
    (hsep : ∀ x y, x ≠ y → δ ≤ (d.distance x y : ℝ))
    (hcap : R * (k+1) * D ≤ (M+1) * δ) (hRD : k*D ≤ R*δ)
    (pre w : List (Fin n)) (original actual : Configuration n k) :
    expected d u M actual (epochs k R hR w) ≤
      (4*(AutomaticTable.coefficient d u (horizon k M) : ℝ)+2)*
        offlineCost d original (pre++w) +
      (2*(AutomaticTable.coefficient d u (horizon k M) : ℝ)+2)*k*D := by
…

Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration, OAI.UniformKServer.ComputedSuffix.expected, OAI.UniformKServer.AutomaticTable.coefficient, OAI.UniformKServer.horizon, OAI.UniformKServer.offlineCost