BanditRLProof.LowerBounds.GaussianMinimax

A realized pull count, converted to `Real` for the source's regret algebra.

noncomputable def finiteHistoryPullCountReal {K : Nat} {Reward : Type*} (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) (arm : Fin K) : Real

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

theorem finiteHistoryPullCountENNReal_ne_top {K : Nat} {Reward : Type*} (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) (arm : Fin K) : finiteHistoryPullCountENNReal n history arm ≠ ∞

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

theorem sum_finiteHistoryPullCountENNReal {K : Nat} {Reward : Type*} (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) : ∑ arm : Fin K, finiteHistoryPullCountENNReal n history arm = n + 1

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

theorem sum_finiteHistoryPullCountReal {K : Nat} {Reward : Type*} (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) : ∑ arm : Fin K, finiteHistoryPullCountReal n history arm = n + 1

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

theorem finiteHistoryPullCountReal_nonneg {K : Nat} {Reward : Type*} (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) (arm : Fin K) : 0 ≤ finiteHistoryPullCountReal n history arm

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

theorem measurable_finiteHistoryPullCountReal {K : Nat} {Reward : Type*} [MeasurableSpace Reward] (n : Nat) (arm : Fin K) : Measurable (fun history : History.FinitePairHistory (Fin K) Reward n => finiteHistoryPullCountReal n history arm)

Event integration lower bound in the exact real-probability convention used by the Bretagnolle--Huber theorem.

theorem ofReal_mul_probReal_le_lintegral_of_event {alpha : Type*} [MeasurableSpace alpha] {mu : Measure alpha} [IsFiniteMeasure mu] {A : Set alpha} (hA : MeasurableSet A) {c : Real} (hc : 0 ≤ c) {f : alpha -> ENNReal} (hf : forall x, x ∈ A -> ENNReal.ofReal c ≤ f x) : ENNReal.ofReal (c * mu.real A) ≤ ∫⁻ x, f x ∂mu

A rigorous rational lower bound for the testing constant in the source proof.

theorem sixteen_div_twentySeven_le_exp_neg_half : (16 / 27 : Real) ≤ Real.exp (-(1 / 2 : Real))

A unit-cube Gaussian environment together with a certified optimal arm. The optimal-arm field is proof data; the induced reward kernel depends only on `mean`.

structure UnitGaussianBanditEnvironment (K : Nat) where

The stationary reward kernel induced by a finite vector of Gaussian means.

noncomputable abbrev unitGaussianKernel {K : Nat} (mean : Fin K -> Real) : Kernel (Fin K) Real

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

theorem unitGaussianKernel_apply {K : Nat} (mean : Fin K -> Real) (arm : Fin K) : unitGaussianKernel mean arm = unitGaussianArm (mean arm)

Realized pseudo-regret on an inclusive finite history.

noncomputable def finiteHistoryGaussianPseudoRegret {K : Nat} (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Real lastRound) : ENNReal

Expected pseudo-regret under the canonical history law. This is the Lemma 4.5-equivalent gap-times-pull-count form of the source quantity `R_n`, represented in `ENNReal` to align with Mathlib's measure-KL API. The separate reward-sum-regret equality is not asserted by this definition.

noncomputable def gaussianExpectedPseudoRegret {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) : ENNReal

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

theorem measurable_finiteHistoryGaussianPseudoRegret {K : Nat} (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) : Measurable (finiteHistoryGaussianPseudoRegret environment lastRound)

Regrouping expected Gaussian pseudo-regret by arm pulls.

theorem gaussianExpectedPseudoRegret_eq_sum_expectedPulls {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) : gaussianExpectedPseudoRegret algorithm environment lastRound = ∑ arm : Fin K, ENNReal.ofReal (environment.mean environment.bestArm - environment.mean arm) * canonicalRealizedExpectedPullCountThrough algorithm (unitGaussianKernel environment.mean) lastRound arm

Every inclusive history contains exactly `lastRound + 1` pulls, hence so do the expected realized counts.

theorem sum_canonicalRealizedExpectedPullCountThrough {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (mean : Fin K -> Real) (lastRound : Nat) : ∑ arm : Fin K, canonicalRealizedExpectedPullCountThrough algorithm (unitGaussianKernel mean) lastRound arm = lastRound + 1

Real-valued first-environment expected pull count.

noncomputable def gaussianExpectedPullCountReal {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (mean : Fin K -> Real) (lastRound : Nat) (arm : Fin K) : Real

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

theorem gaussianExpectedPullCountReal_nonneg {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (mean : Fin K -> Real) (lastRound : Nat) (arm : Fin K) : 0 ≤ gaussianExpectedPullCountReal algorithm mean lastRound arm

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

theorem sum_gaussianExpectedPullCountReal {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (mean : Fin K -> Real) (lastRound : Nat) : ∑ arm : Fin K, gaussianExpectedPullCountReal algorithm mean lastRound arm = lastRound + 1

Base mean vector in the proof of Theorem 15.2: arm zero has mean `gap`, and every alternative has mean zero.

def gaussianMinimaxBaseMean {m : Nat} (gap : Real) : Fin (m + 1) -> Real

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

theorem gaussianMinimaxBaseMean_zero {m : Nat} (gap : Real) : gaussianMinimaxBaseMean (m := m) gap 0 = gap

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

theorem gaussianMinimaxBaseMean_succ {m : Nat} (gap : Real) (i : Fin m) : gaussianMinimaxBaseMean (m := m) gap i.succ = 0

Changed mean vector: the selected alternative `i.succ` is raised from zero to `2*gap`, while arm zero remains at `gap`.

def gaussianMinimaxChangedMean {m : Nat} (gap : Real) (i : Fin m) : Fin (m + 1) -> Real

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

theorem gaussianMinimaxChangedMean_selected {m : Nat} (gap : Real) (i : Fin m) : gaussianMinimaxChangedMean gap i i.succ = 2 * gap

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

theorem gaussianMinimaxChangedMean_zero {m : Nat} (gap : Real) (i : Fin m) : gaussianMinimaxChangedMean gap i 0 = gap

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

theorem gaussianMinimaxChangedMean_other {m : Nat} (gap : Real) {i j : Fin m} (hji : j ≠ i) : gaussianMinimaxChangedMean gap i j.succ = 0

Certified base environment.

noncomputable def gaussianMinimaxBaseEnvironment {m : Nat} (gap : Real) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) : UnitGaussianBanditEnvironment (m + 1) where

Certified changed environment with `i.succ` optimal.

noncomputable def gaussianMinimaxChangedEnvironment {m : Nat} (gap : Real) (i : Fin m) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) : UnitGaussianBanditEnvironment (m + 1) where

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

theorem finiteHistoryGaussianPseudoRegret_ne_top {K : Nat} (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Real lastRound) : finiteHistoryGaussianPseudoRegret environment lastRound history ≠ ∞

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

theorem finiteHistoryGaussianPseudoRegret_toReal {K : Nat} (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Real lastRound) : (finiteHistoryGaussianPseudoRegret environment lastRound history).toReal = ∑ arm : Fin K, (environment.mean environment.bestArm - environment.mean arm) * finiteHistoryPullCountReal lastRound history arm

The source event `A={T_0(n) <= n/2}`, in the repository's inclusive history convention.

def gaussianMinimaxBaseSmallPullEvent {m : Nat} (lastRound : Nat) : Set (History.FinitePairHistory (Fin (m + 1)) Real lastRound)

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

theorem measurableSet_gaussianMinimaxBaseSmallPullEvent {m : Nat} (lastRound : Nat) : MeasurableSet (gaussianMinimaxBaseSmallPullEvent (m := m) lastRound)

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

theorem finiteHistoryGaussianPseudoRegret_base_toReal {m : Nat} (gap : Real) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) (lastRound : Nat) (history : History.FinitePairHistory (Fin (m + 1)) Real lastRound) : (finiteHistoryGaussianPseudoRegret (gaussianMinimaxBaseEnvironment gap hgap hgap_le) lastRound history).toReal = gap * ((lastRound + 1 : Nat) - finiteHistoryPullCountReal lastRound history 0)

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

theorem finiteHistoryGaussianPseudoRegret_changed_toReal_lower {m : Nat} (gap : Real) (i : Fin m) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) (lastRound : Nat) (history : History.FinitePairHistory (Fin (m + 1)) Real lastRound) : gap * finiteHistoryPullCountReal lastRound history 0 ≤ (finiteHistoryGaussianPseudoRegret (gaussianMinimaxChangedEnvironment gap i hgap hgap_le) lastRound history).toReal

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

theorem base_event_forces_gaussianPseudoRegret {m : Nat} (gap : Real) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) (lastRound : Nat) (history : History.FinitePairHistory (Fin (m + 1)) Real lastRound) (hA : history ∈ gaussianMinimaxBaseSmallPullEvent (m := m) lastRound) : ENNReal.ofReal (((lastRound + 1 : Nat) : Real) * gap / 2) ≤ finiteHistoryGaussianPseudoRegret (gaussianMinimaxBaseEnvironment gap hgap hgap_le) lastRound history

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

theorem changed_complement_forces_gaussianPseudoRegret {m : Nat} (gap : Real) (i : Fin m) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) (lastRound : Nat) (history : History.FinitePairHistory (Fin (m + 1)) Real lastRound) (hAc : history ∈ (gaussianMinimaxBaseSmallPullEvent (m := m) lastRound)ᶜ) : ENNReal.ofReal (((lastRound + 1 : Nat) : Real) * gap / 2) ≤ finiteHistoryGaussianPseudoRegret (gaussianMinimaxChangedEnvironment gap i hgap hgap_le) lastRound history

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

theorem base_event_probability_lower_bound {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) (lastRound : Nat) : ENNReal.ofReal ((((lastRound + 1 : Nat) : Real) * gap / 2) * (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxBaseMean gap)) lastRound).real (gaussianMinimaxBaseSmallPullEvent (m := m) lastRound)) ≤ gaussianExpectedPseudoRegret algorithm (gaussianMinimaxBaseEnvironment gap hgap hgap_le) lastRound

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

theorem changed_complement_probability_lower_bound {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (i : Fin m) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) (lastRound : Nat) : ENNReal.ofReal ((((lastRound + 1 : Nat) : Real) * gap / 2) * (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxChangedMean gap i)) lastRound).real (gaussianMinimaxBaseSmallPullEvent (m := m) lastRound)ᶜ) ≤ gaussianExpectedPseudoRegret algorithm (gaussianMinimaxChangedEnvironment gap i hgap hgap_le) lastRound

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

theorem klDiv_unitGaussianKernel_base_changed {m : Nat} (gap : Real) (i j : Fin m) : InformationTheory.klDiv (unitGaussianKernel (gaussianMinimaxBaseMean gap) j.succ) (unitGaussianKernel (gaussianMinimaxChangedMean gap i) j.succ) = if j = i then ENNReal.ofReal (2 * gap ^ 2) else 0

Lemma 15.1 specialized to the source's base/changed Gaussian pair: only the selected alternative contributes to the directed history KL.

theorem klDiv_gaussianMinimax_base_changed_history {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (i : Fin m) (lastRound : Nat) : InformationTheory.klDiv (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxBaseMean gap)) lastRound) (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxChangedMean gap i)) lastRound) = canonicalRealizedExpectedPullCountThrough algorithm (unitGaussianKernel (gaussianMinimaxBaseMean gap)) lastRound i.succ * ENNReal.ofReal (2 * gap ^ 2)

Least-explored alternative under the actual base Gaussian history law.

theorem exists_gaussianMinimax_leastExploredAlternative {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (lastRound : Nat) : ∃ i : Fin m, gaussianExpectedPullCountReal algorithm (gaussianMinimaxBaseMean gap) lastRound i.succ ≤ ((lastRound + 1 : Nat) : Real) / (m : Real)

The source gap choice makes the selected base-to-changed history KL at most `1/2`.

theorem exists_gaussianMinimax_historyKL_le_half {m horizon : Nat} (hm : 0 < m) (hmhorizon : m ≤ horizon) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) : let gap := gaussianMinimaxGap (m : Real) (horizon : Real) ∃ i : Fin m, InformationTheory.klDiv (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxBaseMean gap)) (horizon - 1)) (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxChangedMean gap i)) (horizon - 1)) ≤ ENNReal.ofReal (1 / 2 : Real)

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

theorem horizon_mul_gaussianMinimaxGap_eq_half_sqrt {alternativeCount horizon : Real} (halternatives : 0 ≤ alternativeCount) (hhorizon : 0 < horizon) : horizon * gaussianMinimaxGap alternativeCount horizon = Real.sqrt (alternativeCount * horizon) / 2

Quantitative two-environment conclusion in the exact source constant. For every policy, one of the source's base/changed unit-Gaussian bandits has expected pseudo-regret at least `sqrt(m*n)/27`.

theorem exists_unitGaussianBandit_expectedPseudoRegret_ge_sqrt_div_twentySeven {m horizon : Nat} (hm : 0 < m) (hmhorizon : m ≤ horizon) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) : let gap := gaussianMinimaxGap (m : Real) (horizon : Real) ∃ i : Fin m, ENNReal.ofReal ((1 / 27 : Real) * Real.sqrt ((m : Real) * (horizon : Real))) ≤ max (gaussianExpectedPseudoRegret algorithm (gaussianMinimaxBaseEnvironment gap (show 0 ≤ gaussianMinimaxGap (m : Real) (horizon : Real) from Real.sqrt_nonneg _) (gaussianMinimaxGap_le_half (show (0 : Real) < (horizon : Real) by exact_mod_cast lt_of_lt_of_le hm hmhorizon) (by exact_mod_cast hmhorizon))) (horizon - 1)) (gaussianExpectedPseudoRegret algorithm (gaussianMinimaxChangedEnvironment gap i (show 0 ≤ gaussianMinimaxGap (m : Real) (horizon : Real) from Real.sqrt_nonneg _) (gaussianMinimaxGap_le_half (show (0 : Real) < (horizon : Real) by exact_mod_cast lt_of_lt_of_le hm hmhorizon) (by exact_mod_cast hmhorizon))) (horizon - 1))

Source-facing existence form of Theorem 15.2 with `m=k-1`. The returned environment records both the unit-cube mean vector and a genuinely optimal arm; its reward law is the corresponding unit-variance Gaussian bandit.

theorem exists_unitGaussianBanditEnvironment_expectedPseudoRegret_ge {m horizon : Nat} (hm : 0 < m) (hmhorizon : m ≤ horizon) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) : ∃ environment : UnitGaussianBanditEnvironment (m + 1), ENNReal.ofReal ((1 / 27 : Real) * Real.sqrt ((m : Real) * (horizon : Real))) ≤ gaussianExpectedPseudoRegret algorithm environment (horizon - 1)

*Lattimore--Szepesvari, Theorem 15.2.** For `k>1`, `n≥k-1`, and every possibly randomized nonanticipating policy, there exists a mean vector in `[0,1]^k` for which the unit-variance Gaussian bandit has expected pseudo-regret at least `sqrt((k-1)n)/27`. The local history parameter is `n-1`, hence contains exactly `n` observations.

theorem finiteArmedGaussianMinimaxLowerBound {k horizon : Nat} (hk : 1 < k) (hkhorizon : k - 1 ≤ horizon) (algorithm : Thompson.HistoryAlgorithm (Fin k) Real) : ∃ environment : UnitGaussianBanditEnvironment k, ENNReal.ofReal ((1 / 27 : Real) * Real.sqrt (((k - 1 : Nat) : Real) * (horizon : Real))) ≤ gaussianExpectedPseudoRegret algorithm environment (horizon - 1)

Worst-case expected pseudo-regret over all unit-cube, unit-variance Gaussian environments.

noncomputable def unitGaussianWorstCaseExpectedPseudoRegret (K : Nat) (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (lastRound : Nat) : ENNReal

Minimax expected pseudo-regret over stochastic finite-history policies.

noncomputable def unitGaussianMinimaxExpectedPseudoRegret (K lastRound : Nat) : ENNReal

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

theorem unitGaussianWorstCaseExpectedPseudoRegret_ge {k horizon : Nat} (hk : 1 < k) (hkhorizon : k - 1 ≤ horizon) (algorithm : Thompson.HistoryAlgorithm (Fin k) Real) : ENNReal.ofReal ((1 / 27 : Real) * Real.sqrt (((k - 1 : Nat) : Real) * (horizon : Real))) ≤ unitGaussianWorstCaseExpectedPseudoRegret k algorithm (horizon - 1)

Minimax form of Theorem 15.2.

theorem unitGaussianMinimaxExpectedPseudoRegret_ge {k horizon : Nat} (hk : 1 < k) (hkhorizon : k - 1 ≤ horizon) : ENNReal.ofReal ((1 / 27 : Real) * Real.sqrt (((k - 1 : Nat) : Real) * (horizon : Real))) ≤ unitGaussianMinimaxExpectedPseudoRegret k (horizon - 1)

Chapter 13's coarser `c*sqrt(k*n)` statement, now discharged from the exact Chapter 15 constant. The explicit universal choice here is `c=1/54`; the source only asks for existence of a positive universal constant.

theorem unitGaussianMinimaxExpectedPseudoRegret_ge_one_div_fiftyFour_sqrt {k horizon : Nat} (hk : 1 < k) (hkhorizon : k ≤ horizon) : ENNReal.ofReal ((1 / 54 : Real) * Real.sqrt ((k : Real) * (horizon : Real))) ≤ unitGaussianMinimaxExpectedPseudoRegret k (horizon - 1)