BanditRLProof.HeavyTailTuning

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

theorem power_threshold_bias_term (u c a ε x : ℝ) (hc : 0 < c) (hx : 0 < x) (haε : a * ε = 1-a) : u / (c * x^a)^ε = (u / c^ε) * x^(a-1)

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

theorem power_threshold_bias_sum (u c a ε : ℝ) (hu : 0 ≤ u) (hc : 0 < c) (ha : 0 < a) (ha1 : a ≤ 1) (haε : a * ε = 1-a) (n : ℕ) : (∑ s ∈ Finset.range n, u / (c * ((s : ℝ)+1)^a)^ε) ≤ (u / c^ε) * ((n : ℝ)^a / a)

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

theorem sampleThreshold_factor (ε u : ℝ) (hu : 0 ≤ u) (t s : ℕ) : sampleThreshold ε u t s = (u / confidenceLog t)^(1/(1+ε)) * ((s : ℝ)+1)^(1/(1+ε))

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

theorem sampleThreshold_bias_sum (ε u : ℝ) (hε : 0 ≤ ε) (hu : 0 < u) (t n : ℕ) : (∑ s ∈ Finset.range n, u / (sampleThreshold ε u t s)^ε) ≤ (u / ((u / confidenceLog t)^(1/(1+ε)))^ε) * ((n : ℝ)^(1/(1+ε)) / (1/(1+ε)))

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

theorem power_scale_bias (u L a ε : ℝ) (hu : 0 < u) (hL : 0 < L) (haε : a * ε = 1-a) : u / ((u/L)^a)^ε = u^a * L^(1-a)

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

theorem power_bias_normalization (u L a N : ℝ) (hL : 0 < L) (hN : 0 < N) : (u^a * L^(1-a)) * (N^a / a) / N = (1/a) * u^a * (L/N)^(1-a)

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

theorem sampleThreshold_bias_average (ε u : ℝ) (hε : 0 ≤ ε) (hu : 0 < u) (t n : ℕ) (hn : 0 < n) : (∑ s ∈ Finset.range n, u / (sampleThreshold ε u t s)^ε) / n ≤ (1+ε) * u^(1/(1+ε)) * (confidenceLog t / n)^(ε/(1+ε))

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

theorem threshold_scale_identity (u L N a : ℝ) (hu : 0 ≤ u) (hL : 0 < L) (hN : 0 < N) : (u*N/L)^a * L = N * (u^a * (L/N)^(1-a))

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

theorem threshold_variance_identity (u L N ε : ℝ) (hu : 0 < u) (hL : 0 < L) (hN : 0 < N) (hp : 0 < 1+ε) : N*u*((u*N/L)^(1/(1+ε)))^(1-ε)*L = ((u*N/L)^(1/(1+ε))*L)^2

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

theorem confidenceLog_pos (t : ℕ) : 0 < confidenceLog t

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

theorem sampleThreshold_pos (ε u : ℝ) (hu : 0 < u) (t s : ℕ) : 0 < sampleThreshold ε u t s

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

theorem sampleThreshold_le_terminal (ε u : ℝ) (hε : 0 ≤ ε) (hu : 0 ≤ u) (t n s : ℕ) (hs : s < n) : sampleThreshold ε u t s ≤ (u*n/confidenceLog t)^(1/(1+ε))

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

theorem sampleThreshold_variance_sum (ε u : ℝ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (t n : ℕ) : (∑ s ∈ Finset.range n, u * (sampleThreshold ε u t s)^(1-ε)) ≤ n*u*((u*n/confidenceLog t)^(1/(1+ε)))^(1-ε)

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

theorem tuned_radius_le (ε u : ℝ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (t n : ℕ) (hn : 0 < n) : ((∑ s ∈ Finset.range n, u / (sampleThreshold ε u t s)^ε) + (2 * Real.sqrt ((∑ s ∈ Finset.range n, u * (sampleThreshold ε u t s)^(1-ε)) * confidenceLog t) + 2 * (u*n/confidenceLog t)^(1/(1+ε)) * confidenceLog t)) / n ≤ confidenceRadius ε u t n