BanditRLProof.Algorithms.MusicalChairsReward

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

noncomputable def rewardLaw {k : ℕ} (nu : Fin k → Measure ℝ) (T : ℕ) : Measure (Fin T → Fin k → ℝ)

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

noncomputable def armMean {k : ℕ} (nu : Fin k → Measure ℝ) (a : Fin k) : ℝ

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

theorem reward_coordinate_preserving {k T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (t : Fin T) (a : Fin k) : MeasurePreserving (fun r : Fin T → Fin k → ℝ => r t a) (rewardLaw nu T) (nu a)

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

theorem reward_coordinate_mean {k T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (t : Fin T) (a : Fin k) : (∫ r, r t a ∂rewardLaw nu T) = armMean nu a

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

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

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

theorem reward_coordinate_subGaussian {k T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (t : Fin T) (a : Fin k) : HasSubgaussianMGF (fun r : Fin T → Fin k → ℝ => r t a - armMean nu a) (1/4 : NNReal) (rewardLaw nu T)

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

theorem reward_time_independent {k T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (a : Fin k) : iIndepFun (fun t (r : Fin T → Fin k → ℝ) => r t a - armMean nu a) (rewardLaw nu T)

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

theorem selected_sum_subGaussian {k T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (S : Finset (Fin T)) (a : Fin k) : HasSubgaussianMGF (fun r : Fin T → Fin k → ℝ => ∑ t ∈ S, (r t a - armMean nu a)) ((S.card : NNReal)/4) (rewardLaw nu T)

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

theorem selected_sum_abs_tail {k T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (S : Finset (Fin T)) (a : Fin k) (u : ℝ) (hu : 0 ≤ u) : (rewardLaw nu T).real {r | u ≤ |∑ t ∈ S, (r t a - armMean nu a)|} ≤ 2 * Real.exp (-u^2 / (2 * ((S.card : ℝ)/4)))

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

noncomputable def selectedMean {k T : ℕ} (S : Finset (Fin T)) (a : Fin k) (r : Fin T → Fin k → ℝ) : ℝ

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

theorem selected_centered_sum {k T : ℕ} (nu : Fin k → Measure ℝ) (S : Finset (Fin T)) (a : Fin k) (hS : 0 < S.card) (r : Fin T → Fin k → ℝ) : (∑ t ∈ S, (r t a - armMean nu a)) = (S.card : ℝ) * (selectedMean S a r - armMean nu a)

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

theorem selectedMean_tail_pos {k T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (S : Finset (Fin T)) (a : Fin k) (hS : 0 < S.card) (eps : ℝ) (heps : 0 ≤ eps) : (rewardLaw nu T).real {r | eps/2 ≤ |selectedMean S a r - armMean nu a|} ≤ 2 * Real.exp (-(S.card : ℝ) * eps^2 / 2)

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

theorem selectedMean_tail {k T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (S : Finset (Fin T)) (a : Fin k) (eps : ℝ) (heps : 0 ≤ eps) : (rewardLaw nu T).real {r | eps/2 ≤ |selectedMean S a r - armMean nu a|} ≤ 2 * Real.exp (-(S.card : ℝ) * eps^2 / 2)

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

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

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

theorem localEmpiricalMean_eq_selectedMean {n k T : ℕ} (x : Fin T → Fin n → Fin k) (r : Fin T → Fin k → ℝ) (i : Fin n) (a : Fin k) : localEmpiricalMean (explorationFeedback x r i) a = selectedMean (observedTimes x i a) a r

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

theorem localEmpiricalMean_fixed_tail {n k T : ℕ} (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (x : Fin T → Fin n → Fin k) (i : Fin n) (a : Fin k) (eps : ℝ) (heps : 0 ≤ eps) : (rewardLaw nu T).real {r | eps/2 ≤ |localEmpiricalMean (explorationFeedback x r i) a - armMean nu a|} ≤ 2 * Real.exp (-(observationCount i a x : ℝ) * eps^2 / 2)

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

theorem measurable_selectedMean {k T : ℕ} (S : Finset (Fin T)) (a : Fin k) : Measurable (selectedMean S a)

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

theorem measurable_jointEmpiricalMean {n k T : ℕ} (i : Fin n) (a : Fin k) : Measurable (fun z : (Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ) => localEmpiricalMean (explorationFeedback z.1 z.2 i) a)

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

noncomputable def explorationRewardLaw {n k T : ℕ} (hk : 0 < k) (nu : Fin k → Measure ℝ) : Measure ((Fin T → Fin n → Fin k) × (Fin T → Fin k → ℝ))

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

def meanBadEvent {n k T : ℕ} (nu : Fin k → Measure ℝ) (i : Fin n) (a : Fin k) (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 measurableSet_meanBadEvent {n k T : ℕ} (nu : Fin k → Measure ℝ) (i : Fin n) (a : Fin k) (eps : ℝ) : MeasurableSet (meanBadEvent (T := T) nu i a eps)

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

theorem meanBadEvent_mixture {n k T : ℕ} (hk : 0 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (i : Fin n) (a : Fin k) (eps : ℝ) : explorationRewardLaw hk nu (meanBadEvent (T := T) nu i a eps) = ∑ x, explorationLaw n k T hk x * rewardLaw nu T {r | eps/2 ≤ |localEmpiricalMean (explorationFeedback x r i) a - armMean nu a|}

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

theorem meanBadEvent_count_bound {n k T : ℕ} (hk : 0 < k) (nu : Fin k → Measure ℝ) [∀ a, IsProbabilityMeasure (nu a)] (hb : ∀ a, ∀ᵐ y ∂nu a, y ∈ Set.Icc (0 : ℝ) 1) (i : Fin n) (a : Fin k) (eps : ℝ) (heps : 0 ≤ eps) : let q := (1 / (k : ℝ≥0∞)) * (((k-1 : ℕ) : ℝ≥0∞) / (k : ℝ≥0∞))^(n-1) explorationRewardLaw hk nu (meanBadEvent (T := T) nu i a eps) ≤ 2 * (q * ENNReal.ofReal (Real.exp (-(eps^2/2))) + (1-q))^T

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

theorem half_le_one_sub_exp_neg (x : ℝ) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : x/2 ≤ 1 - Real.exp (-x)

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

theorem count_mixture_exp_bound (q eps : ℝ) (T : ℕ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) (heps0 : 0 ≤ eps) (heps1 : eps ≤ 1) : (q * Real.exp (-(eps^2/2)) + (1-q))^T ≤ Real.exp (-(T : ℝ)*q*eps^2/4)

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

noncomputable def explorationProbReal (n k : ℕ) : ℝ

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

theorem explorationProbReal_nonneg (n k : ℕ) : 0 ≤ explorationProbReal n k

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

theorem explorationProbReal_le_one (n k : ℕ) (hk : 0 < k) : explorationProbReal n k ≤ 1

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

theorem explorationProbReal_lower (n k : ℕ) (hk : 0 < k) (hnk : n ≤ k) : (1 : ℝ)/(4*k) ≤ explorationProbReal n k

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

theorem ofReal_explorationProbReal (n k : ℕ) (hk : 0 < k) : ENNReal.ofReal (explorationProbReal n k) = (1/(k : ℝ≥0∞)) * (((k-1 : ℕ) : ℝ≥0∞)/(k : ℝ≥0∞))^(n-1)

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

theorem meanBadEvent_exponential_bound {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) (i : Fin n) (a : Fin k) (eps : ℝ) (heps0 : 0 ≤ eps) (heps1 : eps ≤ 1) : explorationRewardLaw hk nu (meanBadEvent (T := T) nu i a eps) ≤ ENNReal.ofReal (2 * Real.exp (-(T : ℝ)*eps^2/(16*k)))

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

def allMeanBadEvent {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 allMeanBadEvent_exponential_bound {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 : ℝ) (heps0 : 0 ≤ eps) (heps1 : eps ≤ 1) : explorationRewardLaw hk nu (allMeanBadEvent (n := n) (T := T) nu eps) ≤ ENNReal.ofReal (2 * (k : ℝ)^2 * Real.exp (-(T : ℝ)*eps^2/(16*k)))

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

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

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

theorem allMeanBadEvent_le_half_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 : (16*(k : ℝ)/eps^2) * Real.log (4*(k : ℝ)^2/delta) ≤ T) : explorationRewardLaw hk nu (allMeanBadEvent (n := n) (T := T) nu eps) ≤ ENNReal.ofReal (delta/2)

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

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

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

theorem allMeanAccurate_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 : (16*(k : ℝ)/eps^2) * Real.log (4*(k : ℝ)^2/delta) ≤ T) : 1 - ENNReal.ofReal (delta/2) ≤ explorationRewardLaw hk nu (allMeanAccurate (n := n) (T := T) nu eps)