BanditRLProof.Algorithms.CUCBNiceEvent

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

noncomputable def confidenceRadius {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) (L : ℝ) : ℝ

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

theorem measurable_confidenceRadius {m : ℕ} (n : ℕ) (i : Fin m) (L : ℝ) : Measurable (fun Y : ℕ → Feedback m => confidenceRadius Y n i L)

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

theorem count_mul_radius (T L : ℝ) (hT : 0<T) (hL : 0≤L) : T*Real.sqrt (L/(2*T)) = Real.sqrt (T*L/2)

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

theorem empirical_bad_implies_deviation {A : Type*} {m : ℕ} (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (n : ℕ) (L : ℝ) (hL : 0≤L) (Y : ℕ → Round A m) (hbad : confidenceRadius (fun t => (Y t).2) n i L < |empiricalMean (fun t => (Y t).2) n i-marginalMean D|) : ∃ lower : Bool, 0<observationCount (fun t => (Y t).2) n i ∧ Real.sqrt ((observationCount (fun t => (Y t).2) n i : ℝ)*L/2) ≤ pathDeviation D i n lower Y

On the source confidence event the clipped index is optimistic, and its excess above the true mean is at most twice the clipped confidence radius.

theorem upperIndex_of_confidence {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) (μ : ℝ) (hμ : μ ∈ Set.Icc (0:ℝ) 1) (hgood : |empiricalMean Y n i-μ| ≤ confidenceRadius Y n i (3*Real.log ((n:ℝ)+1))) : μ ≤ upperIndex Y n i ∧ upperIndex Y n i ≤ μ+2*confidenceRadius Y n i (3*Real.log ((n:ℝ)+1))

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

theorem empirical_bad_probability (n : ℕ) (L : ℝ) (hL : 0≤L) : (cucbTrajectory oracle environment) {Y | confidenceRadius (fun t => (Y t).2) n i L < |empiricalMean (fun t => (Y t).2) n i-marginalMean D|} ≤ 2*(n:ENNReal)*ENNReal.ofReal (Real.exp (-L))

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

theorem round_confidence_arithmetic (n : ℕ) : 2*(n:ℝ)*Real.exp (-(3*Real.log ((n:ℝ)+1))) ≤ 2/((n:ℝ)+1)^2

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

theorem empirical_bad_probability_source (n : ℕ) : (cucbTrajectory oracle environment) {Y | confidenceRadius (fun t => (Y t).2) n i (3*Real.log ((n:ℝ)+1)) < |empiricalMean (fun t => (Y t).2) n i-marginalMean D|} ≤ ENNReal.ofReal (2/((n:ℝ)+1)^2)

Source nice event, before round `n+1`, simultaneously over all arms.

def NiceEvent (means : Fin m → ℝ) (n : ℕ) : Set (ℕ → Round A m)

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

theorem measurableSet_niceEvent (means : Fin m → ℝ) (n : ℕ) : MeasurableSet (NiceEvent (A:=A) means n)

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

theorem niceEvent_complement_probability (laws : Fin m → Measure UnitOutcome) [∀i, IsProbabilityMeasure (laws i)] (hcompatAll : ∀a i, ObservationCompatible (environment a) (laws i) i) (n : ℕ) : (cucbTrajectory oracle environment) (NiceEvent (fun i => marginalMean (laws i)) n)ᶜ ≤ ENNReal.ofReal (2*(m:ℝ)/((n:ℝ)+1)^2)