BanditRLProof.Algorithms.HOOConcentration

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

noncomputable def regionNoise (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (i : ℕ) (Y : ℕ → ℝ) : ℝ

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

noncomputable def regionCount (ν ρ : ℝ) (v : Node) (i : ℕ) (Y : ℕ → ℝ) : ℝ

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

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

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

theorem measurable_action_piLE (ν ρ : ℝ) (n : ℕ) : Measurable[Filtration.piLE n] (fun Y : ℕ → ℝ => action ν ρ Y n)

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

theorem measurable_coordinate_piLE (n : ℕ) : Measurable[Filtration.piLE n] (fun Y : ℕ → ℝ => Y n)

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

theorem region_compensated_adapted (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (tilt : ℝ) : StronglyAdapted Filtration.piLE (fun i Y => tilt * regionNoise ν ρ law v i Y - tilt^2/8 * regionCount ν ρ v i Y)

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

theorem region_compensated_successor (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (tilt : ℝ) : Concentration.HasCondMGFUpperBoundAt (Filtration.piLE n) (Filtration.piLE.le n) (fun Y => tilt * regionNoise ν ρ law v (n+1) Y - tilt^2/8 * regionCount ν ρ v (n+1) Y) 1 0 (trajectory ν ρ law)

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

theorem region_compensated_initial (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (tilt : ℝ) : Concentration.HasMGFUpperBoundAt (fun Y => tilt * regionNoise ν ρ law v 0 Y - tilt^2/8 * regionCount ν ρ v 0 Y) 1 0 (trajectory ν ρ law)

A regional noise/count tail for the real HOO process. Both the initial and conditional MGF obligations are derived from its bounded reward kernels.

theorem region_noise_count_tail (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (tilt threshold countBudget : ℝ) (htilt : 0 ≤ tilt) : (trajectory ν ρ law) {Y | threshold ≤ ∑ i ∈ Finset.range n, regionNoise ν ρ law v i Y ∧ (∑ i ∈ Finset.range n, regionCount ν ρ v i Y) ≤ countBudget} ≤ ENNReal.ofReal (Real.exp (-tilt * threshold + tilt^2/8 * countBudget))

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

theorem sum_regionCount_eq_visits (ν ρ : ℝ) (v : Node) (n : ℕ) (Y : ℕ → ℝ) : (∑ i ∈ Finset.range n, regionCount ν ρ v i Y) = (visits (history ν ρ Y n) v : ℝ)

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

theorem sum_regionNoise_eq_rewardSum_sub_means (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (n : ℕ) (Y : ℕ → ℝ) : (∑ i ∈ Finset.range n, regionNoise ν ρ law v i Y) = rewardSum (history ν ρ Y n) v - ∑ i ∈ Finset.range n, regionCount ν ρ v i Y * nodeMean law (action ν ρ Y i)

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

theorem region_negative_noise_count_tail (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (tilt threshold countBudget : ℝ) (htilt : 0 ≤ tilt) : (trajectory ν ρ law) {Y | threshold ≤ -(∑ i ∈ Finset.range n, regionNoise ν ρ law v i Y) ∧ (visits (history ν ρ Y n) v : ℝ) ≤ countBudget} ≤ ENNReal.ofReal (Real.exp (-tilt * threshold + tilt^2/8 * countBudget))

Optimized upper tail, retaining the actual regional visit count in the event.

theorem region_noise_visits_tail (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (threshold countBudget : ℝ) (hthreshold : 0 ≤ threshold) (hcount : 0 < countBudget) : (trajectory ν ρ law) {Y | threshold ≤ ∑ i ∈ Finset.range n, regionNoise ν ρ law v i Y ∧ (visits (history ν ρ Y n) v : ℝ) ≤ countBudget} ≤ ENNReal.ofReal (Real.exp (-2 * threshold^2 / countBudget))

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

theorem region_negative_noise_visits_tail (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (threshold countBudget : ℝ) (hthreshold : 0 ≤ threshold) (hcount : 0 < countBudget) : (trajectory ν ρ law) {Y | threshold ≤ -(∑ i ∈ Finset.range n, regionNoise ν ρ law v i Y) ∧ (visits (history ν ρ Y n) v : ℝ) ≤ countBudget} ≤ ENNReal.ofReal (Real.exp (-2 * threshold^2 / countBudget))