BanditRLProof.Algorithms.HOORegretPartition

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

theorem action_singleton_count_le_one (ν ρ : ℝ) (Y : ℕ → ℝ) (N : ℕ) (p : Node) : (∑ n ∈ Finset.range N, if action ν ρ Y n=p then (1:ℝ) else 0) ≤ 1

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

theorem RegularCovering.deep_regret_le {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hw : WeaklyLipschitz f C.ell best) (H N : ℕ) (Y : ℕ → ℝ) : (∑ n ∈ Finset.range N, if action C.nu1 C.rho Y n ∈ C.deepGoodNodes f best H then best-f (C.toCovering.arm C.nu1 C.rho Y n) else 0) ≤ 4*(C.nu1*C.rho^H)*N

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

theorem RegularCovering.shallow_regret_le {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hw : WeaklyLipschitz f C.ell best) (H N : ℕ) (Y : ℕ → ℝ) : (∑ n ∈ Finset.range N, if action C.nu1 C.rho Y n ∈ C.shallowGoodNodes f best H then best-f (C.toCovering.arm C.nu1 C.rho Y n) else 0) ≤ ∑ h ∈ Finset.range H, 4*(C.nu1*C.rho^h)*(C.nearOptimalNodes f best h).card

Poor-subtree contribution on each actual reward path. Its prefix indicators are exactly the history's visits, including unvisited nodes.

theorem RegularCovering.bad_regret_le {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hw : WeaklyLipschitz f C.ell best) (H N : ℕ) (Y : ℕ → ℝ) : (∑ n ∈ Finset.range N, if action C.nu1 C.rho Y n ∈ C.badSubtreeNodes f best H then best-f (C.toCovering.arm C.nu1 C.rho Y n) else 0) ≤ ∑ h ∈ Finset.range H, ∑ p ∈ C.boundaryNodes f best h, 4*(C.nu1*C.rho^h)*(visits (history C.nu1 C.rho Y N) p : ℝ)

The actual pathwise three-term regret bound before expectation or depth optimization. No partition, visit count or one-play property is assumed.

theorem RegularCovering.pathwise_regret_le {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hf : ∀x, f x≤best) (hbest : regionSup f Set.univ=best) (hw : WeaklyLipschitz f C.ell best) (H N : ℕ) (Y : ℕ → ℝ) : (∑ n ∈ Finset.range N, (best-f (C.toCovering.arm C.nu1 C.rho Y n))) ≤ 4*(C.nu1*C.rho^H)*N + (∑ h ∈ Finset.range H, 4*(C.nu1*C.rho^h)*(C.nearOptimalNodes f best h).card) + ∑ h ∈ Finset.range H, ∑ p ∈ C.boundaryNodes f best h, 4*(C.nu1*C.rho^h)*(visits (history C.nu1 C.rho Y N) p : ℝ)

Source first-step simplification for the actual boundary nodes.

theorem RegularCovering.boundary_expected_visits {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : Kernel X ℝ) [IsMarkovKernel law] (f : X → ℝ) (best : ℝ) (hmean : ∀ x, (∫ y, y ∂law x)=f x) (hf : ∀ x, f x≤best) (hbest : regionSup f Set.univ=best) (hw : WeaklyLipschitz f C.ell best) (hbound : ∀ x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0:ℝ) 1) {h : ℕ} {v : Node} (hv : v ∈ C.boundaryNodes f best h) (N : ℕ) : (∫ Y, (visits (history C.nu1 C.rho Y N) v : ℝ) ∂trajectory C.nu1 C.rho (C.toCovering.nodeLaw law)) ≤ 8*Real.log (max (N:ℝ) 2)/(C.nu1*C.rho^(h+1))^2+4