BanditRLProof.LowerBounds.GaussianHypothesisTesting

Variance `1 / n` of the mean of `n` unit-variance observations.

def gaussianSampleMeanVariance (sampleSize : Nat) : NNReal

The source's sample-mean variance is nondegenerate for a positive sample size.

theorem gaussianSampleMeanVariance_pos (sampleSize : Nat) (hsampleSize : 0 < sampleSize) : 0 < gaussianSampleMeanVariance sampleSize

The Gaussian law stated in Chapter 13.1 for the sample mean observation.

noncomputable def gaussianSampleMeanLaw (sampleSize : Nat) (mean : Real) : Measure Real

Canonical joint law of `n` independent `N(mean, 1)` observations.

noncomputable def gaussianIIDObservationLaw (sampleSize : Nat) (mean : Real) : Measure (Fin sampleSize → Real)

Arithmetic mean of a finite coordinate family.

def gaussianCoordinateAverage (sampleSize : Nat) (observations : Fin sampleSize → Real) : Real

The sum of the canonical iid observations has mean `n * mean` and variance `n`.

theorem gaussianIIDSumLaw (sampleSize : Nat) (mean : Real) : (gaussianIIDObservationLaw sampleSize mean).map (fun observations => ∑ i, observations i) = gaussianReal ((sampleSize : Real) * mean) (sampleSize : NNReal)

The arithmetic mean under the canonical product law of `n > 0` independent `N(mean, 1)` observations has exactly the source law `N(mean, 1 / n)`.

theorem gaussianIIDSampleMeanLaw (sampleSize : Nat) (mean : Real) (hsampleSize : 0 < sampleSize) : (gaussianIIDObservationLaw sampleSize mean).map (gaussianCoordinateAverage sampleSize) = gaussianSampleMeanLaw sampleSize mean

Threshold rule for the two hypotheses `mean = 0` and `mean = gap`. Ties are assigned to `gap`, matching the source's zero-mean error event `sampleMean >= gap / 2`; for a nondegenerate Gaussian law, the tie has mass zero.

def twoPointGaussianThresholdDecision (gap observation : Real) : Real

Under the zero-mean hypothesis, the threshold rule errs exactly above the midpoint.

theorem twoPointGaussianThresholdDecision_zero_error_event {gap : Real} (hgap : 0 < gap) : {observation | twoPointGaussianThresholdDecision gap observation ≠ 0} = Set.Ici (gap / 2)

Under the positive-mean hypothesis, errors occur exactly below the midpoint.

theorem twoPointGaussianThresholdDecision_gap_error_event {gap : Real} (hgap : 0 < gap) : {observation | twoPointGaussianThresholdDecision gap observation ≠ gap} = Set.Iio (gap / 2)

Error probability of the threshold decision under the zero-mean sample-mean law.

noncomputable def gaussianSampleMeanZeroErrorProbability (sampleSize : Nat) (gap : Real) : Real

Error probability of the threshold decision under the positive-mean sample-mean law.

noncomputable def gaussianSampleMeanGapErrorProbability (sampleSize : Nat) (gap : Real) : Real

A centered real Gaussian has its variance as a sub-Gaussian proxy.

theorem hasSubgaussianMGF_id_gaussianReal_zero (variance : NNReal) : HasSubgaussianMGF id variance (gaussianReal 0 variance)

Reflection around the mean turns `N(gap, variance)` into a centered sub-Gaussian.

theorem hasSubgaussianMGF_gap_sub_id_gaussianReal (gap : Real) (variance : NNReal) : HasSubgaussianMGF (fun observation => gap - observation) variance (gaussianReal gap variance)

Chernoff upper bound for a centered Gaussian right tail.

theorem gaussianReal_zero_Ici_le_exp_neg_sq_div_two_variance (variance : NNReal) (threshold : Real) (hthreshold : 0 ≤ threshold) : (gaussianReal 0 variance).real (Set.Ici threshold) ≤ Real.exp (-threshold ^ 2 / (2 * (variance : Real)))

The positive-mean midpoint error has the same Chernoff exponent by reflection.

theorem gaussianReal_gap_Iio_half_le_exp_neg_sq_div_two_variance (gap : Real) (variance : NNReal) (hgap : 0 < gap) : (gaussianReal gap variance).real (Set.Iio (gap / 2)) ≤ Real.exp (-(gap / 2) ^ 2 / (2 * (variance : Real)))

For the Chapter 13.1 zero-mean branch, the midpoint threshold has error at most `exp (-n * gap^2 / 8)` under the stated `N(0, 1/n)` sample-mean law.

theorem gaussianSampleMeanZeroErrorProbability_le_exp (sampleSize : Nat) (gap : Real) (hgap : 0 < gap) : gaussianSampleMeanZeroErrorProbability sampleSize gap ≤ Real.exp (-(sampleSize : Real) * gap ^ 2 / 8)

For the positive-mean branch, the same midpoint rule has the identical `exp (-n * gap^2 / 8)` Chernoff upper bound.

theorem gaussianSampleMeanGapErrorProbability_le_exp (sampleSize : Nat) (gap : Real) (hgap : 0 < gap) : gaussianSampleMeanGapErrorProbability sampleSize gap ≤ Real.exp (-(sampleSize : Real) * gap ^ 2 / 8)

Worst of the two midpoint-decision error probabilities.

noncomputable def gaussianSampleMeanThresholdRisk (sampleSize : Nat) (gap : Real) : Real

Both Gaussian hypotheses obey the same source-shaped Chernoff exponent.

theorem gaussianSampleMeanThresholdRisk_le_exp (sampleSize : Nat) (gap : Real) (hgap : 0 < gap) : gaussianSampleMeanThresholdRisk sampleSize gap ≤ Real.exp (-(sampleSize : Real) * gap ^ 2 / 8)

Exact Mills bounds for the source error probability, in standardized coordinates.

theorem gaussianSampleMeanZeroErrorProbability_mills_bounds (sampleSize : Nat) (hsampleSize : 0 < sampleSize) (gap : Real) (hgap : 0 < gap) : let z := (gap / 2) / Real.sqrt (2 * (gaussianSampleMeanVariance sampleSize : Real)) Real.exp (-z ^ 2) / (z + Real.sqrt (z ^ 2 + 2)) / Real.sqrt Real.pi ≤ gaussianSampleMeanZeroErrorProbability sampleSize gap ∧ gaussianSampleMeanZeroErrorProbability sampleSize gap ≤ Real.exp (-z ^ 2) / (z + Real.sqrt (z ^ 2 + 4 / Real.pi)) / Real.sqrt Real.pi

The exact printed two-sided Gaussian testing inequality, Eq. (13.1).

theorem gaussianSampleMeanZeroErrorProbability_source_bounds (sampleSize : Nat) (hsampleSize : 0 < sampleSize) (gap : Real) (hgap : 0 < gap) : let q := (sampleSize : Real) * gap ^ 2 Real.sqrt (8 / Real.pi) * Real.exp (-q / 8) / (Real.sqrt q + Real.sqrt (q + 16)) ≤ gaussianSampleMeanZeroErrorProbability sampleSize gap ∧ gaussianSampleMeanZeroErrorProbability sampleSize gap ≤ Real.sqrt (8 / Real.pi) * Real.exp (-q / 8) / (Real.sqrt q + Real.sqrt (q + 32 / Real.pi))