BanditRLProof.Algorithms.CUCBChargedConcentration

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

noncomputable def chargeValue (i : Fin m) (N : Fin m → ℕ) (z : Round A m) : ℝ

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

noncomputable def successValue (i : Fin m) (N : Fin m → ℕ) (z : Round A m) : ℝ

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

noncomputable def compensation (i : Fin m) (tilt : ℝ) (N : Fin m → ℕ) (z : Round A m) : ℝ

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

theorem exp_compensation (i : Fin m) (tilt : ℝ) (N : Fin m → ℕ) (z : Round A m) : Real.exp (C.compensation i tilt N z)=C.chargedTriggerFactor i tilt N z

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

theorem compensation_abs_le (i : Fin m) (tilt : ℝ) (N : Fin m → ℕ) (z : Round A m) : |C.compensation i tilt N z|≤|(1-Real.exp (-tilt))*C.triggerLower i|+|tilt|

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

theorem sum_chargeValue (actions : ℕ → Round A m) (n : ℕ) (i : Fin m) : (∑t∈Finset.range n, C.chargeValue i (C.counters (fun s => (actions s).1) t) (actions t)) = (C.counters (fun t => (actions t).1) n i : ℝ)

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

theorem sum_successValue (Y : ℕ → Round A m) (n : ℕ) (i : Fin m) : (∑t∈Finset.range n, C.successValue i (C.counters (fun s => (Y s).1) t) (Y t)) = (C.chargedObservations Y n i : ℝ)

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

theorem measurable_compensation (i : Fin m) (tilt : ℝ) : Measurable (fun p : (Fin m → ℕ) × Round A m => C.compensation i tilt p.1 p.2)

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

theorem integrable_exp_compensation {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν] (i : Fin m) (tilt scale : ℝ) (g : Ω → (Fin m → ℕ) × Round A m) (hg : Measurable g) : Integrable (fun ω => Real.exp (scale*C.compensation i tilt (g ω).1 (g ω).2)) ν

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

theorem measurable_counters_piLE (n : ℕ) : Measurable[Filtration.piLE n] (fun Y : ℕ → Round A m => C.counters (fun t => (Y t).1) n)

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

theorem compensation_adapted (i : Fin m) (tilt : ℝ) : StronglyAdapted Filtration.piLE (fun n (Y : ℕ → Round A m) => C.compensation i tilt (C.counters (fun t => (Y t).1) n) (Y n))

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

theorem charged_successor_condMGF (n : ℕ) (tilt : ℝ) (htilt : 0≤tilt) : Concentration.HasCondMGFUpperBoundAt (MeasurableSpace.comap (Preorder.frestrictLe n) inferInstance) (Preorder.measurable_frestrictLe n).comap_le (fun Y => C.compensation i tilt (C.counters (fun t => (Y t).1) (n+1)) (Y (n+1))) 1 0 (cucbTrajectory oracle environment)

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

theorem charged_initial_MGF (tilt : ℝ) (htilt : 0≤tilt) : Concentration.HasMGFUpperBoundAt (fun Y => C.compensation i tilt (C.counters (fun t => (Y t).1) 0) (Y 0)) 1 0 (cucbTrajectory oracle environment)

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

theorem charged_count_tail (n : ℕ) (tilt k budget : ℝ) (htilt : 0≤tilt) (hp : 0≤C.triggerLower i) : (cucbTrajectory oracle environment) {Y | k≤(C.counters (fun t => (Y t).1) n i : ℝ) ∧ (C.chargedObservations Y n i : ℝ)≤budget} ≤ ENNReal.ofReal (Real.exp (-((1-Real.exp (-tilt))*C.triggerLower i)*k+tilt*budget))

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

theorem observation_below_charged_half (n : ℕ) (k : ℝ) (hk : 0≤k) (hp : 0≤C.triggerLower i) : (cucbTrajectory oracle environment) {Y | k≤(C.counters (fun t => (Y t).1) n i : ℝ) ∧ (observationCount (fun t => (Y t).2) n i : ℝ)≤k*C.triggerLower i/2} ≤ ENNReal.ofReal (Real.exp (-k*C.triggerLower i/8))