BanditRLProof.LowerBounds.GaussianMillsRatio

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

noncomputable def gaussianMillsComparison (c x : ℝ) : ℝ

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

theorem gaussianMillsComparison_denominator_pos {c x : ℝ} (hc : 0 < c) : 0 < x + Real.sqrt (x ^ 2 + c)

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

theorem hasDerivAt_gaussianMillsComparison {c x : ℝ} (hc : 0 < c) : HasDerivAt (gaussianMillsComparison c) (-gaussianMillsComparison c x * (2 * x + 1 / Real.sqrt (x ^ 2 + c))) x

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

theorem gaussianMillsComparison_lower_derivative_bound (x : ℝ) : gaussianMillsComparison 2 x * (2 * x + 1 / Real.sqrt (x ^ 2 + 2)) ≤ Real.exp (-x ^ 2)

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

theorem gaussianMillsComparison_pos {c : ℝ} (hc : 0 < c) (x : ℝ) : 0 < gaussianMillsComparison c x

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

theorem tendsto_gaussianMillsComparison {c : ℝ} (hc : 0 < c) : Tendsto (gaussianMillsComparison c) atTop (𝓝 0)

The exact lower half of Lattimore--Szepesvari Eq. (13.4).

theorem gaussianMills_lower_integral {x : ℝ} (hx : 0 ≤ x) : Real.exp (-x ^ 2) / (x + Real.sqrt (x ^ 2 + 2)) ≤ ∫ t in Ioi x, Real.exp (-t ^ 2)

Algebraic sign test for the derivative of the upper comparison error.

theorem gaussianMills_sign_iff {c x : ℝ} (hc : 1 < c) (hx : 0 ≤ x) : 0 ≤ x ^ 2 + c - 1 - x * Real.sqrt (x ^ 2 + c) ↔ x ^ 2 * (2 - c) ≤ (c - 1) ^ 2

The sign changes at exactly one nonnegative threshold when `1<c<2`.

theorem gaussianMills_sign_threshold {c x : ℝ} (hc : 1 < c) (hc2 : c < 2) (hx : 0 ≤ x) : 0 ≤ x ^ 2 + c - 1 - x * Real.sqrt (x ^ 2 + c) ↔ x ≤ (c - 1) / Real.sqrt (2 - c)

The derivative of comparison minus Gaussian tail has this explicit value.

noncomputable def gaussianMillsErrorDerivative (c x : ℝ) : ℝ

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

theorem gaussianMillsErrorDerivative_factor {c x : ℝ} (hc : 0 < c) : gaussianMillsErrorDerivative c x = Real.exp (-x ^ 2) * (x ^ 2 + c - 1 - x * Real.sqrt (x ^ 2 + c)) / ((x + Real.sqrt (x ^ 2 + c)) * Real.sqrt (x ^ 2 + c))

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

theorem gaussianMillsErrorDerivative_nonneg_iff {c x : ℝ} (hc : 1 < c) (hc2 : c < 2) (hx : 0 ≤ x) : 0 ≤ gaussianMillsErrorDerivative c x ↔ x ≤ (c - 1) / Real.sqrt (2 - c)

Specialization to the exact upper-bound constant in source Eq. (13.4).

theorem gaussianMillsErrorDerivative_source_nonneg_iff {x : ℝ} (hx : 0 ≤ x) : 0 ≤ gaussianMillsErrorDerivative (4 / Real.pi) x ↔ x ≤ (4 / Real.pi - 1) / Real.sqrt (2 - 4 / Real.pi)

Comparison error expressed using a finite-interval Gaussian integral.

noncomputable def gaussianMillsError (c x : ℝ) : ℝ

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

theorem hasDerivAt_gaussianMillsError {c x : ℝ} (hc : 0 < c) : HasDerivAt (gaussianMillsError c) (gaussianMillsErrorDerivative c x) x

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

theorem gaussianMillsError_source_zero : gaussianMillsError (4 / Real.pi) 0 = 0

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

theorem tendsto_gaussianMillsError {c : ℝ} (hc : 0 < c) : Tendsto (gaussianMillsError c) atTop (𝓝 0)

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

theorem gaussianMillsError_source_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ gaussianMillsError (4 / Real.pi) x

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

theorem gaussian_integral_split (x : ℝ) : (∫ t in (0 : ℝ)..x, Real.exp (-t ^ 2)) + (∫ t in Ioi x, Real.exp (-t ^ 2)) = Real.sqrt Real.pi / 2

The exact upper half of Lattimore--Szepesvari Eq. (13.4).

theorem gaussianMills_upper_integral {x : ℝ} (hx : 0 ≤ x) : (∫ t in Ioi x, Real.exp (-t ^ 2)) ≤ Real.exp (-x ^ 2) / (x + Real.sqrt (x ^ 2 + 4 / Real.pi))

Exact density-integral representation for a centered Gaussian tail.

theorem gaussianReal_zero_tail_integral (v : ℝ≥0) (hv : 0 < v) (a : ℝ) : (gaussianReal 0 v).real (Ici a) = (Real.sqrt (2 * Real.pi * (v : ℝ)))⁻¹ * ∫ t in Ioi a, Real.exp (-t ^ 2 / (2 * (v : ℝ)))

The variance-one-half normal law is exactly the normalized source integral.

theorem gaussianReal_half_tail_integral (a : ℝ) : (gaussianReal 0 (1 / 2 : ℝ≥0)).real (Ici a) = (∫ t in Ioi a, Real.exp (-t ^ 2)) / Real.sqrt Real.pi

Both exact Mills bounds for the normalized variance-one-half Gaussian.

theorem gaussianReal_half_mills_bounds {a : ℝ} (ha : 0 ≤ a) : Real.exp (-a ^ 2) / (a + Real.sqrt (a ^ 2 + 2)) / Real.sqrt Real.pi ≤ (gaussianReal 0 (1 / 2 : ℝ≥0)).real (Ici a) ∧ (gaussianReal 0 (1 / 2 : ℝ≥0)).real (Ici a) ≤ Real.exp (-a ^ 2) / (a + Real.sqrt (a ^ 2 + 4 / Real.pi)) / Real.sqrt Real.pi

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

theorem gaussianReal_zero_standardized_tail (v : ℝ≥0) (hv : 0 < v) (a : ℝ) : (gaussianReal 0 v).real (Ici a) = (∫ t in Ioi (a / Real.sqrt (2 * (v : ℝ))), Real.exp (-t ^ 2)) / Real.sqrt Real.pi

Exact standardized Mills bounds for every positive Gaussian variance.

theorem gaussianReal_zero_mills_bounds (v : ℝ≥0) (hv : 0 < v) (a : ℝ) (ha : 0 ≤ a) : let z := a / Real.sqrt (2 * (v : ℝ)) Real.exp (-z ^ 2) / (z + Real.sqrt (z ^ 2 + 2)) / Real.sqrt Real.pi ≤ (gaussianReal 0 v).real (Ici a) ∧ (gaussianReal 0 v).real (Ici a) ≤ Real.exp (-z ^ 2) / (z + Real.sqrt (z ^ 2 + 4 / Real.pi)) / Real.sqrt Real.pi

Rescale a Mills expression to the square-root denominators in Eq. (13.1).

theorem gaussianMills_expression_rescale {z c q : ℝ} (hz : 0 ≤ z) (hc : 0 < c) (hq : q = 8 * z ^ 2) : Real.exp (-z ^ 2) / (z + Real.sqrt (z ^ 2 + c)) / Real.sqrt Real.pi = Real.sqrt (8 / Real.pi) * Real.exp (-q / 8) / (Real.sqrt q + Real.sqrt (q + 8 * c))