BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIConfidenceTuning

Fixed-tilt arithmetic used by the finite UCBVI confidence union.

Module map

Declarations
6
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVITransitionValueConfidence

Imported by

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVISimultaneousConfidence

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bernsteinTilt Compiled

Bernstein tilt optimized for a deterministic variance budget, totalized at zero variance.

noncomputable def bernsteinTilt (logBudget varianceBudget : Real) : Real
Source line 9 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bernsteinCoordinateThreshold Compiled

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

noncomputable def bernsteinCoordinateThreshold (logBudget varianceBudget : Real) : Real
Source line 13 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bernsteinTilt_pos Compiled

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

theorem bernsteinTilt_pos {logBudget varianceBudget : Real} (hlog : 0 < logBudget) (hvariance : 0 <= varianceBudget) : 0 < bernsteinTilt logBudget varianceBudget
Source line 17 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bernsteinTilt_le_one Compiled

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

theorem bernsteinTilt_le_one (logBudget varianceBudget : Real) : bernsteinTilt logBudget varianceBudget <= 1
Source line 28 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bernsteinTilt_abs_le_one Compiled

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

theorem bernsteinTilt_abs_le_one {logBudget varianceBudget : Real} (hlog : 0 < logBudget) (hvariance : 0 <= varianceBudget) : |bernsteinTilt logBudget varianceBudget| <= 1
Source line 34 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.bernsteinTilt_exponent_le Compiled

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

theorem bernsteinTilt_exponent_le {logBudget varianceBudget : Real} (hlog : 0 < logBudget) (hvariance : 0 <= varianceBudget) : -bernsteinTilt logBudget varianceBudget * bernsteinCoordinateThreshold logBudget varianceBudget + bernsteinTilt logBudget varianceBudget ^ 2 * varianceBudget <= -2 * logBudget
Source line 41 Chapter context: Finite-horizon RL