BanditRLProof.Algorithms.MusicalChairsRealized

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

theorem reward_coordinate_integrable {k D : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (t : Fin D) (a : Fin k) : Integrable (fun r : Fin D → Fin k → ℝ => r t a) (rewardLaw nu D)

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

noncomputable def scheduleRealizedRegret {n k D T : ℕ} (mu : Fin k → ℝ) (j : Fin T → Fin D) (a : Fin T → Fin n → Fin k) (r : Fin D → Fin k → ℝ) : ℝ

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

theorem integrable_scheduleRealizedRegret {n k D T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (mu : Fin k → ℝ) (j : Fin T → Fin D) (a : Fin T → Fin n → Fin k) : Integrable (scheduleRealizedRegret mu j a) (rewardLaw nu D)

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

theorem scheduleRealizedRegret_mean {n k D T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (j : Fin T → Fin D) (a : Fin T → Fin n → Fin k) : (∫ r, scheduleRealizedRegret (armMean nu) j a r ∂rewardLaw nu D) = ∑ t : Fin T, globalRoundRegret (armMean nu) (a t)

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

theorem measurable_scheduleRealizedRegret {n k D T : ℕ} (mu : Fin k → ℝ) (j : Fin T → Fin D) : Measurable (fun z : (Fin T → Fin n → Fin k) × (Fin D → Fin k → ℝ) => scheduleRealizedRegret mu j z.1 z.2)

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

theorem integrable_randomScheduleRegret {α : Type*} [MeasurableSpace α] {n k D T : ℕ} (P : Measure α) [IsFiniteMeasure P] (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (mu : Fin k → ℝ) (j : Fin T → Fin D) (a : α → Fin T → Fin n → Fin k) (ha : Measurable a) : Integrable (fun z : α × (Fin D → Fin k → ℝ) => scheduleRealizedRegret mu j (a z.1) z.2) (P.prod (rewardLaw nu D))

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

theorem randomScheduleRegret_mean {α : Type*} [MeasurableSpace α] {n k D T : ℕ} (P : Measure α) [IsFiniteMeasure P] (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (j : Fin T → Fin D) (a : α → Fin T → Fin n → Fin k) (ha : Measurable a) : (∫ z, scheduleRealizedRegret (armMean nu) j (a z.1) z.2 ∂P.prod (rewardLaw nu D)) = ∫ x, ∑ t : Fin T, globalRoundRegret (armMean nu) (a x t) ∂P

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

noncomputable def explorationRealizedRegret {n k S : ℕ} (mu : Fin k → ℝ) (x : Fin S → Fin n → Fin k) (r : Fin S → Fin k → ℝ) (H : ℕ) : ℝ

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

noncomputable def continuationRealizedRegret {n k L : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (d : Fin L → Fin n → Fin k) (r : Fin L → Fin k → ℝ) : ℝ

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

theorem exploration_schedule_pseudo {n k S : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (x : Fin S → Fin n → Fin k) (H : ℕ) : (∑ t : Fin (min H S), globalRoundRegret mu (x (Fin.castLE (Nat.min_le_right H S) t))) = explorationPrefixRegret hk mu x H

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

theorem continuation_schedule_pseudo {n k L : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (d : Fin L → Fin n → Fin k) : (∑ t : Fin L, globalRoundRegret mu (continuationAction hk d t)) = pathCoordinationRegret hk (topArms mu n) mu d

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

theorem integrable_explorationRealizedRegret {n k S : ℕ} (hk : 0 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (mu : Fin k → ℝ) (H : ℕ) : Integrable (fun z : (Fin S → Fin n → Fin k) × (Fin S → Fin k → ℝ) => explorationRealizedRegret mu z.1 z.2 H) (explorationRewardLaw hk nu)

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

theorem explorationRealizedRegret_mean {n k S : ℕ} (hk : 0 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (H : ℕ) : (∫ z : (Fin S → Fin n → Fin k) × (Fin S → Fin k → ℝ), explorationRealizedRegret (armMean nu) z.1 z.2 H ∂explorationRewardLaw hk nu) = ∫ z : (Fin S → Fin n → Fin k) × (Fin S → Fin k → ℝ), explorationPrefixRegret hk (armMean nu) z.1 H ∂explorationRewardLaw hk nu

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

abbrev FullSample (n k S H : ℕ)

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

noncomputable def completeLearnerLaw {n k S H : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) : Measure (FullSample n k S H)

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

theorem completeLearnerLaw_first_preserving {n k S H : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] : MeasurePreserving (Prod.fst : FullSample n k S H → _) (completeLearnerLaw hk nu) (explorationContinuationLaw hk nu (H-S))

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

theorem explorationContinuationLaw_first_preserving {n k S L : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] : MeasurePreserving (Prod.fst : ((Fin S → Fin n → Fin k) × (Fin S → Fin k → ℝ)) × (Fin L → Fin n → Fin k) → _) (explorationContinuationLaw hk nu L) (explorationRewardLaw (by omega) nu)

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

theorem completeLearnerLaw_exploration_preserving {n k S H : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] : MeasurePreserving (fun z : FullSample n k S H => z.1.1) (completeLearnerLaw hk nu) (explorationRewardLaw (by omega) nu)

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

noncomputable def realizedLearnerRegret {n k S H : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (z : FullSample n k S H) : ℝ

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

theorem integral_preserving_pullback {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {P : Measure α} {Q : Measure β} (g : α → β) (hg : MeasurePreserving g P Q) (f : β → ℝ) (hf : Integrable f Q) : (∫ x, f (g x) ∂P) = ∫ y, f y ∂Q

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

theorem measurable_continuationSchedule {n k L : ℕ} (hk : 0 < k) : Measurable (fun d : Fin L → Fin n → Fin k => fun t : Fin L => continuationAction hk d t)

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

theorem integrable_realizedLearnerRegret {n k S H : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (mu : Fin k → ℝ) : Integrable (realizedLearnerRegret (n := n) (S := S) (H := H) (by omega) mu) (completeLearnerLaw hk nu)

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

theorem continuationRealizedRegret_mean_joint {n k S H : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) : (∫ z : FullSample n k S H, continuationRealizedRegret (by omega) (armMean nu) z.1.2 z.2 ∂completeLearnerLaw hk nu) = ∫ z, pathCoordinationRegret (by omega) (trueTopArms nu n) (armMean nu) z.2 ∂explorationContinuationLaw (n := n) (T := S) hk nu (H-S)

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

theorem realizedLearnerRegret_expected_eq_pseudo {n k S H : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) : (∫ z : FullSample n k S H, realizedLearnerRegret (by omega) (armMean nu) z ∂completeLearnerLaw hk nu) = ∫ z, learnerRegret (n := n) (S := S) (H := H) (by omega) (armMean nu) z.1.1 z.2 ∂explorationContinuationLaw (n := n) (T := S) hk nu (H-S)

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

theorem source_expected_realizedLearnerRegret_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 : FullSample n k (explorationLength k eps delta) H, realizedLearnerRegret (by omega) (armMean nu) z ∂completeLearnerLaw (by omega) nu) ≤ 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.

noncomputable def continuationFeedback {n k L : ℕ} (hk : 0 < k) (d : Fin L → Fin n → Fin k) (r : Fin L → Fin k → ℝ) (i : Fin n) (t : Fin L) : ExplorationFeedback k

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

noncomputable def learnerFeedback {n k S H : ℕ} (hk : 0 < k) (z : FullSample n k S H) (i : Fin n) (t : Fin H) : ExplorationFeedback k

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

theorem learnerFeedback_explore {n k S H : ℕ} (hk : 0 < k) (z : FullSample n k S H) (i : Fin n) (t : Fin H) (ht : t.val < S) : learnerFeedback hk z i t = explorationFeedback z.1.1.1 z.1.1.2 i ⟨t.val,ht⟩

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

theorem learnerFeedback_coordinate {n k S H : ℕ} (hk : 0 < k) (z : FullSample n k S H) (i : Fin n) (u : Fin (H-S)) : learnerFeedback hk z i ⟨S+u.val,by omega⟩ = continuationFeedback hk z.1.2 z.2 i u

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

theorem learnerFeedback_arm {n k S H : ℕ} (hk : 0 < k) (z : FullSample n k S H) (i : Fin n) (t : Fin H) : (learnerFeedback hk z i t).arm = learnerAction hk z.1.1.1 z.1.2 t.val i

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

theorem learnerFeedback_collision {n k S H : ℕ} (hk : 0 < k) (z : FullSample n k S H) (i : Fin n) (t : Fin H) : (learnerFeedback hk z i t).collided = collisionBit (learnerAction hk z.1.1.1 z.1.2 t.val) i

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

theorem learnerFeedback_completed_exploration {n k S H : ℕ} (hk : 0 < k) (hSH : S ≤ H) (z : FullSample n k S H) (i : Fin n) : (fun t : Fin S => learnerFeedback hk z i (Fin.castLE hSH t)) = explorationFeedback z.1.1.1 z.1.1.2 i

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

theorem learnedConfig_from_feedback {n k S H : ℕ} (hk : 1 < k) (hSH : S ≤ H) (z : FullSample n k S H) (i : Fin n) : (learnedConfig hk z.1.1).val i = localCandidateSet (fun t : Fin S => learnerFeedback (by omega) z i (Fin.castLE hSH t))

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

theorem continuationFeedback_local_update {n k L : ℕ} (hk : 0 < k) (d : Fin L → Fin n → Fin k) (r : Fin L → Fin k → ℝ) (i : Fin n) (t : Fin L) : trajectory (extendedCoordinationDraws hk d) (t.val+1) i = localUpdate (trajectory (extendedCoordinationDraws hk d) t.val i) (continuationFeedback hk d r i t).arm (continuationFeedback hk d r i t).collided

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

theorem learnerFeedback_prefix {n k S H : ℕ} (hk : 0 < k) (z w : FullSample n k S H) (i : Fin n) (t : Fin H) (hx : ∀ u : Fin S, u.val ≤ t.val → z.1.1.1 u = w.1.1.1 u) (hr : ∀ u : Fin S, u.val ≤ t.val → z.1.1.2 u = w.1.1.2 u) (hd : ∀ u : Fin (H-S), S+u.val ≤ t.val → z.1.2 u = w.1.2 u) (hy : ∀ u : Fin (H-S), S+u.val ≤ t.val → z.2 u = w.2 u) : learnerFeedback hk z i t = learnerFeedback hk w i t

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

theorem finite_sum_split_at {H S : ℕ} (hSH : S ≤ H) (f : Fin H → ℝ) : (∑ t : Fin H, f t) = (∑ t : Fin S, f (Fin.castLE hSH t)) + ∑ u : Fin (H-S), f ⟨S+u.val,by omega⟩

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

theorem realizedLearnerRegret_eq_feedback {n k S H : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (z : FullSample n k S H) : realizedLearnerRegret hk mu z = ∑ t : Fin H, ((∑ a ∈ topArms mu n, mu a) - ∑ i : Fin n, (learnerFeedback hk z i t).reward)

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

theorem measurable_feedback_mk {α : Type*} [MeasurableSpace α] {k : ℕ} (a : α → Fin k) (c : α → Bool) (r : α → ℝ) (ha : Measurable a) (hc : Measurable c) (hr : Measurable r) : Measurable (fun x => (⟨a x,c x,r x⟩ : ExplorationFeedback k))

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

theorem measurable_explorationFeedback {n k S : ℕ} (i : Fin n) (t : Fin S) : Measurable (fun z : (Fin S → Fin n → Fin k) × (Fin S → Fin k → ℝ) => explorationFeedback z.1 z.2 i t)

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

theorem measurable_continuationFeedback {n k L : ℕ} (hk : 0 < k) (i : Fin n) (t : Fin L) : Measurable (fun z : (Fin L → Fin n → Fin k) × (Fin L → Fin k → ℝ) => continuationFeedback hk z.1 z.2 i t)

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

theorem measurable_learnerFeedback {n k S H : ℕ} (hk : 0 < k) (i : Fin n) (t : Fin H) : Measurable (fun z : FullSample n k S H => learnerFeedback hk z i t)

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

theorem measurable_learnerTrace {n k S H : ℕ} (hk : 0 < k) : Measurable (fun z : FullSample n k S H => fun i t => learnerFeedback hk z i t)

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

noncomputable def visibleLearnerLaw {n k S H : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) : Measure (Fin n → Fin H → ExplorationFeedback k)

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

noncomputable def visibleRegret {n k H : ℕ} (mu : Fin k → ℝ) (f : Fin n → Fin H → ExplorationFeedback k) : ℝ

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

theorem measurable_feedback_reward {k : ℕ} : Measurable (ExplorationFeedback.reward : ExplorationFeedback k → ℝ)

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

theorem measurable_visibleRegret {n k H : ℕ} (mu : Fin k → ℝ) : Measurable (visibleRegret (n := n) (H := H) mu)

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

theorem visibleRegret_pullback {n k S H : ℕ} (hk : 0 < k) (mu : Fin k → ℝ) (z : FullSample n k S H) : visibleRegret mu (fun i t => learnerFeedback hk z i t) = realizedLearnerRegret hk mu z

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

theorem integrable_visibleRegret {n k S H : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (mu : Fin k → ℝ) : Integrable (visibleRegret (n := n) (H := H) mu) (visibleLearnerLaw (S := S) hk nu)

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

theorem visibleRegret_expected_eq_realized {n k S H : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) (mu : Fin k → ℝ) : (∫ f, visibleRegret (n := n) (H := H) mu f ∂visibleLearnerLaw (S := S) hk nu) = ∫ z : FullSample n k S H, realizedLearnerRegret (by omega) mu z ∂completeLearnerLaw hk nu

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

theorem source_expected_visibleRegret_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) : (∫ f, visibleRegret (n := n) (H := H) (armMean nu) f ∂visibleLearnerLaw (S := explorationLength k eps delta) (by omega) nu) ≤ min ((n : ℝ)*H) ((n : ℝ)*explorationLength k eps delta + 8*(n : ℝ)^2 + delta*((n : ℝ)*H))