BanditRLProof.Algorithms.MusicalChairsCoordination

No declaration docstring is present; use the chapter context and exact statement below.

abbrev State (n k : ℕ)

No declaration docstring is present; use the chapter context and exact statement below.

def action {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (i : Fin n) : Fin k

No declaration docstring is present; use the chapter context and exact statement below.

def CollisionFree {n k : ℕ} (a : Fin n → Fin k) (i : Fin n) : Prop

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def step {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) : State n k

No declaration docstring is present; use the chapter context and exact statement below.

def DistinctFixed {n k : ℕ} (s : State n k) : Prop

No declaration docstring is present; use the chapter context and exact statement below.

theorem action_of_fixed {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (i : Fin n) (a : Fin k) (h : s i = some a) : action s draw i = a

No declaration docstring is present; use the chapter context and exact statement below.

theorem step_preserves_fixed {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (i : Fin n) (a : Fin k) (h : s i = some a) : step s draw i = some a

No declaration docstring is present; use the chapter context and exact statement below.

theorem step_fixed_action {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (i : Fin n) (a : Fin k) (h : step s draw i = some a) : action s draw i = a

No declaration docstring is present; use the chapter context and exact statement below.

theorem new_fixed_collisionFree {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (i : Fin n) (a : Fin k) (hn : s i = none) (h : step s draw i = some a) : CollisionFree (action s draw) i

No declaration docstring is present; use the chapter context and exact statement below.

theorem step_distinct {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (hs : DistinctFixed s) : DistinctFixed (step s draw)

No declaration docstring is present; use the chapter context and exact statement below.

def initial (n k : ℕ) : State n k

No declaration docstring is present; use the chapter context and exact statement below.

theorem initial_distinct (n k : ℕ) : DistinctFixed (initial n k)

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def trajectory {n k : ℕ} (draws : ℕ → Fin n → Fin k) : ℕ → State n k | 0 => initial n k | t+1 => step (trajectory draws t) (draws t) theorem trajectory_distinct {n k : ℕ} (draws : ℕ → Fin n → Fin k) (t : ℕ) : DistinctFixed (trajectory draws t)

No declaration docstring is present; use the chapter context and exact statement below.

theorem trajectory_distinct {n k : ℕ} (draws : ℕ → Fin n → Fin k) (t : ℕ) : DistinctFixed (trajectory draws t)

The action of player i uses only its own fixed arm and its own private draw.

theorem action_local {n k : ℕ} (s s' : State n k) (draw draw' : Fin n → Fin k) (i : Fin n) (hs : s i = s' i) (hd : draw i = draw' i) : action s draw i = action s' draw' i

Uniform law on the finite Cartesian product of local candidate sets.

noncomputable def jointDraw {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) : PMF (Fin n → Fin k)

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def transition {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) (s : State n k) : PMF (State n k)

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def stateLaw {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) : ℕ → PMF (State n k) | 0 => PMF.pure (initial n k) | t+1 => (stateLaw candidates hne t).bind (transition candidates hne) theorem transition_distinct {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) (s s' : State n k) (hs : DistinctFixed s) (h : s' ∈ (transition candidates hne s).support) : DistinctFixed s'

No declaration docstring is present; use the chapter context and exact statement below.

theorem transition_distinct {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) (s s' : State n k) (hs : DistinctFixed s) (h : s' ∈ (transition candidates hne s).support) : DistinctFixed s'

No declaration docstring is present; use the chapter context and exact statement below.

theorem stateLaw_distinct {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) (t : ℕ) (s : State n k) (h : s ∈ (stateLaw candidates hne t).support) : DistinctFixed s

A player's update consumes only its own old state, action, and collision bit.

def localUpdate {k : ℕ} (old : Option (Fin k)) (played : Fin k) (collided : Bool) : Option (Fin k)

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def collisionBit {n k : ℕ} (a : Fin n → Fin k) (i : Fin n) : Bool

No declaration docstring is present; use the chapter context and exact statement below.

theorem step_localUpdate {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (i : Fin n) : step s draw i = localUpdate (s i) (action s draw i) (collisionBit (action s draw) i)

No declaration docstring is present; use the chapter context and exact statement below.

theorem jointDraw_mem {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) (draw : Fin n → Fin k) (h : draw ∈ (jointDraw candidates hne).support) (i : Fin n) : draw i ∈ candidates i

No declaration docstring is present; use the chapter context and exact statement below.

def FixedWithin {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (s : State n k) : Prop

No declaration docstring is present; use the chapter context and exact statement below.

theorem step_within {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (s : State n k) (draw : Fin n → Fin k) (hs : FixedWithin candidates s) (hd : ∀ i, draw i ∈ candidates i) : FixedWithin candidates (step s draw)

No declaration docstring is present; use the chapter context and exact statement below.

theorem stateLaw_within {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) (t : ℕ) (s : State n k) (h : s ∈ (stateLaw candidates hne t).support) : FixedWithin candidates s

Exact rectangular-event law, including empty restrictions.

theorem jointDraw_rectangle {n k : ℕ} (candidates allowed : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) : (jointDraw candidates hne).toOuterMeasure {draw | ∀ i, draw i ∈ allowed i} = (∏ i, ((candidates i ∩ allowed i).card : ℝ≥0∞)) / (∏ i, ((candidates i).card : ℝ≥0∞))

Rectangle probabilities factor into their coordinate counting ratios.

theorem jointDraw_rectangle_product {n k : ℕ} (candidates allowed : Fin n → Finset (Fin k)) (hne : ∀ i, (candidates i).Nonempty) : (jointDraw candidates hne).toOuterMeasure {draw | ∀ i, draw i ∈ allowed i} = ∏ i, ((candidates i ∩ allowed i).card : ℝ≥0∞) / ((candidates i).card : ℝ≥0∞)

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def fixationWindow {n k : ℕ} (s : State n k) (i : Fin n) (a : Fin k) (j : Fin n) : Finset (Fin k)

No declaration docstring is present; use the chapter context and exact statement below.

theorem fixationWindow_fixes {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (i : Fin n) (a : Fin k) (hi : s i = none) (ha : ∀ j b, s j = some b → b ≠ a) (hd : ∀ j, draw j ∈ fixationWindow s i a j) : step s draw i = some a

A genuine lower bound on the constructed next-state law, obtained from one explicit collision-free draw event. Candidate sets may differ.

theorem transition_fixation_lower {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ j, (candidates j).Nonempty) (s : State n k) (i : Fin n) (a : Fin k) (hi : s i = none) (ha : ∀ j b, s j = some b → b ≠ a) : (∏ j, ((candidates j ∩ fixationWindow s i a j).card : ℝ≥0∞) / ((candidates j).card : ℝ≥0∞)) ≤ (transition candidates hne s).toOuterMeasure {s' | s' i = some a}

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def isolationWindow {n k : ℕ} (i : Fin n) (a : Fin k) (j : Fin n) : Finset (Fin k)

No declaration docstring is present; use the chapter context and exact statement below.

theorem isolationWindow_subset {n k : ℕ} (s : State n k) (i : Fin n) (a : Fin k) (j : Fin n) : isolationWindow i a j ⊆ fixationWindow s i a j

Exact probability of a tagged draw and avoidance by every other private coin.

theorem jointDraw_isolation {n k : ℕ} (S : Finset (Fin k)) (i : Fin n) (a : Fin k) (ha : a ∈ S) (hcard : S.card = n) : (jointDraw (fun _ : Fin n => S) (fun _ => ⟨a, ha⟩)).toOuterMeasure {draw | ∀ j, draw j ∈ isolationWindow i a j} = (1 / (n : ℝ≥0∞)) * (((n-1 : ℕ) : ℝ≥0∞) / (n : ℝ≥0∞))^(n-1)

Statewise fixation hazard from the actual joint law on a common N-arm set. Existence of an unused arm and the numerical 1/(4N) bound are separate obligations.

theorem transition_common_fixation_lower {n k : ℕ} (S : Finset (Fin k)) (s : State n k) (i : Fin n) (a : Fin k) (hmem : a ∈ S) (hcard : S.card = n) (hi : s i = none) (ha : ∀ j b, s j = some b → b ≠ a) : (1 / (n : ℝ≥0∞)) * (((n-1 : ℕ) : ℝ≥0∞) / (n : ℝ≥0∞))^(n-1) ≤ (transition (fun _ : Fin n => S) (fun _ => ⟨a, hmem⟩) s).toOuterMeasure {s' | s' i = some a}

One unfixed player leaves at most N-1 occupied labels, so an N-label set contains an unused label. No successful coordination is assumed.

theorem exists_unoccupied {n k : ℕ} (S : Finset (Fin k)) (s : State n k) (i : Fin n) (hi : s i = none) (hcard : S.card = n) : ∃ a ∈ S, ∀ j b, s j = some b → b ≠ a

A statewise hazard for every unfixed player, produced without an externally supplied unused arm, settling event, or hazard premise.

theorem transition_unfixed_hazard {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (s : State n k) (i : Fin n) (hi : s i = none) (hcard : S.card = n) : (1 / (n : ℝ≥0∞)) * (((n-1 : ℕ) : ℝ≥0∞) / (n : ℝ≥0∞))^(n-1) ≤ (transition (fun _ : Fin n => S) (fun _ => hne) s).toOuterMeasure {s' | s' i ≠ none}