BanditRLProof.Algorithms.MusicalChairsCollision

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

theorem iid_toMeasure_pi {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (T : ℕ) : (iid p T).toMeasure = Measure.pi (fun _ : Fin T => p.toMeasure)

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

noncomputable def eventIndicator {α : Type*} (E : Set α) (a : α) : ℝ

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

theorem eventIndicator_mean {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (E : Set α) : (∫ a, eventIndicator E a ∂p.toMeasure) = p.toMeasure.real E

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

theorem iid_indicator_mean {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (E : Set α) {T : ℕ} (t : Fin T) : (∫ x, eventIndicator E (x t) ∂(iid p T).toMeasure) = p.toMeasure.real E

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

theorem iid_indicator_subGaussian {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (E : Set α) {T : ℕ} (t : Fin T) : HasSubgaussianMGF (fun x => eventIndicator E (x t) - p.toMeasure.real E) (1/4 : NNReal) (iid p T).toMeasure

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

theorem iid_indicator_independent {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (E : Set α) (T : ℕ) : iIndepFun (fun t (x : Fin T → α) => eventIndicator E (x t) - p.toMeasure.real E) (iid p T).toMeasure

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

theorem eventCount_eq_sum {α : Type*} {T : ℕ} (E : Set α) (x : Fin T → α) : (eventCount E x : ℝ) = ∑ t, eventIndicator E (x t)

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

theorem iid_centered_sum_subGaussian {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (E : Set α) (T : ℕ) : HasSubgaussianMGF (fun x : Fin T → α => ∑ t, (eventIndicator E (x t) - p.toMeasure.real E)) ((T : NNReal)/4) (iid p T).toMeasure

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

theorem iid_centered_sum_abs_tail {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (E : Set α) (T : ℕ) (u : ℝ) (hu : 0 ≤ u) : (iid p T).toMeasure.real {x | u ≤ |∑ t, (eventIndicator E (x t) - p.toMeasure.real E)|} ≤ 2 * Real.exp (-u^2 / (2 * ((T : ℝ)/4)))

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

theorem iid_frequency_tail {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (E : Set α) {T : ℕ} (hT : 0 < T) (eta : ℝ) (heta : 0 ≤ eta) : (iid p T).toMeasure.real {x | eta ≤ |(eventCount E x : ℝ)/T - p.toMeasure.real E|} ≤ 2 * Real.exp (-2 * T * eta^2)

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

noncomputable def collisionProbReal (n k : ℕ) : ℝ

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

theorem collision_indicator_mean {n k : ℕ} (hk : 0 < k) (i : Fin n) : (explorationDraw n k hk).toMeasure.real {draw | ¬ CollisionFree draw i} = collisionProbReal n k

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

noncomputable def localCollisionRate {n k T : ℕ} (x : Fin T → Fin n → Fin k) (r : Fin T → Fin k → ℝ) (i : Fin n) : ℝ

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

theorem localCollisionRate_eq {n k T : ℕ} (x : Fin T → Fin n → Fin k) (r : Fin T → Fin k → ℝ) (i : Fin n) : localCollisionRate x r i = (collisionCount i x : ℝ)/T

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

def collisionBadEvent {n k T : ℕ} (i : Fin n) : Set (Fin T → Fin n → Fin k)

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

theorem collisionBadEvent_bound {n k T : ℕ} (hk : 0 < k) (hT : 0 < T) (i : Fin n) : (explorationLaw n k T hk).toMeasure (collisionBadEvent (k := k) (T := T) i) ≤ ENNReal.ofReal (2 * Real.exp (-(T : ℝ)/(50*(k : ℝ)^2)))

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

def allCollisionBadEvent {n k T : ℕ} : Set (Fin T → Fin n → Fin k)

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

theorem allCollisionBadEvent_bound {n k T : ℕ} (hk : 0 < k) (hnk : n ≤ k) (hT : 0 < T) : (explorationLaw n k T hk).toMeasure (allCollisionBadEvent (n := n) (k := k) (T := T)) ≤ ENNReal.ofReal (2*(k : ℝ)*Real.exp (-(T : ℝ)/(50*(k : ℝ)^2)))

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

theorem collision_exploration_threshold (k T : ℕ) (hk : 0 < k) (delta : ℝ) (hdelta : 0 < delta) (hT : (50*(k : ℝ)^2) * Real.log (4*(k : ℝ)/delta) ≤ T) : 2*(k : ℝ) * Real.exp (-(T : ℝ)/(50*(k : ℝ)^2)) ≤ delta/2

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

theorem allCollisionBadEvent_le_half_delta {n k T : ℕ} (hk : 0 < k) (hnk : n ≤ k) (hT : 0 < T) (delta : ℝ) (hdelta : 0 < delta) (hbudget : (50*(k : ℝ)^2) * Real.log (4*(k : ℝ)/delta) ≤ T) : (explorationLaw n k T hk).toMeasure (allCollisionBadEvent (n := n) (k := k) (T := T)) ≤ ENNReal.ofReal (delta/2)

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

def allCollisionAccurate {n k T : ℕ} : Set (Fin T → Fin n → Fin k)

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

theorem allCollisionAccurate_eq_compl {n k T : ℕ} : allCollisionAccurate (n := n) (k := k) (T := T) = (allCollisionBadEvent)ᶜ

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

theorem allCollisionAccurate_probability {n k T : ℕ} (hk : 0 < k) (hnk : n ≤ k) (hT : 0 < T) (delta : ℝ) (hdelta : 0 < delta) (hbudget : (50*(k : ℝ)^2) * Real.log (4*(k : ℝ)/delta) ≤ T) : 1 - ENNReal.ofReal (delta/2) ≤ (explorationLaw n k T hk).toMeasure (allCollisionAccurate (n := n) (k := k) (T := T))

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

theorem explorationRewardLaw_fst_event {n k T : ℕ} (hk : 0 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (E : Set (Fin T → Fin n → Fin k)) : explorationRewardLaw hk nu (Prod.fst ⁻¹' E) = (explorationLaw n k T hk).toMeasure E

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

def statisticsBadEvent {n k T : ℕ} (nu : Fin k → Measure ℝ) (eps : ℝ) : 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 statisticsBadEvent_le_delta {n k T : ℕ} (hk : 0 < k) (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) (heps1 : eps ≤ 1) (hdelta : 0 < delta) (hT : 0 < T) (hmeans : (16*(k : ℝ)/eps^2) * Real.log (4*(k : ℝ)^2/delta) ≤ T) (hcoll : (50*(k : ℝ)^2) * Real.log (4*(k : ℝ)/delta) ≤ T) : explorationRewardLaw hk nu (statisticsBadEvent (n := n) (T := T) nu eps) ≤ ENNReal.ofReal delta

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

def explorationStatisticsAccurate {n k T : ℕ} (nu : Fin k → Measure ℝ) (eps : ℝ) : 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 explorationStatisticsAccurate_eq_compl {n k T : ℕ} (nu : Fin k → Measure ℝ) (eps : ℝ) : explorationStatisticsAccurate (n := n) (T := T) nu eps = (statisticsBadEvent nu eps)ᶜ

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

theorem explorationStatisticsAccurate_probability {n k T : ℕ} (hk : 0 < k) (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) (heps1 : eps ≤ 1) (hdelta : 0 < delta) (hT : 0 < T) (hmeans : (16*(k : ℝ)/eps^2) * Real.log (4*(k : ℝ)^2/delta) ≤ T) (hcoll : (50*(k : ℝ)^2) * Real.log (4*(k : ℝ)/delta) ≤ T) : 1 - ENNReal.ofReal delta ≤ explorationRewardLaw hk nu (explorationStatisticsAccurate (n := n) (T := T) nu eps)

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

noncomputable def explorationLength (k : ℕ) (eps delta : ℝ) : ℕ

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

theorem explorationLength_mean_budget (k : ℕ) (eps delta : ℝ) : (16*(k : ℝ)/eps^2) * Real.log (4*(k : ℝ)^2/delta) ≤ explorationLength k eps delta

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

theorem explorationLength_collision_budget (k : ℕ) (eps delta : ℝ) : (50*(k : ℝ)^2) * Real.log (4*(k : ℝ)/delta) ≤ explorationLength k eps delta

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

theorem explorationLength_pos {k : ℕ} (hk : 0 < k) (eps delta : ℝ) (hdelta : 0 < delta) (hdelta1 : delta < 1) : 0 < explorationLength k eps delta

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

theorem explorationStatisticsAccurate_at_explorationLength {n k : ℕ} (hk : 0 < k) (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) (heps1 : eps ≤ 1) (hdelta : 0 < delta) (hdelta1 : delta < 1) : 1 - ENNReal.ofReal delta ≤ explorationRewardLaw hk nu (explorationStatisticsAccurate (n := n) (T := explorationLength k eps delta) nu eps)