BanditRLProof.Algorithms.MusicalChairsPopulation

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

theorem base_gamma_upper {k : ℝ} (hk : 1 < k) : (1-1/k) ^ (2/5 : ℝ) ≤ 1 - (2/5 : ℝ)/k

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

theorem base_neg_gamma_lower {k : ℝ} (hk : 1 < k) : 1 + (2/5 : ℝ)/k ≤ (1-1/k) ^ (-(2/5 : ℝ))

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

theorem avoidanceBase_eq {k : ℕ} (hk : 0 < k) : (((k-1 : ℕ) : ℝ)/(k : ℝ)) = 1-1/(k : ℝ)

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

theorem avoidance_mass_lower {n k : ℕ} (hk : 1 < k) (hnk : n ≤ k) : (1/4 : ℝ) ≤ (1-1/(k : ℝ))^(n-1)

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

theorem collision_accuracy_sandwich {n k : ℕ} (hk : 1 < k) (hnk : n ≤ k) (pHat : ℝ) (hacc : |pHat-collisionProbReal n k| ≤ 1/(10*(k : ℝ))) : (1-1/(k : ℝ))^(n-1) * (1-1/(k : ℝ))^(2/5 : ℝ) ≤ 1-pHat ∧ 1-pHat ≤ (1-1/(k : ℝ))^(n-1) * (1-1/(k : ℝ))^(-(2/5 : ℝ))

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

theorem collision_accuracy_survival_pos {n k : ℕ} (hk : 1 < k) (hnk : n ≤ k) (pHat : ℝ) (hacc : |pHat-collisionProbReal n k| ≤ 1/(10*(k : ℝ))) : 0 < 1-pHat

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

theorem population_inverse_margin {n k : ℕ} (hn : 0 < n) (hk : 1 < k) (hnk : n ≤ k) (pHat : ℝ) (hacc : |pHat-collisionProbReal n k| ≤ 1/(10*(k : ℝ))) : (n : ℝ)-(2/5 : ℝ) ≤ 1+Real.log (1-pHat)/Real.log (1-1/(k : ℝ)) ∧ 1+Real.log (1-pHat)/Real.log (1-1/(k : ℝ)) ≤ (n : ℝ)+(2/5 : ℝ)

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

theorem population_inverse_round {n k : ℕ} (hn : 0 < n) (hk : 1 < k) (hnk : n ≤ k) (pHat : ℝ) (hacc : |pHat-collisionProbReal n k| ≤ 1/(10*(k : ℝ))) : round (1+Real.log (1-pHat)/Real.log (1-1/(k : ℝ))) = (n : ℤ)

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

noncomputable def populationInverse (k T C : ℕ) : ℝ

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

noncomputable def populationEstimate (k T C : ℕ) : ℕ

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

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

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

theorem localCollisionCount_le {k T : ℕ} (f : Fin T → ExplorationFeedback k) : localCollisionCount f ≤ T

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

theorem noncollision_fraction_eq {T C : ℕ} (hT : 0 < T) (hC : C ≤ T) : (((T-C : ℕ) : ℝ)/(T : ℝ)) = 1-(C : ℝ)/(T : ℝ)

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

theorem populationInverse_ge_one {k T C : ℕ} (hk : 1 < k) (hC : C < T) : 1 ≤ populationInverse k T C

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

theorem populationEstimate_le (k T C : ℕ) : populationEstimate k T C ≤ k

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

theorem populationEstimate_all_collision (k T : ℕ) : populationEstimate k T T = k

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

theorem populationEstimate_zero_collision {k T : ℕ} (hk : 0 < k) (hT : 0 < T) : populationEstimate k T 0 = 1

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

theorem populationEstimate_correct {n k T C : ℕ} (hn : 0 < n) (hk : 1 < k) (hnk : n ≤ k) (hT : 0 < T) (hC : C ≤ T) (hacc : |(C : ℝ)/T-collisionProbReal n k| ≤ 1/(10*(k : ℝ))) : populationEstimate k T C = n

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

theorem localPopulationEstimate_correct {n k T : ℕ} (hn : 0 < n) (hk : 1 < k) (hnk : n ≤ k) (hT : 0 < T) (f : Fin T → ExplorationFeedback k) (hacc : |(localCollisionCount f : ℝ)/T-collisionProbReal n k| ≤ 1/(10*(k : ℝ))) : localPopulationEstimate f = n

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

theorem populationEstimate_regular_cast {k T C : ℕ} (hk : 1 < k) (hC : C < T) : (populationEstimate k T C : ℤ) = min (k : ℤ) (round (populationInverse k T C))

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

theorem collisionCount_le {n k T : ℕ} (x : Fin T → Fin n → Fin k) (i : Fin n) : collisionCount i x ≤ T

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

theorem localPopulationEstimate_eq {n k T : ℕ} (x : Fin T → Fin n → Fin k) (r : Fin T → Fin k → ℝ) (i : Fin n) : localPopulationEstimate (explorationFeedback x r i) = populationEstimate k T (collisionCount i x)

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

def populationRecovered {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_subset_populationRecovered {n k T : ℕ} (hn : 0 < n) (hk : 1 < k) (hnk : n ≤ k) (hT : 0 < T) : allCollisionAccurate (n := n) (k := k) (T := T) ⊆ populationRecovered

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

theorem populationRecovered_probability {n k T : ℕ} (hn : 0 < n) (hk : 1 < 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 (by omega)).toMeasure (populationRecovered (n := n) (k := k) (T := T))

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

def explorationEstimatesCorrect {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 explorationEstimatesCorrect_eq_inter {n k T : ℕ} (nu : Fin k → Measure ℝ) (eps : ℝ) : explorationEstimatesCorrect (n := n) (T := T) nu eps = allMeanAccurate nu eps ∩ Prod.fst ⁻¹' populationRecovered

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

theorem measurableSet_explorationEstimatesCorrect {n k T : ℕ} (nu : Fin k → Measure ℝ) (eps : ℝ) : MeasurableSet (explorationEstimatesCorrect (n := n) (T := T) nu eps)

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

theorem explorationStatisticsAccurate_subset_estimatesCorrect {n k T : ℕ} (hn : 0 < n) (hk : 1 < k) (hnk : n ≤ k) (hT : 0 < T) (nu : Fin k → Measure ℝ) (eps : ℝ) : explorationStatisticsAccurate (n := n) (T := T) nu eps ⊆ explorationEstimatesCorrect nu eps

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

theorem explorationEstimatesCorrect_probability {n k : ℕ} (hn : 0 < n) (hk : 1 < 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 (by omega) nu (explorationEstimatesCorrect (n := n) (T := explorationLength k eps delta) nu eps)