BanditRLProof.Algorithms.HOOActualRegret

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

theorem trajectory_reward_bounded (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀v, ∀ᵐ y ∂law v, y ∈ Set.Icc (0:ℝ) 1) (n : ℕ) : ∀ᵐ Y ∂trajectory ν ρ law, Y n ∈ Set.Icc (0:ℝ) 1

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

theorem integrable_trajectory_reward (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀v, ∀ᵐ y ∂law v, y ∈ Set.Icc (0:ℝ) 1) (n : ℕ) : Integrable (fun Y => Y n) (trajectory ν ρ law)

The reward mean at each actual round equals the mean of its causally selected node. Both the initial round and the successor joint law are used.

theorem integral_trajectory_reward (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀v, ∀ᵐ y ∂law v, y ∈ Set.Icc (0:ℝ) 1) (n : ℕ) : (∫ Y, Y n ∂trajectory ν ρ law) = ∫ Y, nodeMean law (action ν ρ Y n) ∂trajectory ν ρ law

Source model version of the one-round expectation identity.

theorem Covering.integral_actual_reward {X : Type*} [MeasurableSpace X] (C : Covering X) (law : Kernel X ℝ) [IsMarkovKernel law] (ν ρ : ℝ) (f : X → ℝ) (hmean : ∀x, (∫ y, y ∂law x)=f x) (hbound : ∀x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0:ℝ) 1) (n : ℕ) : (∫ Y, Y n ∂trajectory ν ρ (C.nodeLaw law)) = ∫ Y, f (C.arm ν ρ Y n) ∂trajectory ν ρ (C.nodeLaw law)

Expected cumulative realized regret and pseudo-regret coincide at every horizon for one fixed policy and compatible infinite reward trajectory.

theorem RegularCovering.expected_actual_eq_pseudoRegret {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : Kernel X ℝ) [IsMarkovKernel law] (f : X → ℝ) (best : ℝ) (hmean : ∀x, (∫ y, y ∂law x)=f x) (hfrange : ∀x, f x ∈ Set.Icc (0:ℝ) 1) (hbound : ∀x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0:ℝ) 1) (N : ℕ) : (∫ Y, (∑ n ∈ Finset.range N, (best-Y n)) ∂trajectory C.nu1 C.rho (C.toCovering.nodeLaw law)) = (∫ Y, (∑ n ∈ Finset.range N, (best-f (C.toCovering.arm C.nu1 C.rho Y n))) ∂trajectory C.nu1 C.rho (C.toCovering.nodeLaw law))

The same repaired source rate for expected realized cumulative regret.

theorem RegularCovering.expected_actualRegret_rate {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : Kernel X ℝ) [IsMarkovKernel law] (f : X → ℝ) (best d : ℝ) (hmean : ∀x, (∫ y, y ∂law x)=f x) (hf : ∀x, f x≤best) (hfrange : ∀x, f x ∈ Set.Icc (0:ℝ) 1) (hbest : regionSup f Set.univ=best) (hw : WeaklyLipschitz f C.ell best) (hbound : ∀x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0:ℝ) 1) (hd : C.nearOptimalityDimension f best (4*C.nu1/C.nu2) < (d:EReal)) : ∃ γ : ℝ, 0<γ ∧ ∀ N : ℕ, 1≤N → (∫ Y, (∑ n ∈ Finset.range N, (best-Y n)) ∂trajectory C.nu1 C.rho (C.toCovering.nodeLaw law)) ≤ γ*(N:ℝ)^((d+1)/(d+2))*(Real.log (max (N:ℝ) 2))^(1/(d+2))