BanditRLProof.Algorithms.HOOIndexConfidence

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

theorem regional_means_lower (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (m : ℝ) (hm : ∀ a, v <+: a → m ≤ nodeMean law a) (n : ℕ) (Y : ℕ → ℝ) : m * (visits (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 regional_means_upper (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (m : ℝ) (hm : ∀ a, v <+: a → nodeMean law a ≤ m) (n : ℕ) (Y : ℕ → ℝ) : (∑ i ∈ Finset.range n, regionCount ν ρ v i Y * nodeMean law (action ν ρ Y i)) ≤ m * (visits (history ν ρ Y n) v : ℝ)

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

theorem count_mul_width (T L : ℝ) (hT : 0 < T) : T * Real.sqrt (2*L/T) = Real.sqrt (2*T*L)

A low U value in a region whose descendant means exceed `best-D` forces a lower centered-noise deviation, on the exact generated history.

theorem upper_le_implies_lower_deviation (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (best : ℝ) (hm : ∀ a, v <+: a → best - ν*ρ^v.length ≤ nodeMean law a) (n : ℕ) (Y : ℕ → ℝ) (hu : upper ν ρ (history ν ρ Y n) v ≤ (best : WithTop ℝ)) : 0 < visits (history ν ρ Y n) v ∧ Real.sqrt (2*(visits (history ν ρ Y n) v : ℝ)*Real.log (max (n:ℝ) 2)) ≤ regionDeviation ν ρ law v n true Y

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

theorem upper_underestimate_probability (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (best : ℝ) (hm : ∀ a, v <+: a → best - ν*ρ^v.length ≤ nodeMean law a) (n : ℕ) : (trajectory ν ρ law) {Y | upper ν ρ (history ν ρ Y n) v ≤ (best : WithTop ℝ)} ≤ (n : ENNReal) * ENNReal.ofReal (Real.exp (-4*Real.log (max (n:ℝ) 2)))

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

theorem width_le_half_gap (T L gap : ℝ) (hT : 0 < T) (hgap : 0 < gap) (hcount : 8*L/gap^2 ≤ T) : Real.sqrt (2*L/T) ≤ gap/2

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

theorem upper_ge_implies_upper_deviation (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (best gap : ℝ) (hgap : 0 < gap - ν*ρ^v.length) (hm : ∀ a, v <+: a → nodeMean law a ≤ best-gap) (n : ℕ) (Y : ℕ → ℝ) (hcount : 8*Real.log (max (n:ℝ) 2)/(gap-ν*ρ^v.length)^2 ≤ (visits (history ν ρ Y n) v : ℝ)) (hu : (best : WithTop ℝ) ≤ upper ν ρ (history ν ρ Y n) v) : 0 < visits (history ν ρ Y n) v ∧ Real.sqrt (2*(visits (history ν ρ Y n) v : ℝ)*Real.log (max (n:ℝ) 2)) ≤ regionDeviation ν ρ law v n false Y

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

theorem upper_overestimate_probability (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (best gap : ℝ) (hgap : 0 < gap - ν*ρ^v.length) (hm : ∀ a, v <+: a → nodeMean law a ≤ best-gap) (n : ℕ) : (trajectory ν ρ law) {Y | 8*Real.log (max (n:ℝ) 2)/(gap-ν*ρ^v.length)^2 ≤ (visits (history ν ρ Y n) v : ℝ) ∧ (best : WithTop ℝ) ≤ upper ν ρ (history ν ρ Y n) v} ≤ (n : ENNReal) * ENNReal.ofReal (Real.exp (-4*Real.log (max (n:ℝ) 2)))

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

theorem Covering.nodeMean_eq {X : Type*} [MeasurableSpace X] (C : Covering X) (law : Kernel X ℝ) (f : X → ℝ) (hmean : ∀ x, (∫ y, y ∂law x) = f x) (a : Node) : nodeMean (C.nodeLaw law) a = f (C.representative a)

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

theorem RegularCovering.optimal_descendant_mean_lower {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : Kernel X ℝ) (f : X → ℝ) (best : ℝ) (hmean : ∀ x, (∫ y, y ∂law x) = f x) (hw : WeaklyLipschitz f C.ell best) (v : Node) (hv : regionSup f (C.region v) = best) : ∀ a, v <+: a → best - C.nu1*C.rho^v.length ≤ nodeMean (C.toCovering.nodeLaw law) a

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

theorem Covering.descendant_mean_upper {X : Type*} [MeasurableSpace X] (C : Covering X) (law : Kernel X ℝ) (f : X → ℝ) (best : ℝ) (hmean : ∀ x, (∫ y, y ∂law x) = f x) (hf : ∀ x, f x ≤ best) (v : Node) : ∀ a, v <+: a → nodeMean (C.nodeLaw law) a ≤ regionSup f (C.region v)

Source optimal-region underestimation bound, now produced from A1/A2, the reward-mean identity and bounded reward support. No confidence premise.

theorem RegularCovering.optimal_upper_underestimate_probability {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : Kernel X ℝ) [IsMarkovKernel law] (f : X → ℝ) (best : ℝ) (hmean : ∀ x, (∫ y, y ∂law x) = f x) (hw : WeaklyLipschitz f C.ell best) (hbound : ∀ x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (hv : regionSup f (C.region v) = best) (n : ℕ) : (trajectory C.nu1 C.rho (C.toCovering.nodeLaw law)) {Y | upper C.nu1 C.rho (history C.nu1 C.rho Y n) v ≤ (best : WithTop ℝ)} ≤ (n : ENNReal) * ENNReal.ofReal (Real.exp (-4*Real.log (max (n:ℝ) 2)))

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

theorem RegularCovering.poor_upper_overestimate_probability {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) (hbound : ∀ x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (hv : C.nu1*C.rho^v.length < best-regionSup f (C.region v)) (n : ℕ) : (trajectory C.nu1 C.rho (C.toCovering.nodeLaw law)) {Y | 8*Real.log (max (n:ℝ) 2)/(best-regionSup f (C.region v)-C.nu1*C.rho^v.length)^2 ≤ (visits (history C.nu1 C.rho Y n) v : ℝ) ∧ (best : WithTop ℝ) ≤ upper C.nu1 C.rho (history C.nu1 C.rho Y n) v} ≤ (n : ENNReal) * ENNReal.ofReal (Real.exp (-4*Real.log (max (n:ℝ) 2)))