BanditRLProof.Algorithms.MusicalChairsHandoff

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

noncomputable def rankedArm {k : ℕ} (score : Fin k → ℝ) (j : Fin k) : Fin k

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

noncomputable def rankIndex {k : ℕ} (score : Fin k → ℝ) (a : Fin k) : Fin k

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

theorem rankedArm_rankIndex {k : ℕ} (score : Fin k → ℝ) (a : Fin k) : rankedArm score (rankIndex score a) = a

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

theorem rankIndex_rankedArm {k : ℕ} (score : Fin k → ℝ) (j : Fin k) : rankIndex score (rankedArm score j) = j

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

theorem mem_topArms_iff_rankIndex {k : ℕ} (score : Fin k → ℝ) (n : ℕ) (a : Fin k) : a ∈ topArms score n ↔ (rankIndex score a).val < n

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

theorem ranked_score_antitone {k : ℕ} (score : Fin k → ℝ) {i j : Fin k} (hij : i ≤ j) : score (rankedArm score j) ≤ score (rankedArm score i)

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

noncomputable def boundaryGap {k : ℕ} (score : Fin k → ℝ) (n : ℕ) (hn : 0 < n) (hnk : n < k) : ℝ

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

theorem boundaryGap_nonneg {k : ℕ} (score : Fin k → ℝ) (n : ℕ) (hn : 0 < n) (hnk : n < k) : 0 ≤ boundaryGap score n hn hnk

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

theorem boundaryGap_separates {k : ℕ} (score : Fin k → ℝ) (n : ℕ) (hn : 0 < n) (hnk : n < k) : ∀ a ∈ topArms score n, ∀ b ∉ topArms score n, boundaryGap score n hn hnk ≤ score a - score b

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

theorem explorationGoodEvent_orderStatistic_probability {n k : ℕ} (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) : 1 - ENNReal.ofReal delta ≤ explorationRewardLaw (by omega) nu (explorationGoodEvent (n := n) (T := explorationLength k eps delta) (trueTopArms nu n))

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

theorem measurableSet_actualCandidate_eq {n k T : ℕ} (i : Fin n) (S : Finset (Fin k)) : MeasurableSet {z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ) | localCandidateSet (explorationFeedback z.1 z.2 i) = S}

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

def CandidateConfig (n k : ℕ)

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

noncomputable def learnedConfig {n k T : ℕ} (hk : 1 < k) (z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) : CandidateConfig n k

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

theorem measurable_learnedConfig {n k T : ℕ} (hk : 1 < k) : Measurable (learnedConfig (n := n) (T := T) hk)

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

noncomputable def configDrawPathKernel (n k L : ℕ) : Kernel (CandidateConfig n k) (Fin L → Fin n → Fin k)

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

noncomputable def learnedDrawPathKernel {n k T : ℕ} (hk : 1 < k) (L : ℕ) : Kernel ((Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) (Fin L → Fin n → Fin k)

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

theorem learnedDrawPathKernel_apply {n k T L : ℕ} (hk : 1 < k) (z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) : learnedDrawPathKernel hk L z = (FinitePMF.iid (jointDraw (learnedConfig hk z).val (learnedConfig hk z).property) L).toMeasure

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

theorem learnedDrawPathKernel_pi {n k T L : ℕ} (hk : 1 < k) (z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) : learnedDrawPathKernel hk L z = Measure.pi (fun _ : Fin L => (jointDraw (learnedConfig hk z).val (learnedConfig hk z).property).toMeasure)

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

theorem learnedDrawPathKernel_time_independent {n k T L : ℕ} (hk : 1 < k) (z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) : iIndepFun (fun t (draws : Fin L → Fin n → Fin k) => draws t) (learnedDrawPathKernel hk L z)

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

noncomputable def commonConfig {n k : ℕ} (S : Finset (Fin k)) (hne : S.Nonempty) : CandidateConfig n k

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

theorem learnedConfig_eq_common_on_good {n k T : ℕ} (hk : 1 < k) (S : Finset (Fin k)) (hne : S.Nonempty) (z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) (hz : z ∈ explorationGoodEvent (n := n) S) : learnedConfig hk z = commonConfig S hne

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

theorem learnedDrawPathKernel_on_good {n k T L : ℕ} (hk : 1 < k) (S : Finset (Fin k)) (hne : S.Nonempty) (z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) (hz : z ∈ explorationGoodEvent (n := n) S) : learnedDrawPathKernel hk L z = (FinitePMF.iid (jointDraw (fun _ : Fin n => S) (fun _ => hne)) L).toMeasure

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

noncomputable def explorationContinuationLaw {n k T : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) (L : ℕ) : Measure (((Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ)) × (Fin L → Fin n → Fin k))

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

theorem explorationContinuationLaw_fst_event {n k T L : ℕ} (hk : 1 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (E : Set ((Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ))) (hE : MeasurableSet E) : explorationContinuationLaw hk nu L (Prod.fst ⁻¹' E) = explorationRewardLaw (by omega) nu E

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

theorem explorationContinuationLaw_rectangle_on_good {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) (B : Set (Fin L → Fin n → Fin k)) : explorationContinuationLaw hk nu L (E ×ˢ B) = explorationRewardLaw (by omega) nu E * (FinitePMF.iid (jointDraw (fun _ : Fin n => S) (fun _ => hne)) L).toMeasure B

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

theorem explorationContinuationLaw_good_probability {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) : 1 - ENNReal.ofReal delta ≤ explorationContinuationLaw (by omega) nu L (Prod.fst ⁻¹' (explorationGoodEvent (n := n) (T := explorationLength k eps delta) (trueTopArms nu n)))

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

theorem trajectory_eq_of_prefix {n k : ℕ} (d e : ℕ → Fin n → Fin k) (t : ℕ) (h : ∀ u < t, d u = e u) : trajectory d t = trajectory e t

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

noncomputable def extendedCoordinationDraws {n k L : ℕ} (hk : 0 < 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.

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

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

theorem continuationAction_prefix {n k L : ℕ} (hk : 0 < k) (d e : Fin L → Fin n → Fin k) (t : Fin L) (h : ∀ u : Fin L, u ≤ t → d u = e u) : continuationAction hk d t = continuationAction hk e t

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

theorem continuationAction_fixed_stays {n k L : ℕ} (hk : 0 < k) (d : Fin L → Fin n → Fin k) (t : Fin L) (i : Fin n) (a : Fin k) (hs : trajectory (extendedCoordinationDraws hk d) t.val i = some a) : continuationAction hk d t i = a

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

theorem explorationGoodEvent_positive {n k : ℕ} (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) : 0 < explorationRewardLaw (by omega) nu (explorationGoodEvent (n := n) (T := explorationLength k eps delta) (trueTopArms nu n))

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

theorem explorationContinuationLaw_normalized_rectangle {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) (hpos : 0 < explorationRewardLaw (by omega) nu E) (B : Set (Fin L → Fin n → Fin k)) : explorationContinuationLaw hk nu L (E ×ˢ B) / explorationContinuationLaw hk nu L (Prod.fst ⁻¹' E) = (FinitePMF.iid (jointDraw (fun _ : Fin n => S) (fun _ => hne)) L).toMeasure B