BanditRLProof.Algorithms.MusicalChairsRanking

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

def scoreOrder {k : ℕ} (score : Fin k → ℝ) (a b : Fin k) : Prop

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

noncomputable def rankedArms {k : ℕ} (score : Fin k → ℝ) : List (Fin k)

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

noncomputable def topArms {k : ℕ} (score : Fin k → ℝ) (n : ℕ) : Finset (Fin k)

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

theorem topArms_card {k : ℕ} (score : Fin k → ℝ) (n : ℕ) : (topArms score n).card = min n k

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

theorem topArms_before_unselected {k : ℕ} (score : Fin k → ℝ) (n : ℕ) {a b : Fin k} (ha : a ∈ topArms score n) (hb : b ∉ topArms score n) : scoreOrder score a b

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

theorem topArms_eq_of_order_separated {k : ℕ} (score : Fin k → ℝ) (n : ℕ) (S : Finset (Fin k)) (hcard : S.card = n) (hnk : n ≤ k) (hsep : ∀ a ∈ S, ∀ b ∉ S, scoreOrder score a b) : topArms score n = S

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

theorem topArms_eq_of_strict_separation {k : ℕ} (score : Fin k → ℝ) (n : ℕ) (S : Finset (Fin k)) (hcard : S.card = n) (hnk : n ≤ k) (hsep : ∀ a ∈ S, ∀ b ∉ S, score b < score a) : topArms score n = S

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

theorem topArms_eq_iff {k : ℕ} (score : Fin k → ℝ) (n : ℕ) (hnk : n ≤ k) (S : Finset (Fin k)) : topArms score n = S ↔ S.card = n ∧ ∀ a ∈ S, ∀ b ∉ S, scoreOrder score a b

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

theorem populationEstimate_pos {k T C : ℕ} (hk : 1 < k) (hC : C ≤ T) : 0 < populationEstimate k T C

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

noncomputable def localCandidateSet {k T : ℕ} (f : Fin T → ExplorationFeedback k) : Finset (Fin k)

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

theorem localCandidateSet_card {k T : ℕ} (f : Fin T → ExplorationFeedback k) : (localCandidateSet f).card = localPopulationEstimate f

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

theorem localCandidateSet_nonempty {k T : ℕ} (hk : 1 < k) (f : Fin T → ExplorationFeedback k) : (localCandidateSet f).Nonempty

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

theorem empirical_strict_separation {k : ℕ} (mu score : Fin k → ℝ) (S : Finset (Fin k)) (eps gap : ℝ) (hepsgap : eps < gap) (hgap : ∀ a ∈ S, ∀ b ∉ S, gap ≤ mu a - mu b) (hacc : ∀ a, |score a-mu a| < eps/2) : ∀ a ∈ S, ∀ b ∉ S, score b < score a

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

theorem localCandidateSet_correct {n k T : ℕ} (f : Fin T → ExplorationFeedback k) (mu : Fin k → ℝ) (S : Finset (Fin k)) (hcard : S.card = n) (hnk : n ≤ k) (eps gap : ℝ) (hepsgap : eps < gap) (hgap : ∀ a ∈ S, ∀ b ∉ S, gap ≤ mu a - mu b) (hacc : ∀ a, |localEmpiricalMean f a-mu a| < eps/2) (hpop : localPopulationEstimate f = n) : localCandidateSet f = S

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

theorem localCandidateSet_eq_iff {k T : ℕ} (f : Fin T → ExplorationFeedback k) (S : Finset (Fin k)) : localCandidateSet f = S ↔ S.card = localPopulationEstimate f ∧ ∀ a ∈ S, ∀ b ∉ S, scoreOrder (localEmpiricalMean f) a b

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

theorem measurableSet_localScoreOrder {n k T : ℕ} (i : Fin n) (a b : Fin k) : MeasurableSet {z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ) | scoreOrder (localEmpiricalMean (explorationFeedback z.1 z.2 i)) a b}

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

def explorationGoodEvent {n k T : ℕ} (S : Finset (Fin k)) : Set ((Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ))

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

theorem explorationGoodEvent_eq_comparisons {n k T : ℕ} (S : Finset (Fin k)) (hcard : S.card = n) : explorationGoodEvent (n := n) (T := T) S = (Prod.fst ⁻¹' populationRecovered) ∩ {z | ∀ i : Fin n, ∀ a ∈ S, ∀ b ∉ S, scoreOrder (localEmpiricalMean (explorationFeedback z.1 z.2 i)) a b}

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

theorem measurableSet_explorationGoodEvent {n k T : ℕ} (S : Finset (Fin k)) (hcard : S.card = n) : MeasurableSet (explorationGoodEvent (n := n) (T := T) S)

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

theorem explorationEstimatesCorrect_subset_goodEvent {n k T : ℕ} (nu : Fin k → Measure ℝ) (S : Finset (Fin k)) (hcard : S.card = n) (hnk : n ≤ k) (eps gap : ℝ) (hepsgap : eps < gap) (hgap : ∀ a ∈ S, ∀ b ∉ S, gap ≤ armMean nu a - armMean nu b) : explorationEstimatesCorrect (n := n) (T := T) nu eps ⊆ explorationGoodEvent S

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

noncomputable def trueTopArms {k : ℕ} (nu : Fin k → Measure ℝ) (n : ℕ) : Finset (Fin k)

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

theorem trueTopArms_eq_of_gap {n k : ℕ} (nu : Fin k → Measure ℝ) (S : Finset (Fin k)) (hcard : S.card = n) (hnk : n ≤ k) (gap : ℝ) (hgap0 : 0 < gap) (hgap : ∀ a ∈ S, ∀ b ∉ S, gap ≤ armMean nu a - armMean nu b) : trueTopArms nu n = S

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

theorem explorationGoodEvent_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) (S : Finset (Fin k)) (hcard : S.card = n) (eps gap delta : ℝ) (heps : 0 < eps) (heps1 : eps ≤ 1) (hepsgap : eps < gap) (hgap : ∀ a ∈ S, ∀ b ∉ S, gap ≤ armMean nu a - armMean nu b) (hdelta : 0 < delta) (hdelta1 : delta < 1) : 1 - ENNReal.ofReal delta ≤ explorationRewardLaw (by omega) nu (explorationGoodEvent (n := n) (T := explorationLength k eps delta) S)

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

theorem explorationGoodEvent_trueTop_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) (S : Finset (Fin k)) (hcard : S.card = n) (eps gap delta : ℝ) (heps : 0 < eps) (heps1 : eps ≤ 1) (hepsgap : eps < gap) (hgap : ∀ a ∈ S, ∀ b ∉ S, gap ≤ armMean nu a - armMean nu b) (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 armMean_mem_unitInterval {k : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (a : Fin k) : armMean nu a ∈ Set.Icc (0 : ℝ) 1

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

theorem separating_gap_le_one {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) (S : Finset (Fin k)) (hcard : S.card = n) (gap : ℝ) (hgap : ∀ a ∈ S, ∀ b ∉ S, gap ≤ armMean nu a - armMean nu b) : gap ≤ 1

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

theorem source_exploration_good_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) (S : Finset (Fin k)) (hcard : S.card = n) (eps gap delta : ℝ) (heps : 0 < eps) (hepsgap : eps < gap) (hgap : ∀ a ∈ S, ∀ b ∉ S, gap ≤ armMean nu a - armMean nu b) (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))