BanditRLProof.Algorithms.MusicalChairsCoordinationRegret

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

noncomputable def fixedPlayers {n k : ℕ} (s : State n k) : Finset (Fin n)

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

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

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

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

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

theorem fixed_action_injective {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (hs : DistinctFixed s) : Set.InjOn (action s draw) (fixedPlayers s)

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

theorem hitFixed_partner {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (hs : DistinctFixed s) (i : Fin n) (hi : i ∈ hitFixed s draw) : ∃ j, s j = none ∧ action s draw j = action s draw i

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

theorem hitFixed_card_le {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (hs : DistinctFixed s) : (hitFixed s draw).card ≤ unfixedCount s

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

theorem safeFixed_count {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (hs : DistinctFixed s) : n ≤ (safeFixed s draw).card + 2 * unfixedCount s

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

noncomputable def roundMeanReward {n k : ℕ} (mu : Fin k → ℝ) (s : State n k) (draw : Fin n → Fin k) : ℝ

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

noncomputable def roundPseudoRegret {n k : ℕ} (S : Finset (Fin k)) (mu : Fin k → ℝ) (s : State n k) (draw : Fin n → Fin k) : ℝ

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

theorem safeFixed_mem {n k : ℕ} (s : State n k) (draw : Fin n → Fin k) (i : Fin n) (hi : i ∈ safeFixed s draw) : i ∈ fixedPlayers s ∧ CollisionFree (action s draw) i

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

theorem safeFixed_arms_subset {n k : ℕ} (S : Finset (Fin k)) (s : State n k) (draw : Fin n → Fin k) (hw : FixedWithin (fun _ => S) s) : (safeFixed s draw).image (action s draw) ⊆ S

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

theorem safeFixed_reward_le {n k : ℕ} (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a) (s : State n k) (draw : Fin n → Fin k) (hs : DistinctFixed s) : ∑ a ∈ (safeFixed s draw).image (action s draw), mu a ≤ roundMeanReward mu s draw

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

theorem roundPseudoRegret_le_twice_unfixed {n k : ℕ} (S : Finset (Fin k)) (hcard : S.card = n) (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (s : State n k) (draw : Fin n → Fin k) (hs : DistinctFixed s) (hw : FixedWithin (fun _ => S) s) : roundPseudoRegret S mu s draw ≤ 2 * (unfixedCount s : ℝ)

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

theorem roundPseudoRegret_nonneg {n k : ℕ} (S : Finset (Fin k)) (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a) (s : State n k) (draw : Fin n → Fin k) (hw : FixedWithin (fun _ => S) s) (hd : ∀ i, draw i ∈ S) : 0 ≤ roundPseudoRegret S mu s draw

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

theorem expected_round_charge {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (hcard : S.card = n) (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (s : State n k) (hs : DistinctFixed s) (hw : FixedWithin (fun _ => S) s) : ∑ draw, (jointDraw (fun _ : Fin n => S) (fun _ => hne)) draw * ENNReal.ofReal (roundPseudoRegret S mu s draw) ≤ 2 * (unfixedCount s : ℝ≥0∞)

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

noncomputable def expectedCoordinationRegret {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (mu : Fin k → ℝ) (T : ℕ) : ℝ≥0∞

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

theorem expectedCoordinationRegret_le {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (hcard : S.card = n) (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (T : ℕ) : expectedCoordinationRegret (n := n) S hne mu T ≤ 8 * (n : ℝ≥0∞)^2

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

theorem expectedCoordinationRegret_toReal {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a) (T : ℕ) : (expectedCoordinationRegret (n := n) S hne mu T).toReal = ∑ t ∈ Finset.range T, ∑ s, ((stateLaw (fun _ : Fin n => S) (fun _ => hne) t) s).toReal * ∑ draw, ((jointDraw (fun _ : Fin n => S) (fun _ => hne)) draw).toReal * roundPseudoRegret S mu s draw

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

theorem expectedCoordinationRegret_real_le {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) (hcard : S.card = n) (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (T : ℕ) : (∑ t ∈ Finset.range T, ∑ s, ((stateLaw (fun _ : Fin n => S) (fun _ => hne) t) s).toReal * ∑ draw, ((jointDraw (fun _ : Fin n => S) (fun _ => hne)) draw).toReal * roundPseudoRegret S mu s draw) ≤ 8 * (n : ℝ)^2