BanditRLProof.Algorithms.MusicalChairsLearnerRegret

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

theorem ordered_set_sum_max {α : Type*} [DecidableEq α] (score : α → ℝ) (S B : Finset α) (hcard : B.card ≤ S.card) (hnonneg : ∀ a, 0 ≤ score a) (horder : ∀ a ∈ S, ∀ b ∉ S, score b ≤ score a) : ∑ b ∈ B, score b ≤ ∑ a ∈ S, score a

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

theorem topArms_sum_max {k n : ℕ} (score : Fin k → ℝ) (hnk : n ≤ k) (hnonneg : ∀ a, 0 ≤ score a) (B : Finset (Fin k)) (hcard : B.card ≤ n) : ∑ b ∈ B, score b ≤ ∑ a ∈ topArms score n, score a

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

noncomputable def collisionFreePlayers {n k : ℕ} (a : Fin n → Fin k) : Finset (Fin n)

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

noncomputable def earnedArms {n k : ℕ} (a : Fin n → Fin k) : Finset (Fin k)

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

theorem collisionFree_action_injective {n k : ℕ} (a : Fin n → Fin k) : Set.InjOn a (collisionFreePlayers a)

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

theorem earnedArms_card_le {n k : ℕ} (a : Fin n → Fin k) : (earnedArms a).card ≤ n

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

theorem earnedArms_sum {n k : ℕ} (mu : Fin k → ℝ) (a : Fin n → Fin k) : ∑ b ∈ earnedArms a, mu b = ∑ i, if CollisionFree a i then mu (a i) else 0

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

noncomputable def globalRoundRegret {n k : ℕ} (mu : Fin k → ℝ) (a : Fin n → Fin k) : ℝ

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

theorem globalRoundRegret_nonneg {n k : ℕ} (mu : Fin k → ℝ) (hnk : n ≤ k) (hmu : ∀ b, 0 ≤ mu b) (a : Fin n → Fin k) : 0 ≤ globalRoundRegret mu a

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

theorem globalRoundRegret_le {n k : ℕ} (mu : Fin k → ℝ) (hnk : n ≤ k) (hmu : ∀ b, 0 ≤ mu b ∧ mu b ≤ 1) (a : Fin n → Fin k) : globalRoundRegret mu a ≤ n

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

theorem roundPseudoRegret_global {n k : ℕ} (mu : Fin k → ℝ) (s : State n k) (d : Fin n → Fin k) : roundPseudoRegret (topArms mu n) mu s d = globalRoundRegret mu (action s d)

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

noncomputable def learnerAction {n k S L : ℕ} (hk : 0 < k) (x : Fin S → Fin n → Fin k) (d : Fin L → Fin n → Fin k) (t : ℕ) : Fin n → Fin k

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

theorem learnerAction_explore {n k S L : ℕ} (hk : 0 < k) (x : Fin S → Fin n → Fin k) (d : Fin L → Fin n → Fin k) (t : ℕ) (ht : t < S) : learnerAction hk x d t = x ⟨t,ht⟩

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

theorem learnerAction_coordinate {n k S L : ℕ} (hk : 0 < k) (x : Fin S → Fin n → Fin k) (d : Fin L → Fin n → Fin k) (t : Fin L) : learnerAction hk x d (S+t.val) = continuationAction hk d t

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

noncomputable def explorationPrefixRegret {n k S : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (x : Fin S → Fin n → Fin k) (H : ℕ) : ℝ

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

noncomputable def learnerRegret {n k S H : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (x : Fin S → Fin n → Fin k) (d : Fin (H-S) → Fin n → Fin k) : ℝ

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

theorem learnerRegret_split {n k S H : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (x : Fin S → Fin n → Fin k) (d : Fin (H-S) → Fin n → Fin k) : learnerRegret hk mu x d = explorationPrefixRegret hk mu x H + pathCoordinationRegret hk (topArms mu n) mu d

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

theorem explorationPrefixRegret_bounds {n k S : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (hnk : n ≤ k) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (x : Fin S → Fin n → Fin k) (H : ℕ) : 0 ≤ explorationPrefixRegret hk mu x H ∧ explorationPrefixRegret hk mu x H ≤ (n : ℝ) * min H S

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

theorem learnerRegret_bounds {n k S H : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (hnk : n ≤ k) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (x : Fin S → Fin n → Fin k) (d : Fin (H-S) → Fin n → Fin k) : 0 ≤ learnerRegret hk mu x d ∧ learnerRegret hk mu x d ≤ (n : ℝ) * H

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

theorem learnerRegret_le_exploration_add {n k S H : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (hnk : n ≤ k) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (x : Fin S → Fin n → Fin k) (d : Fin (H-S) → Fin n → Fin k) : learnerRegret hk mu x d ≤ (n : ℝ)*min H S + pathCoordinationRegret hk (topArms mu n) mu d

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

theorem learnerAction_prefix {n k S L : ℕ} (hk : 0 < k) (x y : Fin S → Fin n → Fin k) (d e : Fin L → Fin n → Fin k) (t : ℕ) (ht : t < S+L) (hx : ∀ u : Fin S, u.val ≤ t → x u = y u) (hd : ∀ u : Fin L, S+u.val ≤ t → d u = e u) : learnerAction hk x d t = learnerAction hk y e t

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

theorem integrable_learnerRegret {n k S H : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (P : Measure (((Fin S → Fin n → Fin k) × (Fin S → Fin k → ℝ)) × (Fin (H-S) → Fin n → Fin k))) [IsFiniteMeasure P] : Integrable (fun z => learnerRegret hk mu z.1.1 z.2) P

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

theorem integrable_pathRegret_projection {n k S L : ℕ} (hk : 0 < k) (A : Finset (Fin k)) (mu : Fin k → ℝ) (P : Measure (((Fin S → Fin n → Fin k) × (Fin S → Fin k → ℝ)) × (Fin L → Fin n → Fin k))) [IsFiniteMeasure P] : Integrable (fun z => pathCoordinationRegret hk A mu z.2) P

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

theorem learnerRegret_good_integral_le {n k S H : ℕ} (hk : 1 < k) (hnk : n ≤ k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (hne : (topArms mu n).Nonempty) (E : Set ((Fin S → Fin n → Fin k) × (Fin S → Fin k → ℝ))) (hE : MeasurableSet E) (hEG : E ⊆ explorationGoodEvent (n := n) (topArms mu n)) : (∫ z in Prod.fst ⁻¹' E, learnerRegret (n := n) (by omega) mu z.1.1 z.2 ∂explorationContinuationLaw hk nu (H-S)) ≤ (explorationRewardLaw (by omega) nu E).toReal * ((n : ℝ)*min H S + 8*(n : ℝ)^2)

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

theorem learnerRegret_expected_le {n k S H : ℕ} (hk : 1 < k) (hnk : n ≤ k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (mu : Fin k → ℝ) (hmu : ∀ a, 0 ≤ mu a ∧ mu a ≤ 1) (hne : (topArms mu n).Nonempty) (E : Set ((Fin S → Fin n → Fin k) × (Fin S → Fin k → ℝ))) (hE : MeasurableSet E) (hEG : E ⊆ explorationGoodEvent (n := n) (topArms mu n)) (delta : ℝ) (hdelta : 0 ≤ delta) (hprob : 1-ENNReal.ofReal delta ≤ explorationRewardLaw (by omega) nu E) : (∫ z, learnerRegret (n := n) (by omega) mu z.1.1 z.2 ∂explorationContinuationLaw hk nu (H-S)) ≤ min ((n : ℝ)*H) ((n : ℝ)*min H S + 8*(n : ℝ)^2 + delta*((n : ℝ)*H))

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

theorem source_expected_learnerRegret_le {n k H : ℕ} (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, learnerRegret (n := n) (S := explorationLength k eps delta) (H := H) (by omega) (armMean nu) z.1.1 z.2 ∂explorationContinuationLaw (by omega) nu (H-explorationLength k eps delta)) ≤ min ((n : ℝ)*H) ((n : ℝ)*min H (explorationLength k eps delta) + 8*(n : ℝ)^2 + delta*((n : ℝ)*H))

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

theorem source_conditional_learnerRegret_le {n k H : ℕ} (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)), learnerRegret (H := H) (by omega) (armMean nu) z.1.1 z.2 ∂explorationContinuationLaw (by omega) nu (H-explorationLength k eps delta)) / (explorationContinuationLaw (by omega) nu (H-explorationLength k eps delta) (Prod.fst ⁻¹' (explorationGoodEvent (n := n) (T := explorationLength k eps delta) (trueTopArms nu n)))).toReal ≤ (n : ℝ)*min H (explorationLength k eps delta) + 8*(n : ℝ)^2

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

theorem source_expected_learnerRegret_coarse {n k H : ℕ} (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, learnerRegret (n := n) (S := explorationLength k eps delta) (H := H) (by omega) (armMean nu) z.1.1 z.2 ∂explorationContinuationLaw (by omega) nu (H-explorationLength k eps delta)) ≤ min ((n : ℝ)*H) ((n : ℝ)*explorationLength k eps delta + 8*(n : ℝ)^2 + delta*((n : ℝ)*H))

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

theorem coordination_residual_source_constant (n : ℕ) : 8*(n : ℝ)^2 ≤ 2*Real.exp 2*(n : ℝ)^2

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

theorem source_expected_learnerRegret_published_residual {n k H : ℕ} (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, learnerRegret (n := n) (S := explorationLength k eps delta) (H := H) (by omega) (armMean nu) z.1.1 z.2 ∂explorationContinuationLaw (by omega) nu (H-explorationLength k eps delta)) ≤ min ((n : ℝ)*H) ((n : ℝ)*explorationLength k eps delta + 2*Real.exp 2*(n : ℝ)^2 + delta*((n : ℝ)*H))

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

theorem source_expected_learnerRegret_inverse_horizon {n k H : ℕ} (hn : 0 < n) (hnk : n < k) (hH : 2 ≤ H) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (eps : ℝ) (heps : 0 < eps) (hepsgap : eps < boundaryGap (armMean nu) n hn hnk) : (∫ z, learnerRegret (n := n) (S := explorationLength k eps (1/(H : ℝ))) (H := H) (by omega) (armMean nu) z.1.1 z.2 ∂explorationContinuationLaw (by omega) nu (H-explorationLength k eps (1/(H : ℝ)))) ≤ min ((n : ℝ)*H) ((n : ℝ)*explorationLength k eps (1/(H : ℝ)) + 8*(n : ℝ)^2 + n)

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

theorem source_conditional_learnerRegret_published_residual {n k H : ℕ} (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) (hSH : explorationLength k eps delta ≤ H) : (∫ z in Prod.fst ⁻¹' (explorationGoodEvent (n := n) (T := explorationLength k eps delta) (trueTopArms nu n)), learnerRegret (H := H) (by omega) (armMean nu) z.1.1 z.2 ∂explorationContinuationLaw (by omega) nu (H-explorationLength k eps delta)) / (explorationContinuationLaw (by omega) nu (H-explorationLength k eps delta) (Prod.fst ⁻¹' (explorationGoodEvent (n := n) (T := explorationLength k eps delta) (trueTopArms nu n)))).toReal ≤ (n : ℝ)*explorationLength k eps delta + 2*Real.exp 2*(n : ℝ)^2