Lean module · Foundations
BanditRLProof.LowerBounds.GaussianTesting
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.Minimax
Imported by
BanditRLProof, BanditRLProof.LowerBounds.RelativeEntropyNonMetric
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.LowerBounds.log_gaussianPDFReal_div_same_variance
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.log_gaussianPDFReal_div_same_varianceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem log_gaussianPDFReal_div_same_variance (m n x : ℝ) (v : ℝ≥0) (hv : v ≠ 0) : Real.log (gaussianPDFReal m v x / gaussianPDFReal n v x) = ((m - n) * x + (n ^ 2 - m ^ 2) / 2) / v
theorem
BanditRLProof.LowerBounds.llr_gaussianReal_same_variance_ae
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.llr_gaussianReal_same_variance_aeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem llr_gaussianReal_same_variance_ae (m n : ℝ) (v : ℝ≥0) (hv : v ≠ 0) : llr (gaussianReal m v) (gaussianReal n v) =ᵐ[gaussianReal m v] fun x => ((m - n) * x + (n ^ 2 - m ^ 2) / 2) / v
theorem
BanditRLProof.LowerBounds.integrable_llr_gaussianReal_same_variance
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.integrable_llr_gaussianReal_same_varianceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_llr_gaussianReal_same_variance (m n : ℝ) (v : ℝ≥0) (hv : v ≠ 0) : Integrable (llr (gaussianReal m v) (gaussianReal n v)) (gaussianReal m v)
theorem
BanditRLProof.LowerBounds.klDiv_gaussianReal_same_variance
Compiled
The common positive variance Gaussian KL formula in Chapter 14.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret · Chapter 14: Foundations of Information Theory
Canonical node identity
declaration:BanditRLProof.LowerBounds.klDiv_gaussianReal_same_varianceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem klDiv_gaussianReal_same_variance (m n : ℝ) (v : ℝ≥0) (hv : v ≠ 0) : InformationTheory.klDiv (gaussianReal m v) (gaussianReal n v) = ENNReal.ofReal ((m - n) ^ 2 / (2 * v))
theorem
BanditRLProof.LowerBounds.three_fifths_le_exp_neg_half
Compiled
Exact rational certification of the displayed Gaussian testing constant.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.three_fifths_le_exp_neg_halfReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem three_fifths_le_exp_neg_half : (3 / 5 : ℝ) ≤ Real.exp (-(1 / 2 : ℝ))
theorem
BanditRLProof.LowerBounds.gaussian_testing_error_lower_bound
Compiled
Testing two Gaussian means from one observation, with arbitrary positive variance.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.gaussian_testing_error_lower_boundReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gaussian_testing_error_lower_bound (Δ : ℝ) (v : ℝ≥0) (hv : v ≠ 0) {A : Set ℝ} (hA : MeasurableSet A) : (1 / 2 : ℝ) * Real.exp (-(Δ ^ 2 / (2 * v))) ≤ (gaussianReal 0 v).real A + (gaussianReal Δ v).real Aᶜ
theorem
BanditRLProof.LowerBounds.gaussian_testing_error_three_tenths
Compiled
Under signal-to-noise ratio at most one, the sum of errors is at least 3/10.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.gaussian_testing_error_three_tenthsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gaussian_testing_error_three_tenths (Δ : ℝ) (v : ℝ≥0) (hv : v ≠ 0) (hsnr : Δ ^ 2 / (v : ℝ) ≤ 1) {A : Set ℝ} (hA : MeasurableSet A) : (3 / 10 : ℝ) ≤ (gaussianReal 0 v).real A + (gaussianReal Δ v).real Aᶜ
theorem
BanditRLProof.LowerBounds.gaussian_testing_max_error_three_twentieths
Compiled
No measurable decision rule has both errors below 3/20 in the low-SNR regime.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret · Chapter 14: Foundations of Information Theory
Canonical node identity
declaration:BanditRLProof.LowerBounds.gaussian_testing_max_error_three_twentiethsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gaussian_testing_max_error_three_twentieths (Δ : ℝ) (v : ℝ≥0) (hv : v ≠ 0) (hsnr : Δ ^ 2 / (v : ℝ) ≤ 1) {A : Set ℝ} (hA : MeasurableSet A) : (3 / 20 : ℝ) ≤ max ((gaussianReal 0 v).real A) ((gaussianReal Δ v).real Aᶜ)