Lean module · Foundations
BanditRLProof.Algorithms.MusicalChairsCoordinationTime
Quantitative continuation of the actual static coordination kernel. This module does not provide the exploration-good event or the full learner.
Module map
Imports
BanditRLProof.Algorithms.MusicalChairsCoordination
Imported by
BanditRLProof, BanditRLProof.Algorithms.MusicalChairsCollision, BanditRLProof.Algorithms.MusicalChairsCoordinationRegret, BanditRLProof.Algorithms.MusicalChairsExploration, BanditRLProof.Algorithms.MusicalChairsHandoff, BanditRLProof.Algorithms.MusicalChairsLearnerRegret, BanditRLProof.Algorithms.MusicalChairsMarginal, BanditRLProof.Algorithms.MusicalChairsPopulation, BanditRLProof.Algorithms.MusicalChairsRanking, BanditRLProof.Algorithms.MusicalChairsRealized, BanditRLProof.Algorithms.MusicalChairsReward
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.MusicalChairs.quarter_le_avoidance_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.quarter_le_avoidance_succReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem quarter_le_avoidance_succ (m : ℕ) (hm : 0 < m) : (1/4 : ℝ) ≤ ((m : ℝ) / ((m : ℝ)+1))^m
theorem
BanditRLProof.MusicalChairs.quarter_le_avoidance
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.quarter_le_avoidanceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem quarter_le_avoidance (n : ℕ) (hn : 2 ≤ n) : (1/4 : ℝ) ≤ (((n-1 : ℕ) : ℝ) / (n : ℝ))^(n-1)
theorem
BanditRLProof.MusicalChairs.real_uniform_hazard_lower
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.real_uniform_hazard_lowerReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem real_uniform_hazard_lower (n : ℕ) (hn : 0 < n) : (1 : ℝ) / (4 * n) ≤ (1 / (n : ℝ)) * (((n-1 : ℕ) : ℝ) / (n : ℝ))^(n-1)
theorem
BanditRLProof.MusicalChairs.uniform_hazard_lower
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.uniform_hazard_lowerReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem uniform_hazard_lower (n : ℕ) (hn : 0 < n) : (1 : ℝ≥0∞) / (4 * n) ≤ (1 / (n : ℝ≥0∞)) * (((n-1 : ℕ) : ℝ≥0∞) / (n : ℝ≥0∞))^(n-1)
theorem
BanditRLProof.MusicalChairs.transition_unfixed_hazard_quarter
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.transition_unfixed_hazard_quarterReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem transition_unfixed_hazard_quarter {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 : ℝ≥0∞) / (4 * n) ≤ (transition (fun _ : Fin n => S) (fun _ => hne) s).toOuterMeasure {s' | s' i ≠ none}
theorem
BanditRLProof.MusicalChairs.event_add_compl
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.event_add_complReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem event_add_compl {α : Type*} (p : PMF α) (E : Set α) : p.toOuterMeasure E + p.toOuterMeasure Eᶜ = 1
theorem
BanditRLProof.MusicalChairs.transition_fixed_no_return
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.transition_fixed_no_returnReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem transition_fixed_no_return {n k : ℕ} (candidates : Fin n → Finset (Fin k)) (hne : ∀ j, (candidates j).Nonempty) (s : State n k) (i : Fin n) (hi : s i ≠ none) : (transition candidates hne s).toOuterMeasure {s' | s' i = none} = 0
theorem
BanditRLProof.MusicalChairs.transition_unfixed_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.transition_unfixed_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem transition_unfixed_le {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (s : State n k) (i : Fin n) (hcard : S.card = n) : (transition (fun _ : Fin n => S) (fun _ => hne) s).toOuterMeasure {s' | s' i = none} ≤ if s i = none then 1 - (1 : ℝ≥0∞)/(4*n) else 0
theorem
BanditRLProof.MusicalChairs.unfixed_survival
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.unfixed_survivalReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem unfixed_survival {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (i : Fin n) (hcard : S.card = n) (t : ℕ) : (stateLaw (fun _ : Fin n => S) (fun _ => hne) t).toOuterMeasure {s | s i = none} ≤ (1 - (1 : ℝ≥0∞)/(4*n))^t
theorem
BanditRLProof.MusicalChairs.quarter_rate_le_one
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.quarter_rate_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem quarter_rate_le_one (n : ℕ) (hn : 0 < n) : (1 : ℝ≥0∞) / (4*n) ≤ 1
theorem
BanditRLProof.MusicalChairs.unfixed_survival_sum
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.unfixed_survival_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem unfixed_survival_sum {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (i : Fin n) (hcard : S.card = n) (T : ℕ) : ∑ t ∈ Finset.range T, (stateLaw (fun _ : Fin n => S) (fun _ => hne) t).toOuterMeasure {s | s i = none} ≤ 4*n
theorem
BanditRLProof.MusicalChairs.total_unfixed_occupation_le
Compiled
Expected total unfixed occupancy, expressed by actual finite-time marginals. The full pathwise regret adapter is a separate obligation.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.total_unfixed_occupation_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem total_unfixed_occupation_le {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (hcard : S.card = n) (T : ℕ) : ∑ t ∈ Finset.range T, ∑ i : Fin n, (stateLaw (fun _ : Fin n => S) (fun _ => hne) t).toOuterMeasure {s | s i = none} ≤ 4*(n : ℝ≥0∞)^2
def
BanditRLProof.MusicalChairs.unfixedCount
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.unfixedCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def unfixedCount {n k : ℕ} (s : State n k) : ℕ
theorem
BanditRLProof.MusicalChairs.unfixedCount_eq_sum
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.unfixedCount_eq_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem unfixedCount_eq_sum {n k : ℕ} (s : State n k) : (unfixedCount s : ℝ≥0∞) = ∑ i : Fin n, if s i = none then 1 else 0
theorem
BanditRLProof.MusicalChairs.expected_unfixed_eq_prob_sum
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.expected_unfixed_eq_prob_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_unfixed_eq_prob_sum {n k : ℕ} (p : PMF (State n k)) : ∑ s, p s * (unfixedCount s : ℝ≥0∞) = ∑ i : Fin n, p.toOuterMeasure {s | s i = none}
theorem
BanditRLProof.MusicalChairs.expected_unfixed_occupation_le
Compiled
Finite cumulative expected occupancy of the actual recursive state law. Counts are charged before each transition, including the initial all-unfixed state.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Multi-agent bandits
Canonical node identity
declaration:BanditRLProof.MusicalChairs.expected_unfixed_occupation_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_unfixed_occupation_le {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (hcard : S.card = n) (T : ℕ) : ∑ t ∈ Finset.range T, ∑ s, (stateLaw (fun _ : Fin n => S) (fun _ => hne) t) s * (unfixedCount s : ℝ≥0∞) ≤ 4*(n : ℝ≥0∞)^2