BanditRLProof.Algorithms.CUCBFeedbackModel

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

structure FeedbackModel (A : Type*) [MeasurableSpace A] (m : ℕ) where

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

noncomputable def trueInput : Input m

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

noncomputable def expectedReward (a : A) : ℝ

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

noncomputable def triggerProbability (a : A) (i : Fin m) : ℝ

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

theorem expectedReward_nonneg (a : A) : 0≤M.expectedReward a

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

theorem triggerProbability_le_one (a : A) (i : Fin m) : M.triggerProbability a i≤1

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

theorem triggerProbability_pos (a : A) (i : Fin m) (hi : i∈M.possible a) : 0<M.triggerProbability a i

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

noncomputable def triggerActions (i : Fin m) : Finset A

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

theorem mem_triggerActions (a : A) (i : Fin m) : a∈M.triggerActions i ↔ i∈M.possible a

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

theorem triggerActions_nonempty (i : Fin m) : (M.triggerActions i).Nonempty

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

noncomputable def minTrigger (i : Fin m) : ℝ

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

theorem minTrigger_pos (i : Fin m) : 0<M.minTrigger i

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

theorem minTrigger_le (a : A) (i : Fin m) (hi : i∈M.possible a) : M.minTrigger i≤M.triggerProbability a i

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

theorem minTrigger_le_one (i : Fin m) : M.minTrigger i≤1

Source gaps will supply the two analysis fields; the trigger lower bound is already fixed to the actual environment minimum, with its proof below.

noncomputable def chargeData (bad : A → Bool) (inverseGap : A → ℝ) : ChargeData A m where

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

theorem chargeData_trigger_bound (bad : A → Bool) (inverseGap : A → ℝ) (i : Fin m) : ∀a, i∈(M.chargeData bad inverseGap).triggers a → (M.chargeData bad inverseGap).triggerLower i≤(M.environment a (observedSet i)).toReal

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

theorem deterministic_counter_bound (oracle : Kernel (Input m) A) [IsMarkovKernel oracle] (bad : A → Bool) (inverseGap : A → ℝ) (i : Fin m) (hp : M.minTrigger i=1) : ∀ᵐ Y ∂cucbTrajectory oracle M.environment, ∀n, (M.chargeData bad inverseGap).counters (fun t => (Y t).1) n i≤ observationCount (fun t => (Y t).2) n i

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

theorem charged_observation_tail (oracle : Kernel (Input m) A) [IsMarkovKernel oracle] (bad : A → Bool) (inverseGap : A → ℝ) (i : Fin m) (n : ℕ) (k : ℝ) (hk : 0≤k) : (cucbTrajectory oracle M.environment) {Y | k≤((M.chargeData bad inverseGap).counters (fun t => (Y t).1) n i : ℝ) ∧ (observationCount (fun t => (Y t).2) n i : ℝ)≤k*M.minTrigger i/2} ≤ ENNReal.ofReal (Real.exp (-k*M.minTrigger i/8))

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

theorem nice_event_probability (oracle : Kernel (Input m) A) [IsMarkovKernel oracle] (n : ℕ) : (cucbTrajectory oracle M.environment) (NiceEvent (fun i => (M.trueInput i:ℝ)) n)ᶜ ≤ ENNReal.ofReal (2*(m:ℝ)/((n:ℝ)+1)^2)