BanditRLProof.Algorithms.MusicalChairsMarginal

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

theorem iid_sum_snoc {α : Type*} [Fintype α] (p : PMF α) (T : ℕ) (f : (Fin (T+1) → α) → ℝ≥0∞) : ∑ d, iid p (T+1) d * f d = ∑ x, iid p T x * ∑ a, p a * f (Fin.snoc x a)

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

theorem iid_snoc {α : Type*} [Fintype α] (p : PMF α) (T : ℕ) : iid p (T+1) = (iid p T).bind (fun x => p.map (Fin.snoc x))

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

theorem trajectory_snoc_prefix {n k T : ℕ} (hk : 0 < k) (d : Fin T → Fin n → Fin k) (a : Fin n → Fin k) : trajectory (extendedCoordinationDraws hk (Fin.snoc d a)) T = trajectory (extendedCoordinationDraws hk d) T

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

theorem trajectory_snoc_last {n k T : ℕ} (hk : 0 < k) (d : Fin T → Fin n → Fin k) (a : Fin n → Fin k) : trajectory (extendedCoordinationDraws hk (Fin.snoc d a)) (T+1) = step (trajectory (extendedCoordinationDraws hk d) T) a

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

theorem iid_trajectory_stateLaw {n k : ℕ} (hk : 0 < k) (C : Fin n → Finset (Fin k)) (hne : ∀ i, (C i).Nonempty) (T : ℕ) : (FinitePMF.iid (jointDraw C hne) T).map (fun d => trajectory (extendedCoordinationDraws hk d) T) = stateLaw C hne T

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

theorem iid_take {α : Type*} [Fintype α] (p : PMF α) {T L : ℕ} (h : T ≤ L) : (iid p L).map (fun d t => d (Fin.castLE h t)) = iid p T

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

theorem sum_map {α β : Type*} [Fintype α] [Fintype β] (p : PMF α) (g : α → β) (f : β → ℝ≥0∞) : ∑ b, p.map g b * f b = ∑ a, p a * f (g a)

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

theorem trajectory_take {n k T L : ℕ} (hk : 0 < k) (h : T ≤ L) (d : Fin L → Fin n → Fin k) : trajectory (extendedCoordinationDraws hk d) T = trajectory (extendedCoordinationDraws hk (fun t => d (Fin.castLE h t))) T

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

theorem iid_trajectory_marginal {n k T L : ℕ} (hk : 0 < k) (h : T ≤ L) (C : Fin n → Finset (Fin k)) (hne : ∀ i, (C i).Nonempty) : (FinitePMF.iid (jointDraw C hne) L).map (fun d => trajectory (extendedCoordinationDraws hk d) T) = stateLaw C hne T

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

theorem iid_last_state_draw {n k T : ℕ} (hk : 0 < k) (C : Fin n → Finset (Fin k)) (hne : ∀ i, (C i).Nonempty) : (FinitePMF.iid (jointDraw C hne) (T+1)).map (fun d => (trajectory (extendedCoordinationDraws hk d) T, d (Fin.last T))) = (stateLaw C hne T).bind (fun s => (jointDraw C hne).map (fun a => (s,a)))

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

theorem iid_round_state_draw {n k L : ℕ} (hk : 0 < k) (t : Fin L) (C : Fin n → Finset (Fin k)) (hne : ∀ i, (C i).Nonempty) : (FinitePMF.iid (jointDraw C hne) L).map (fun d => (trajectory (extendedCoordinationDraws hk d) t.val, d t)) = (stateLaw C hne t.val).bind (fun s => (jointDraw C hne).map (fun a => (s,a)))

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

theorem sum_map_real {α β : Type*} [Fintype α] [Fintype β] (p : PMF α) (g : α → β) (f : β → ℝ) : ∑ b, (p.map g b).toReal * f b = ∑ a, (p a).toReal * f (g a)

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

theorem sum_bind_real {α β : Type*} [Fintype α] [Fintype β] (p : PMF α) (q : α → PMF β) (f : β → ℝ) : ∑ b, (p.bind q b).toReal * f b = ∑ a, (p a).toReal * ∑ b, (q a b).toReal * f b

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

noncomputable def pathCoordinationRegret {n k L : ℕ} (hk : 0 < k) (S : Finset (Fin k)) (mu : Fin k → ℝ) (d : Fin L → Fin n → Fin k) : ℝ

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

theorem iid_round_regret_expectation {n k L : ℕ} (hk : 0 < k) (t : Fin L) (C : Fin n → Finset (Fin k)) (hne : ∀ i, (C i).Nonempty) (S : Finset (Fin k)) (mu : Fin k → ℝ) : (∑ d, (FinitePMF.iid (jointDraw C hne) L d).toReal * roundPseudoRegret S mu (trajectory (extendedCoordinationDraws hk d) t.val) (d t)) = ∑ s, (stateLaw C hne t.val s).toReal * ∑ a, (jointDraw C hne a).toReal * roundPseudoRegret S mu s a

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

theorem iid_path_regret_expectation {n k L : ℕ} (hk : 0 < k) (S : Finset (Fin k)) (hne : S.Nonempty) (mu : Fin k → ℝ) : (∑ d, (FinitePMF.iid (jointDraw (fun _ : Fin n => S) (fun _ => hne)) L d).toReal * pathCoordinationRegret hk S mu d) = ∑ t ∈ Finset.range L, ∑ s, (stateLaw (fun _ : Fin n => S) (fun _ => hne) t s).toReal * ∑ a, (jointDraw (fun _ : Fin n => S) (fun _ => hne) a).toReal * roundPseudoRegret S mu s a

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

theorem iid_path_regret_le {n k L : ℕ} (hk : 0 < k) (S : Finset (Fin k)) (hne : S.Nonempty) (hcard : S.card = n) (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) : (∑ d, (FinitePMF.iid (jointDraw (fun _ : Fin n => S) (fun _ => hne)) L d).toReal * pathCoordinationRegret hk S mu d) ≤ 8 * (n : ℝ)^2

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

theorem learnedDrawPathKernel_state_marginal {n k T L t : ℕ} (hk : 1 < k) (ht : t ≤ L) (z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) : (learnedDrawPathKernel hk L z).map (fun d => trajectory (extendedCoordinationDraws (by omega) d) t) = (stateLaw (learnedConfig hk z).val (learnedConfig hk z).property t).toMeasure

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

theorem learnedDrawPathKernel_round_marginal {n k T L : ℕ} (hk : 1 < k) (t : Fin L) (z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) : (learnedDrawPathKernel hk L z).map (fun d => (trajectory (extendedCoordinationDraws (by omega) d) t.val, d t)) = ((stateLaw (learnedConfig hk z).val (learnedConfig hk z).property t.val).bind (fun s => (jointDraw (learnedConfig hk z).val (learnedConfig hk z).property).map (fun a => (s,a)))).toMeasure

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

theorem explorationContinuationLaw_restricted_path {n k T L : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (S : Finset (Fin k)) (hne : S.Nonempty) (E : Set ((Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ))) (hE : MeasurableSet E) (hEG : E ⊆ explorationGoodEvent (n := n) S) : ((explorationContinuationLaw hk nu L).restrict (Prod.fst ⁻¹' E)).map Prod.snd = explorationRewardLaw (by omega) nu E • (FinitePMF.iid (jointDraw (fun _ : Fin n => S) (fun _ => hne)) L).toMeasure

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

theorem explorationContinuationLaw_good_regret_integral {n k T L : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (S : Finset (Fin k)) (hne : S.Nonempty) (mu : Fin k → ℝ) (E : Set ((Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ))) (hE : MeasurableSet E) (hEG : E ⊆ explorationGoodEvent (n := n) S) : (∫ z in Prod.fst ⁻¹' E, pathCoordinationRegret (by omega) S mu z.2 ∂explorationContinuationLaw hk nu L) = (explorationRewardLaw (by omega) nu E).toReal * ∑ d, (FinitePMF.iid (jointDraw (fun _ : Fin n => S) (fun _ => hne)) L d).toReal * pathCoordinationRegret (by omega) S mu d

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

theorem explorationContinuationLaw_conditional_coordination_regret {n k T L : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (S : Finset (Fin k)) (hne : S.Nonempty) (hcard : S.card = n) (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (E : Set ((Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ))) (hE : MeasurableSet E) (hEG : E ⊆ explorationGoodEvent (n := n) S) (hpos : 0 < explorationRewardLaw (by omega) nu E) : (∫ z in Prod.fst ⁻¹' E, pathCoordinationRegret (by omega) S mu z.2 ∂explorationContinuationLaw hk nu L) / (explorationContinuationLaw hk nu L (Prod.fst ⁻¹' E)).toReal ≤ 8 * (n : ℝ)^2

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

theorem iid_continuationAction_marginal {n k L : ℕ} (hk : 0 < k) (t : Fin L) (C : Fin n → Finset (Fin k)) (hne : ∀ i, (C i).Nonempty) : (FinitePMF.iid (jointDraw C hne) L).map (fun d => continuationAction hk d t) = (stateLaw C hne t.val).bind (fun s => (jointDraw C hne).map (action s))

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

theorem source_conditional_coordination_regret {n k L : ℕ} (hn : 0 < n) (hnk : n < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (eps delta : ℝ) (heps : 0 < eps) (hepsgap : eps < boundaryGap (armMean nu) n hn hnk) (hdelta : 0 < delta) (hdelta1 : delta < 1) : (∫ z in Prod.fst ⁻¹' (explorationGoodEvent (n := n) (T := explorationLength k eps delta) (trueTopArms nu n)), pathCoordinationRegret (by omega) (trueTopArms nu n) (armMean nu) z.2 ∂explorationContinuationLaw (by omega) nu L) / (explorationContinuationLaw (by omega) nu L (Prod.fst ⁻¹' (explorationGoodEvent (n := n) (T := explorationLength k eps delta) (trueTopArms nu n)))).toReal ≤ 8 * (n : ℝ)^2