BanditRLProof.Algorithms.HOOTrajectory

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

def prefixExtension (n : ℕ) (h : (i : Finset.Iic n) → ℝ) : ℕ → ℝ

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

theorem measurable_prefixExtension (n : ℕ) : Measurable (prefixExtension n)

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

theorem action_prefixExtension (ν ρ : ℝ) (Y : ℕ → ℝ) (n : ℕ) : action ν ρ (prefixExtension n (Preorder.frestrictLe n Y)) (n+1) = action ν ρ Y (n+1)

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

noncomputable def stepKernel (ν ρ : ℝ) (law : Kernel Node ℝ) (n : ℕ) : Kernel ((i : Finset.Iic n) → ℝ) ℝ

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

noncomputable def trajectory (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] : Measure (ℕ → ℝ)

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

theorem stepKernel_apply_prefix (ν ρ : ℝ) (law : Kernel Node ℝ) (Y : ℕ → ℝ) (n : ℕ) : stepKernel ν ρ law n (Preorder.frestrictLe n Y) = law (action ν ρ Y (n+1))

Conditional reward distribution is produced by the constructed trajectory, not supplied as a confidence or stochastic-process oracle.

theorem trajectory_condDistrib (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (n : ℕ) : condDistrib (fun Y : ℕ → ℝ => Y (n+1)) (Preorder.frestrictLe n) (trajectory ν ρ law) =ᵐ[(trajectory ν ρ law).map (Preorder.frestrictLe n)] stepKernel ν ρ law n

The joint prefix/next-reward law, useful without choosing a conditional expectation version. It keeps the actual history-dependent kernel.

theorem trajectory_prefix_compProd (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (n : ℕ) : (trajectory ν ρ law).map (Preorder.frestrictLe n) ⊗ₘ stepKernel ν ρ law n = (trajectory ν ρ law).map (fun Y => (Preorder.frestrictLe n Y, Y (n+1)))

The chronological trajectory starts with exactly the first selected node's reward law. No artificial reward is inserted at index zero.

theorem trajectory_initial_law (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] : (trajectory ν ρ law).map (fun Y => Y 0) = law (action ν ρ (fun _ => 0) 0)