Proof of Lemma 13, first case — the unvisited transition region contains the simplex

Proved

NonstatRL.NoWidening.unvisited_region_is_simplex

by mikedeng1 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

confidence-regionmdpnon-stationaryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Fix a finite state space with at least two states, nonempty allowed action sets, a horizon $T\ge1$ , and $0<\delta<1$ . For an allowed state-action pair $(s,a)$ with no visits in the chosen window, the transition radius satisfies

\operatorname{rad}_p(s,a)\ge1,

and every probability distribution on the states belongs to the unwidened confidence region $H_p(s,a;0)$ .

This is the first case in the authors' construction of a transition model inside the region.

Formalization Note A zero count gives $N^+=1$ and empirical center $\hat p=0$ . The hypotheses $S>1$ and $0<\delta<1$ are explicit pins needed for the printed radius claim. The window uses zero-based half-open indices.

Preamble

import Mathlib
import Definitions.Def_NonstatRL_PerStep_Window

open BanditAlgorithm

Formal statement

namespace NonstatRL.NoWidening

theorem unvisited_region_is_simplex {S A : ℕ} (hS : 1 < S)
    (As : Fin S → Finset (Fin A)) (hAs : ∀ s, (As s).Nonempty)
    (T : ℕ) (hT : 1 ≤ T) (δ : ℝ) (hδ : 0 < δ ∧ δ < 1)
    (st : ℕ → Fin S) (ac : ℕ → Fin A) (lo hi : ℕ)
    (s : Fin S) (a : Fin A) (ha : a ∈ As s)
    (hzero : NonstatRL.PerStep.count st ac lo hi s a = 0) :
    1 ≤ NonstatRL.PerStep.radP As T δ (NonstatRL.PerStep.countPlus st ac lo hi s a) ∧
      ∀ p : Fin S → ℝ, (∀ s', 0 ≤ p s') → (∑ s', p s') = 1 →
        p ∈ NonstatRL.PerStep.Hp As T δ st ac lo hi 0 s a := by sorry

end NonstatRL.NoWidening

Source

Cheung, Simchi-Levi & Zhu, Non-Stationary Reinforcement Learning: The Blessing of (More) Optimism, arXiv:1906.02922v4, p. 50, proof of Lemma 13, first case

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph