BanditRLProof.Algorithms.MusicalChairsExploration

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

noncomputable def iid {α : Type*} [Fintype α] (p : PMF α) (T : ℕ) : PMF (Fin T → α)

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

theorem iid_apply {α : Type*} [Fintype α] (p : PMF α) (T : ℕ) (x : Fin T → α) : iid p T x = ∏ t, p (x t)

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

theorem iid_product_expectation {α : Type*} [Fintype α] (p : PMF α) (T : ℕ) (f : Fin T → α → ℝ≥0∞) : ∑ x, iid p T x * ∏ t, f t (x t) = ∏ t, ∑ a, p a * f t a

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

noncomputable def eventCount {α : Type*} {T : ℕ} (E : Set α) (x : Fin T → α) : ℕ

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

theorem pow_eventCount {α : Type*} {T : ℕ} (E : Set α) (x : Fin T → α) (z : ℝ≥0∞) : z ^ eventCount E x = ∏ t, if x t ∈ E then z else 1

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

theorem indicator_weight_sum {α : Type*} [Fintype α] (p : PMF α) (E : Set α) (z : ℝ≥0∞) : ∑ a, p a * (if a ∈ E then z else 1) = p.toOuterMeasure E * z + p.toOuterMeasure Eᶜ

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

theorem iid_count_pgf {α : Type*} [Fintype α] (p : PMF α) (T : ℕ) (E : Set α) (z : ℝ≥0∞) : ∑ x, iid p T x * z ^ eventCount E x = (p.toOuterMeasure E * z + p.toOuterMeasure Eᶜ)^T

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

noncomputable def explorationDraw (n k : ℕ) (hk : 0 < k) : PMF (Fin n → Fin k)

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

noncomputable def explorationLaw (n k T : ℕ) (hk : 0 < k) : PMF (Fin T → Fin n → Fin k)

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

def observes {n k : ℕ} (i : Fin n) (a : Fin k) : Set (Fin n → Fin k)

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

theorem observes_rectangle {n k : ℕ} (i : Fin n) (a : Fin k) : observes i a = {draw | ∀ j, draw j ∈ isolationWindow i a j}

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

theorem exploration_observes_probability {n k : ℕ} (hk : 0 < k) (i : Fin n) (a : Fin k) : (explorationDraw n k hk).toOuterMeasure (observes i a) = (1 / (k : ℝ≥0∞)) * (((k-1 : ℕ) : ℝ≥0∞) / (k : ℝ≥0∞))^(n-1)

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

theorem exploration_collisionFree_split {n k : ℕ} (hk : 0 < k) (i : Fin n) : (explorationDraw n k hk).toOuterMeasure {draw | CollisionFree draw i} = ∑ a : Fin k, (explorationDraw n k hk).toOuterMeasure (observes i a)

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

theorem exploration_collisionFree_probability {n k : ℕ} (hk : 0 < k) (i : Fin n) : (explorationDraw n k hk).toOuterMeasure {draw | CollisionFree draw i} = (((k-1 : ℕ) : ℝ≥0∞) / (k : ℝ≥0∞))^(n-1)

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

theorem exploration_collision_probability {n k : ℕ} (hk : 0 < k) (i : Fin n) : (explorationDraw n k hk).toOuterMeasure {draw | ¬ CollisionFree draw i} = 1 - (((k-1 : ℕ) : ℝ≥0∞) / (k : ℝ≥0∞))^(n-1)

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

noncomputable def observationCount {n k T : ℕ} (i : Fin n) (a : Fin k) (x : Fin T → Fin n → Fin k) : ℕ

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

noncomputable def collisionCount {n k T : ℕ} (i : Fin n) (x : Fin T → Fin n → Fin k) : ℕ

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

theorem observationCount_pgf {n k : ℕ} (hk : 0 < k) (T : ℕ) (i : Fin n) (a : Fin k) (z : ℝ≥0∞) : let q := (1 / (k : ℝ≥0∞)) * (((k-1 : ℕ) : ℝ≥0∞) / (k : ℝ≥0∞))^(n-1) ∑ x, explorationLaw n k T hk x * z ^ observationCount i a x = (q * z + (1-q))^T

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

theorem collisionCount_pgf {n k : ℕ} (hk : 0 < k) (T : ℕ) (i : Fin n) (z : ℝ≥0∞) : let b := (((k-1 : ℕ) : ℝ≥0∞) / (k : ℝ≥0∞))^(n-1) ∑ x, explorationLaw n k T hk x * z ^ collisionCount i x = ((1-b) * z + b)^T

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

theorem exploration_observes_lower {n k : ℕ} (hk : 0 < k) (hnk : n ≤ k) (i : Fin n) (a : Fin k) : (1 : ℝ≥0∞) / (4*k) ≤ (explorationDraw n k hk).toOuterMeasure (observes i a)

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

theorem observationCount_laplace {n k : ℕ} (hk : 0 < k) (T : ℕ) (i : Fin n) (a : Fin k) (eta : ℝ) : let q := (1 / (k : ℝ≥0∞)) * (((k-1 : ℕ) : ℝ≥0∞) / (k : ℝ≥0∞))^(n-1) ∑ x, explorationLaw n k T hk x * ENNReal.ofReal (Real.exp (-eta * (observationCount i a x : ℝ))) = (q * ENNReal.ofReal (Real.exp (-eta)) + (1-q))^T

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

structure ExplorationFeedback (k : ℕ) where

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

noncomputable def explorationFeedback {n k T : ℕ} (x : Fin T → Fin n → Fin k) (rewards : Fin T → Fin k → ℝ) (i : Fin n) : Fin T → ExplorationFeedback k

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

noncomputable def localObservationCount {k T : ℕ} (f : Fin T → ExplorationFeedback k) (a : Fin k) : ℕ

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

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

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

noncomputable def localRewardSum {k T : ℕ} (f : Fin T → ExplorationFeedback k) (a : Fin k) : ℝ

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

noncomputable def localEmpiricalMean {k T : ℕ} (f : Fin T → ExplorationFeedback k) (a : Fin k) : ℝ

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

theorem localObservationCount_eq {n k T : ℕ} (x : Fin T → Fin n → Fin k) (rewards : Fin T → Fin k → ℝ) (i : Fin n) (a : Fin k) : localObservationCount (explorationFeedback x rewards i) a = observationCount i a x

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

theorem localCollisionCount_eq {n k T : ℕ} (x : Fin T → Fin n → Fin k) (rewards : Fin T → Fin k → ℝ) (i : Fin n) : localCollisionCount (explorationFeedback x rewards i) = collisionCount i x

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

theorem localRewardSum_eq {n k T : ℕ} (x : Fin T → Fin n → Fin k) (rewards : Fin T → Fin k → ℝ) (i : Fin n) (a : Fin k) : localRewardSum (explorationFeedback x rewards i) a = ∑ t ∈ Finset.univ.filter (fun t => x t ∈ observes i a), rewards t a