BanditRLProof.Algorithms.HOOConditionalMGF

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

noncomputable def nodeMean (law : Kernel Node ℝ) (v : Node) : ℝ

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

theorem bounded_node_subgaussian (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ v, ∀ᵐ y ∂law v, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) : HasSubgaussianMGF (fun y => y - nodeMean law v) (1/4 : ℝ≥0) (law v)

The new setting supplies the existing fixed-MGF interface from bounded reward laws, rather than assuming a conditional confidence theorem.

theorem bounded_node_fixedMGF (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ v, ∀ᵐ y ∂law v, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (tilt : ℝ) : Concentration.HasMGFUpperBoundAt (fun y => y - nodeMean law v) tilt (tilt^2/8) (law v)

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

noncomputable def selectedNode (ν ρ : ℝ) (n : ℕ) (h : (i : Finset.Iic n) → ℝ) : Node

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

noncomputable def regionIncrement (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (n : ℕ) (h : (i : Finset.Iic n) → ℝ) (y : ℝ) : ℝ

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

noncomputable def regionSelected (ν ρ : ℝ) (v : Node) (n : ℕ) (h : (i : Finset.Iic n) → ℝ) : ℝ

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

theorem region_step_fixedMGF (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (h : (i : Finset.Iic n) → ℝ) (tilt : ℝ) : Concentration.HasMGFUpperBoundAt (regionIncrement ν ρ law v n h) tilt (tilt^2/8 * regionSelected ν ρ v n h) (stepKernel ν ρ law n h)

Predictable variance is paid only when this region is selected. This is the one-step exponential process needed for count-dependent concentration.

theorem region_step_compensated_integral_le_one (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (h : (i : Finset.Iic n) → ℝ) (tilt : ℝ) : (∫ y, Real.exp (tilt * regionIncrement ν ρ law v n h y - tilt^2/8 * regionSelected ν ρ v n h) ∂stepKernel ν ρ law n h) ≤ 1

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

theorem measurable_selectedNode (ν ρ : ℝ) (n : ℕ) : Measurable (selectedNode ν ρ n)

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

theorem measurable_regionSelected (ν ρ : ℝ) (v : Node) (n : ℕ) : Measurable (regionSelected ν ρ v n)

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

theorem measurable_regionIncrement (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (n : ℕ) : Measurable (fun p : ((i : Finset.Iic n) → ℝ) × ℝ => regionIncrement ν ρ law v n p.1 p.2)

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

noncomputable def regionCompensated (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (n : ℕ) (tilt : ℝ) (p : ((i : Finset.Iic n) → ℝ) × ℝ) : ℝ

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

theorem measurable_regionCompensated (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (n : ℕ) (tilt : ℝ) : Measurable (regionCompensated ν ρ law v n tilt)

All exponential moments are integrable under the joint prefix/reward law. This supplies the global integrability required by conditional MGF iteration.

theorem integrable_regionCompensated_exp (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (tilt s : ℝ) (μ : Measure ((i : Finset.Iic n) → ℝ)) [IsProbabilityMeasure μ] : Integrable (fun p => Real.exp (s * regionCompensated ν ρ law v n tilt p)) (μ ⊗ₘ stepKernel ν ρ law n)

The conditional exponential inequality holds for the actual constructed trajectory and its observed prefix, without a supplied concentration premise.

theorem trajectory_region_condExp_le_one (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (tilt : ℝ) : (trajectory ν ρ law)[fun Y => Real.exp (regionCompensated ν ρ law v n tilt (Preorder.frestrictLe n Y, Y (n+1))) | MeasurableSpace.comap (Preorder.frestrictLe n) inferInstance] ≤ᵐ[trajectory ν ρ law] fun _ => 1

Actual HOO successor increments now inhabit the shared conditional MGF interface. The only probabilistic premise is bounded support of each reward law.

theorem trajectory_region_condMGF (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (tilt : ℝ) : Concentration.HasCondMGFUpperBoundAt (MeasurableSpace.comap (Preorder.frestrictLe n) inferInstance) (Preorder.measurable_frestrictLe n).comap_le (fun Y => regionCompensated ν ρ law v n tilt (Preorder.frestrictLe n Y, Y (n+1))) 1 0 (trajectory ν ρ law)