AdaptiveLedger.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Finite adaptive all-step accounting. This is the filtering telescope used twice in the allocation proof (primitive trackers and output-rule switching). No martingale assertion is conditioned on the later event being charged.

def OAI.UniformKServer.AdaptiveLedger.expect line 17
def OAI.UniformKServer.AdaptiveLedger.linear line 19
def OAI.UniformKServer.AdaptiveLedger.post line 21
def OAI.UniformKServer.AdaptiveLedger.increment line 24
def OAI.UniformKServer.AdaptiveLedger.drift line 27
theorem OAI.UniformKServer.AdaptiveLedger.expect_add line 30
theorem OAI.UniformKServer.AdaptiveLedger.expect_sub line 34
theorem OAI.UniformKServer.AdaptiveLedger.expect_const line 38
theorem OAI.UniformKServer.AdaptiveLedger.expect_mono line 41
theorem OAI.UniformKServer.AdaptiveLedger.filtering_zero line 47
Source documentation
Expected filtering vanishes for old-history coefficients even if the subsequent domains, stopping events and output rules are chosen adaptively.
```
theorem filtering_zero {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω) (F G : Setoid Ω)
    (hGF : ∀ ω v, G.r ω v → F.r ω v) (a X : Ω → ι → ℝ)
    (ha : ∀ i, measurable F (fun ω => a ω i)) :
    expect w (increment w F G a X)=0 := by
…
```
Mentions: OAI.UniformKServer.AdaptiveLedger.expect, OAI.UniformKServer.AdaptiveLedger.increment
theorem OAI.UniformKServer.AdaptiveLedger.drift_bound line 59
Source documentation
Hidden drift is evaluated at the new information, while old coefficient bounds alone suffice. The L1 contraction has coefficient one.
```
theorem drift_bound {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω) (F : Setoid Ω)
    (a X Y : Ω → ι → ℝ) {C : ℝ} (hC : 0 ≤ C) (ha : ∀ ω i, |a ω i| ≤ C) :
    expect w (drift w F a X Y) ≤ C*expect w (fun ω => ∑ i, |Y ω i-X ω i|) := by
…
```
Mentions: OAI.UniformKServer.AdaptiveLedger.expect, OAI.UniformKServer.AdaptiveLedger.drift

theorem OAI.UniformKServer.AdaptiveLedger.telescope line 87

Source documentation

Generic ledger with genuine filtering increments and hidden L1 drift. One-step inequalities are deterministic algorithmic obligations, not a substitute for an assumed competitive bound. The conclusion sums all steps.

theorem telescope {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω)
    (F : ℕ → Setoid Ω) (hF : ∀ t ω v, (F (t+1)).r ω v → (F t).r ω v)
    (a X : ℕ → Ω → ι → ℝ) (P M Q : ℕ → Ω → ℝ) {C : ℝ}
    (hC : 0 ≤ C) (ha : ∀ t ω i, |a t ω i| ≤ C)
    (hmeas : ∀ t i, measurable (F t) (fun ω => a t ω i))
    (hstep : ∀ t ω, M t ω ≤ P t ω-P (t+1) ω+
      increment w (F t) (F (t+1)) (a t) (X t) ω+
      drift w (F (t+1)) (a t) (X t) (X (t+1)) ω+Q t ω) (H : ℕ) :
    (∑ t ∈ range H, expect w (M t)) ≤ expect w (P 0)-expect w (P H)+
      C*(∑ t ∈ range H, expect w (fun ω => ∑ i, |X (t+1) ω i-X t ω i|))+
      ∑ t ∈ range H, expect w (Q t) := by
…

Mentions: OAI.UniformKServer.AdaptiveLedger.increment, OAI.UniformKServer.AdaptiveLedger.drift, OAI.UniformKServer.AdaptiveLedger.expect