BanditRLProof.Algorithms.HOOMeasurable

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

theorem measurable_backward {Ω : Type*} [MeasurableSpace Ω] (S : Finset Node) (U : Ω → Node → WithTop ℝ) (hU : ∀ v, Measurable (fun ω => U ω v)) (k : ℕ) (v : Node) : Measurable (fun ω => backward S (U ω) k v)

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

theorem measurable_walk {Ω : Type*} [MeasurableSpace Ω] (S : Finset Node) (B : Ω → Node → WithTop ℝ) (hB : ∀ v, Measurable (fun ω => B ω v)) (k : ℕ) (v : Node) : Measurable (fun ω => walk S (B ω) k v)

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

theorem measurable_select {Ω : Type*} [MeasurableSpace Ω] (S : Finset Node) (U : Ω → Node → WithTop ℝ) (hU : ∀ v, Measurable (fun ω => U ω v)) : Measurable (fun ω => select S (U ω))

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

theorem visits_ofFn {n : ℕ} (a : Fin n → Node) (r : Fin n → ℝ) (v : Node) : visits (List.ofFn (fun i => (a i, r i))) v = (List.ofFn a).countP (fun w => decide (v <+: w))

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

theorem expanded_ofFn {n : ℕ} (a : Fin n → Node) (r : Fin n → ℝ) : expanded (List.ofFn (fun i => (a i, r i))) = insert [] (List.ofFn a).toFinset

A genuine history-to-action map: discrete past nodes and real past rewards.

theorem measurable_next_ofFn (ν ρ : ℝ) (n : ℕ) : Measurable (fun p : (Fin n → Node) × (Fin n → ℝ) => next ν ρ (List.ofFn (fun i => (p.1 i, p.2 i))))

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

theorem measurable_action (ν ρ : ℝ) (n : ℕ) : Measurable (fun Y : ℕ → ℝ => action ν ρ Y n)