BanditRLProof.Algorithms.HOOHistory

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

abbrev Observations

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

def expanded (h : Observations) : Finset Node

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

def visits (h : Observations) (v : Node) : ℕ

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

noncomputable def rewardSum (h : Observations) (v : Node) : ℝ

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

noncomputable def upper (ν ρ : ℝ) (h : Observations) (v : Node) : WithTop ℝ

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

noncomputable def next (ν ρ : ℝ) (h : Observations) : Node

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

noncomputable def step (ν ρ : ℝ) (h : Observations) (y : ℝ) : Observations

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

noncomputable def history (ν ρ : ℝ) (Y : ℕ → ℝ) : ℕ → Observations | 0 => [] | n+1 => step ν ρ (history ν ρ Y n) (Y n) noncomputable def action (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : Node

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

noncomputable def action (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : Node

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

@[simp] theorem step_length (ν ρ : ℝ) (h : Observations) (y : ℝ) : (step ν ρ h y).length = h.length + 1

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

@[simp] theorem history_length (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : (history ν ρ Y n).length = n

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

theorem expanded_step (ν ρ : ℝ) (h : Observations) (y : ℝ) : expanded (step ν ρ h y) = insert (next ν ρ h) (expanded h)

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

theorem next_not_expanded (ν ρ : ℝ) (h : Observations) : next ν ρ h ∉ expanded h

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

theorem next_ne_root (ν ρ : ℝ) (h : Observations) : next ν ρ h ≠ []

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

theorem next_not_previously_played (ν ρ : ℝ) (h : Observations) : next ν ρ h ∉ h.map Prod.fst

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

theorem visits_step (ν ρ : ℝ) (h : Observations) (y : ℝ) (v : Node) : visits (step ν ρ h y) v = visits h v + if v <+: next ν ρ h then 1 else 0

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

theorem rewardSum_step (ν ρ : ℝ) (h : Observations) (y : ℝ) (v : Node) : rewardSum (step ν ρ h y) v = rewardSum h v + if v <+: next ν ρ h then y else 0

Generated state uses only rewards strictly before the current round.

theorem history_causal (ν ρ : ℝ) (Y Z : ℕ → ℝ) (n : ℕ) (hYZ : ∀ i < n, Y i = Z i) : history ν ρ Y n = history ν ρ Z n

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

theorem action_causal (ν ρ : ℝ) (Y Z : ℕ → ℝ) (n : ℕ) (hYZ : ∀ i < n, Y i = Z i) : action ν ρ Y n = action ν ρ Z n

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

theorem expanded_card_history (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : (expanded (history ν ρ Y n)).card = n+1

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

theorem depthBound_history (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : depthBound (expanded (history ν ρ Y n)) ≤ n

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

theorem action_depth_le (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : (action ν ρ Y n).length ≤ n+1

The stored history is precisely the generated action/reward trace.

theorem history_eq_ofFn (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : history ν ρ Y n = List.ofFn (fun i : Fin n => (action ν ρ Y i, Y i))

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

theorem action_ne_of_lt (ν ρ : ℝ) (Y : ℕ → ℝ) {m n : ℕ} (hmn : m < n) : action ν ρ Y n ≠ action ν ρ Y m

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

theorem action_injective (ν ρ : ℝ) (Y : ℕ → ℝ) : Function.Injective (action ν ρ Y)