BanditRLProof.LowerBounds.HighProbability

The tail event used throughout Chapter 17: the realized quantity is at least the displayed lower-bound threshold.

def tailAtLeast {Omega : Type*} (quantity : Omega -> Real) (threshold : Real) : Set Omega

The exact threshold inside Theorem 17.1, with `alternativeArms = k - 1`. The theorem's factor `1/4` multiplies the whole minimum.

def stochasticHighProbabilityThreshold (horizon alternativeArms : Nat) (B delta : Real) : Real

The exact threshold in Corollary 17.2, again with `alternativeArms = k - 1`.

def stochasticMinimaxHighProbabilityThreshold (horizon alternativeArms : Nat) (delta : Real) : Real

The threshold shape in Theorem 17.4. The universal constant `c` remains an explicit argument, and the logarithm is `log (1 / (2 * delta))`.

def adversarialHighProbabilityThreshold (horizon arms : Nat) (c delta : Real) : Real

The stochastic random pseudo-regret from Section 17.1, evaluated on one realized canonical finite history. It is deliberately separate from the deterministic expected pseudo-regret below.

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

The deterministic expected pseudo-regret presentation used in Eq. (17.4), written as expected pull counts times gaps (the Lemma 4.5 identity). This is not the random pseudo-regret and is not adversarial random regret.

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

The source class `E^k`: unit-variance Gaussian arms with gaps bounded by one, without an artificial absolute restriction on the means.

structure GapOneGaussianBanditEnvironment (K : Nat) where

Deterministic expected pseudo-regret for the full source class `E^k`.

noncomputable def gapOneGaussianExpectedPseudoRegretReal {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : GapOneGaussianBanditEnvironment K) (lastRound : Nat) : Real

The stochastic random pseudo-regret on the full source class `E^k`. Unlike `gapOneGaussianExpectedPseudoRegretReal`, this is a random variable on the realized finite history.

noncomputable def gapOneGaussianRandomPseudoRegret {K : Nat} (environment : GapOneGaussianBanditEnvironment K) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Real lastRound) : Real

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

def UnitGaussianBanditEnvironment.toGapOne {K : Nat} (environment : UnitGaussianBanditEnvironment K) : GapOneGaussianBanditEnvironment K where

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

theorem gapOneGaussianExpectedPseudoRegretReal_toGapOne {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) : gapOneGaussianExpectedPseudoRegretReal algorithm environment.toGapOne lastRound = gaussianExpectedPseudoRegretReal algorithm environment lastRound

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

theorem gapOneGaussianRandomPseudoRegret_toGapOne {K : Nat} (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Real lastRound) : gapOneGaussianRandomPseudoRegret environment.toGapOne lastRound history = gaussianRandomPseudoRegret environment lastRound history

The exact gap selected in the proof of Theorem 17.1.

noncomputable def stochasticHighProbabilityGap (horizon alternativeArms : Nat) (B delta : Real) : Real

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

theorem gaussianRandomPseudoRegret_nonneg {K : Nat} (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Real lastRound) : 0 <= gaussianRandomPseudoRegret environment lastRound history

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

theorem measurable_gaussianRandomPseudoRegret {K : Nat} (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) : Measurable (gaussianRandomPseudoRegret environment lastRound)

Unit-cube gaps and the exact pull-count sum bound stochastic random pseudo-regret by the number of observed rounds.

theorem gaussianRandomPseudoRegret_le_horizon {K : Nat} (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Real lastRound) : gaussianRandomPseudoRegret environment lastRound history <= (lastRound + 1 : Nat)

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

theorem integrable_gaussianRandomPseudoRegret {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) : Integrable (gaussianRandomPseudoRegret environment lastRound) (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) lastRound)

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

theorem gaussianExpectedPseudoRegret_toReal_eq {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) : (gaussianExpectedPseudoRegret algorithm environment lastRound).toReal = gaussianExpectedPseudoRegretReal algorithm environment lastRound

The deterministic expected pseudo-regret surface is the integral of the random pseudo-regret under the same policy/environment history law.

theorem integral_gaussianRandomPseudoRegret_eq_expected {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) : ∫ history, gaussianRandomPseudoRegret environment lastRound history ∂canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) lastRound = gaussianExpectedPseudoRegretReal algorithm environment lastRound

Integrating a nonnegative bounded random variable after splitting at one measurable upper-tail event.

theorem integral_le_threshold_add_bound_mul_tailMass {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (quantity : Omega -> Real) (threshold bound : Real) (hmeas : Measurable quantity) (hintegrable : Integrable quantity mu) (hthreshold : 0 <= threshold) (hbound : forall omega, quantity omega <= bound) : ∫ omega, quantity omega ∂mu <= threshold + bound * mu.real (tailAtLeast quantity threshold)

In the base environment, expected pseudo-regret is exactly the common alternative gap times the sum of the alternative expected pull counts.

theorem gaussianExpectedPseudoRegretReal_base_eq {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (hgap : 0 <= gap) (hgap_le : gap <= 1 / 2) (lastRound : Nat) : gaussianExpectedPseudoRegretReal algorithm (gaussianMinimaxBaseEnvironment gap hgap hgap_le) lastRound = gap * ∑ i : Fin m, gaussianExpectedPullCountReal algorithm (gaussianMinimaxBaseMean gap) lastRound i.succ

Positive-horizon square-root normalization used by the exact Chapter 17 gap calibration.

theorem horizon_mul_sqrt_div_eq_sqrt_mul {horizon alternatives : Real} (hhorizon : 0 < horizon) (halternatives : 0 <= alternatives) : horizon * Real.sqrt (alternatives / horizon) = Real.sqrt (horizon * alternatives)

The two square-root factors in the information exponent cancel exactly.

theorem sqrt_mul_mul_sqrt_div_eq_alternatives {horizon alternatives : Real} (hhorizon : 0 < horizon) (halternatives : 0 <= alternatives) : Real.sqrt (alternatives * horizon) * Real.sqrt (alternatives / horizon) = alternatives

The chosen source gap times half the horizon is exactly the threshold displayed in Theorem 17.1, including the outer factor `1/4`.

theorem horizon_mul_stochasticHighProbabilityGap_div_two (horizon alternatives : Nat) (B delta : Real) (hhorizon : 0 < horizon) (hB : 0 < B) : (horizon : Real) * stochasticHighProbabilityGap horizon alternatives B delta / 2 = stochasticHighProbabilityThreshold horizon alternatives B delta

Exact scalar information calibration in the positive-logarithm branch of Theorem 17.1.

theorem stochasticHighProbability_informationExponent_le_log (horizon alternatives : Nat) (B delta : Real) (hhorizon : 0 < horizon) (halternatives : 0 < alternatives) (hB : 0 < B) (hlog : 0 < Real.log (1 / (4 * delta))) : let gap := stochasticHighProbabilityGap horizon alternatives B delta (B * Real.sqrt ((alternatives : Real) * (horizon : Real)) / (gap * (alternatives : Real))) * (2 * gap ^ 2) <= Real.log (1 / (4 * delta))

The positive-logarithm branch of Lattimore--Szepesvari Theorem 17.1. The algorithm is one common randomized nonanticipating history policy in the base and changed environments. The expected-regret premise is deterministic; the conclusion is a tail probability for random pseudo-regret.

theorem gaussianRandomPseudoRegret_ge_theorem17_1_of_four_mul_delta_lt_one {alternatives horizon : Nat} (halternatives : 0 < alternatives) (hhorizon : 0 < horizon) (B delta : Real) (hB : 0 < B) (hdelta : 0 < delta) (hfourDelta : 4 * delta < 1) (algorithm : Thompson.HistoryAlgorithm (Fin (alternatives + 1)) Real) (hExpected : forall environment : UnitGaussianBanditEnvironment (alternatives + 1), gaussianExpectedPseudoRegretReal algorithm environment (horizon - 1) <= B * Real.sqrt ((alternatives : Real) * (horizon : Real))) : exists environment : UnitGaussianBanditEnvironment (alternatives + 1), delta <= (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) (horizon - 1)).real (tailAtLeast (gaussianRandomPseudoRegret environment (horizon - 1)) (stochasticHighProbabilityThreshold horizon alternatives B delta))

*Lattimore--Szepesvari, Theorem 17.1.** A single policy whose deterministic expected pseudo-regret is uniformly at most `B * sqrt ((k-1) * n)` on the unit-cube subfamily has a unit-Gaussian environment whose random pseudo-regret exceeds the exact source threshold with probability at least `delta`. This internal theorem is stronger than the printed result because it assumes the uniform bound only on the unit-cube Gaussian subfamily used by the proof. The public source-class wrapper below restores the printed `E^k` premise.

theorem gaussianRandomPseudoRegret_ge_theorem17_1_unitCube {alternatives horizon : Nat} (halternatives : 0 < alternatives) (hhorizon : 0 < horizon) (B delta : Real) (hB : 0 < B) (hdelta : 0 < delta) (hdelta_one : delta < 1) (algorithm : Thompson.HistoryAlgorithm (Fin (alternatives + 1)) Real) (hExpected : forall environment : UnitGaussianBanditEnvironment (alternatives + 1), gaussianExpectedPseudoRegretReal algorithm environment (horizon - 1) <= B * Real.sqrt ((alternatives : Real) * (horizon : Real))) : exists environment : UnitGaussianBanditEnvironment (alternatives + 1), delta <= (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) (horizon - 1)).real (tailAtLeast (gaussianRandomPseudoRegret environment (horizon - 1)) (stochasticHighProbabilityThreshold horizon alternatives B delta))

Theorem 17.1 with the premise quantified over the full source class `E^k` of unit-variance Gaussian bandits whose gaps are at most one. The hard witness lies in the unit-cube subfamily, which is embedded into `E^k`.

theorem gaussianRandomPseudoRegret_ge_theorem17_1 {alternatives horizon : Nat} (halternatives : 0 < alternatives) (hhorizon : 0 < horizon) (B delta : Real) (hB : 0 < B) (hdelta : 0 < delta) (hdelta_one : delta < 1) (algorithm : Thompson.HistoryAlgorithm (Fin (alternatives + 1)) Real) (hExpected : forall environment : GapOneGaussianBanditEnvironment (alternatives + 1), gapOneGaussianExpectedPseudoRegretReal algorithm environment (horizon - 1) <= B * Real.sqrt ((alternatives : Real) * (horizon : Real))) : exists environment : UnitGaussianBanditEnvironment (alternatives + 1), delta <= (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) (horizon - 1)).real (tailAtLeast (gaussianRandomPseudoRegret environment (horizon - 1)) (stochasticHighProbabilityThreshold horizon alternatives B delta))

The square-root identity used to specialize Theorem 17.1 in Corollary 17.2. Keeping it separate makes the source constant `B = sqrt (2 log (1/(4δ)))` mechanically visible.

theorem stochasticMinimax_sourceTerm_eq {horizon alternatives : Nat} (delta : Real) (hlog : 0 < Real.log (1 / (4 * delta))) : (1 / Real.sqrt (2 * Real.log (1 / (4 * delta)))) * Real.sqrt ((alternatives : Real) * (horizon : Real)) * Real.log (1 / (4 * delta)) = Real.sqrt (((horizon : Real) * (alternatives : Real) / 2) * Real.log (1 / (4 * delta)))

The Theorem 17.1 threshold at the source choice of `B` is exactly the Corollary 17.2 minimax threshold.

theorem stochasticHighProbabilityThreshold_at_minimax_scale {horizon alternatives : Nat} (delta : Real) (hlog : 0 < Real.log (1 / (4 * delta))) : stochasticHighProbabilityThreshold horizon alternatives (Real.sqrt (2 * Real.log (1 / (4 * delta)))) delta = stochasticMinimaxHighProbabilityThreshold horizon alternatives delta

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

theorem stochasticMinimaxHighProbabilityThreshold_le_quarter_root {horizon alternatives : Nat} (delta : Real) (hlog : 0 <= Real.log (1 / (4 * delta))) : stochasticMinimaxHighProbabilityThreshold horizon alternatives delta <= (1 / 4 : Real) * Real.sqrt ((horizon : Real) * (alternatives : Real) * Real.log (1 / (4 * delta)))

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

theorem minimax_expected_scale_identity {horizon alternatives : Nat} (delta : Real) (hlog : 0 <= Real.log (1 / (4 * delta))) : Real.sqrt (2 * Real.log (1 / (4 * delta))) * Real.sqrt ((alternatives : Real) * (horizon : Real)) = Real.sqrt 2 * Real.sqrt ((horizon : Real) * (alternatives : Real) * Real.log (1 / (4 * delta)))

The analytic inequality quoted in Corollary 17.3: `integral_0^infinity exp (-x^(1/p)) dx <= 1` for `0<p<1`. The change of variables identifies the integral with `Gamma (p+1)`; convexity of Gamma between one and two gives the bound.

theorem integral_exp_neg_rpow_inv_le_one {p : Real} (hp : 0 < p) (hp_one : p < 1) : (∫ x : Real in Set.Ioi 0, Real.exp (-(x ^ (1 / p)))) <= 1

Integrating an all-confidence stretched-exponential tail gives the first-moment bound used by Corollary 17.3. The strict source tail is retained at the caller; only its weak consequence is needed under the integral.

theorem integral_le_scale_of_all_rpow_log_tail {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (quantity : Omega -> Real) (scale p : Real) (hscale : 0 < scale) (hp : 0 < p) (hp_one : p < 1) (hintegrable : Integrable quantity mu) (hnonneg : forall omega, 0 <= quantity omega) (htail : forall delta : Real, 0 < delta -> delta < 1 -> mu.real (tailAtLeast quantity (scale * (Real.log (1 / delta)) ^ p)) < delta) : (∫ omega, quantity omega ∂mu) <= scale

*Lattimore--Szepesvari, Corollary 17.2.** Under the exact side condition in Eq. (17.6), every policy has a unit-Gaussian instance whose random pseudo-regret reaches the minimax high-probability threshold with probability at least `delta`.

theorem gaussianRandomPseudoRegret_ge_corollary17_2 {alternatives horizon : Nat} (halternatives : 0 < alternatives) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta < 1) (hside : (horizon : Real) * delta <= Real.sqrt ((horizon : Real) * (alternatives : Real) * Real.log (1 / (4 * delta)))) (algorithm : Thompson.HistoryAlgorithm (Fin (alternatives + 1)) Real) : exists environment : UnitGaussianBanditEnvironment (alternatives + 1), delta <= (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) (horizon - 1)).real (tailAtLeast (gaussianRandomPseudoRegret environment (horizon - 1)) (stochasticMinimaxHighProbabilityThreshold horizon alternatives delta))

*Lattimore--Szepesvari, Corollary 17.3.** No single policy has a strictly smaller than `delta` random-pseudo-regret tail at every horizon, confidence level, and environment in the full gap-at-most-one Gaussian class when the logarithmic exponent lies in `(0,1)`.

theorem noUniformGaussianRandomPseudoRegretTail_corollary17_3 {alternatives : Nat} (halternatives : 0 < alternatives) (p B : Real) (hp : 0 < p) (hp_one : p < 1) (hB : 0 < B) : ¬ exists algorithm : Thompson.HistoryAlgorithm (Fin (alternatives + 1)) Real, forall horizon : Nat, 0 < horizon -> forall delta : Real, 0 < delta -> delta < 1 -> forall environment : GapOneGaussianBanditEnvironment (alternatives + 1), (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) (horizon - 1)).real (tailAtLeast (gapOneGaussianRandomPseudoRegret environment (horizon - 1)) (B * Real.sqrt ((alternatives : Real) * (horizon : Real)) * (Real.log (1 / delta)) ^ p)) < delta

Claim 17.5 in its abstract first-moment form. If the average tail mass is at least `delta`, some deterministic instance has tail mass at least `delta`. The textbook suppresses the regularity needed to write the expectation. Lean makes it explicit as `Integrable tailMass Q`; `Q` is explicitly a probability measure.

theorem exists_tailMass_ge_of_integral_ge {Instance : Type*} [MeasurableSpace Instance] (Q : Measure Instance) [IsProbabilityMeasure Q] (tailMass : Instance -> Real) (delta : Real) (hIntegrable : Integrable tailMass Q) (hAverage : delta <= ∫ x, tailMass x ∂Q) : exists x, delta <= tailMass x

Claim 17.5 specialized to the source notation `1 - F_x(u)`.

theorem exists_cdfTail_ge_of_integral_ge {Instance : Type*} [MeasurableSpace Instance] (Q : Measure Instance) [IsProbabilityMeasure Q] (cdf : Instance -> Real -> Real) (threshold delta : Real) (hIntegrable : Integrable (fun x => 1 - cdf x threshold) Q) (hAverage : delta <= ∫ x, 1 - cdf x threshold ∂Q) : exists x, delta <= 1 - cdf x threshold

Probability subtraction used after Claims 17.6 and 17.7. If the pull-count event has probability at least `2 * delta` and the clipping event has probability at most `delta`, their good difference has probability at least `delta`. No measurability hypothesis is hidden: `Measure.real` is defined for all sets, and `le_measureReal_diff` is an outer-measure inequality.

theorem measureReal_diff_ge_delta {Omega : Type*} [MeasurableSpace Omega] (P : Measure Omega) [IsFiniteMeasure P] (pullSmall clippingBad : Set Omega) (delta : Real) (hPullSmall : 2 * delta <= P.real pullSmall) (hClippingBad : P.real clippingBad <= delta) : delta <= P.real (pullSmall \ clippingBad)

The deterministic lower expression on the right-hand side of Eq. (17.8), after writing the pull and clipping counts as real numbers.

def adversarialRegretLowerExpression (horizon pullCount clippingCount : Nat) (gap : Real) : Real

If fewer than half of the rounds pull the distinguished arm and at most a quarter are clipped, the Eq. (17.8) lower expression is at least one quarter of `gap * horizon`.

theorem adversarialRegretLowerExpression_ge_quarter (horizon pullCount clippingCount : Nat) (gap : Real) (hGap : 0 <= gap) (hPull : (pullCount : Real) <= (horizon : Real) / 2) (hClipping : (clippingCount : Real) <= (horizon : Real) / 4) : gap * ((horizon : Real) / 4) <= adversarialRegretLowerExpression horizon pullCount clippingCount gap

The explicit transfer from Eq. (17.8) to the quarter-horizon regret threshold. The premise `hSource` is exactly the construction-specific part that Chapter 17 must still supply.

theorem randomRegret_ge_quarter_of_clippingDecomposition (horizon pullCount clippingCount : Nat) (gap randomRegret : Real) (hGap : 0 <= gap) (hPull : (pullCount : Real) <= (horizon : Real) / 2) (hClipping : (clippingCount : Real) <= (horizon : Real) / 4) (hSource : adversarialRegretLowerExpression horizon pullCount clippingCount gap <= randomRegret) : gap * ((horizon : Real) / 4) <= randomRegret

Clipping to the reward interval `[0,1]`.

def clipUnitReward (x : Real) : Real

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

theorem clipUnitReward_mono {x y : Real} (hxy : x <= y) : clipUnitReward x <= clipUnitReward y

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

theorem clipUnitReward_eq_self {x : Real} (hx0 : 0 <= x) (hx1 : x <= 1) : clipUnitReward x = x

The source hard-family shift: arm zero receives `gap`, the distinguished nonzero arm receives `2*gap`, and every other arm receives zero.

def adversarialHardShift {alternatives : Nat} (gap : Real) (distinguished : Fin alternatives) (arm : Fin (alternatives + 1)) : Real

The exact pre-sampled construction underlying Theorem 17.4. One scalar `eta t` is shared by every arm at round `t`; hence the arm rewards are correlated within a round. Independence and standard-Gaussian assumptions belong to the law of the path `eta`, not to this pathwise definition.

def adversarialClippedGaussianReward {horizon alternatives : Nat} (eta : Fin horizon -> Real) (gap : Real) (distinguished : Fin alternatives) (t : Fin horizon) (arm : Fin (alternatives + 1)) : Real

The IID centered-Gaussian path law used by the equivalent centered form of the source construction. Adding `1/2` in `adversarialClippedGaussianReward` makes `1/2 + eta t` have the source law `N(1/2, sigma^2)`.

noncomputable def adversarialCenteredNoiseLaw (horizon : Nat) (sigma : Real) : Measure (Fin horizon -> Real)

One observed arm's marginal in the clipped Gaussian construction. The joint reward matrix still uses a shared noise coordinate for all arms.

noncomputable def adversarialClippedArmLaw (sigma shift : Real) : Measure Real

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

theorem measurable_adversarialClippedArmMap (shift : Real) : Measurable (fun x : Real => clipUnitReward (1 / 2 + x + shift))

Finite-arm observation kernel, parameterized also for the base family used in Claim 17.6.

noncomputable abbrev adversarialClippedKernel {K : Nat} (sigma : Real) (shift : Fin K -> Real) : Kernel (Fin K) Real

The observable history law under a fixed randomized policy and the clipped Gaussian feedback kernel. This is not a law on full reward matrices.

noncomputable def adversarialClippedHistoryLaw {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (sigma : Real) (shift : Fin K -> Real) (lastRound : Nat) : Measure (History.FinitePairHistory (Fin K) Real lastRound)

A coordinate of the shared-noise matrix has exactly the arm marginal used by the observation kernel. This retains the original product noise law.

theorem adversarialCenteredNoiseLaw_reward_marginal {horizon alternatives : Nat} (sigma gap : Real) (distinguished : Fin alternatives) (t : Fin horizon) (arm : Fin (alternatives + 1)) : (adversarialCenteredNoiseLaw horizon sigma).map (fun eta => adversarialClippedGaussianReward eta gap distinguished t arm) = adversarialClippedArmLaw sigma (adversarialHardShift gap distinguished arm)

Clip the observed reward coordinates while retaining every action.

def adversarialClipHistory {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : History.FinitePairHistory (Fin K) Real n

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

theorem measurable_adversarialClipHistory {K : Nat} (n : Nat) : Measurable (adversarialClipHistory (K := K) n)

Lift the original policy to unbounded observations by feeding it only the clipped history. This construction is independent of the hard instance.

noncomputable def adversarialClipHistoryAlgorithm {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) : Thompson.HistoryAlgorithm (Fin K) Real where

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

theorem adversarialClipHistoryAlgorithm_policy_apply {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : (adversarialClipHistoryAlgorithm algorithm).policy n history = algorithm.policy n (adversarialClipHistory n history)

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

theorem adversarialClipHistory_pullCount {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : finiteHistoryPullCountENNReal n (adversarialClipHistory n history) arm = finiteHistoryPullCountENNReal n history arm

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

theorem adversarialClipHistory_pullCountReal {K : Nat} (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : finiteHistoryPullCountReal n (adversarialClipHistory n history) arm = finiteHistoryPullCountReal n history arm

Unclipped feedback law used with the lifted policy.

noncomputable abbrev adversarialUnclippedKernel {K : Nat} (sigma : Real) (shift : Fin K -> Real) : Kernel (Fin K) Real

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

theorem adversarialClippedKernel_eq_map {K : Nat} (sigma : Real) (shift : Fin K -> Real) : adversarialClippedKernel sigma shift = (adversarialUnclippedKernel sigma shift).map clipUnitReward

Initial action/reward law transport for the original and lifted policy.

theorem adversarialClipped_initialPairLaw {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (sigma : Real) (shift : Fin K -> Real) : algorithm.initialAction ⊗ₘ adversarialClippedKernel sigma shift = ((adversarialClipHistoryAlgorithm algorithm).initialAction ⊗ₘ adversarialUnclippedKernel sigma shift).map (Prod.map id clipUnitReward)

The exact observable history transport at the first observation.

theorem adversarialClippedHistoryLaw_zero {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (sigma : Real) (shift : Fin K -> Real) : adversarialClippedHistoryLaw algorithm sigma shift 0 = (canonicalBanditHistoryMeasure (adversarialClipHistoryAlgorithm algorithm) (adversarialUnclippedKernel sigma shift) 0).map (adversarialClipHistory 0)

Pointwise transport of the next action/reward pair after a history.

theorem adversarialClipped_historyStepLaw {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (sigma : Real) (shift : Fin K -> Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : Thompson.historyStepKernel algorithm (stationaryBanditHistoryEnvironment (adversarialClippedKernel sigma shift)) n (adversarialClipHistory n history) = (Thompson.historyStepKernel (adversarialClipHistoryAlgorithm algorithm) (stationaryBanditHistoryEnvironment (adversarialUnclippedKernel sigma shift)) n history).map (Prod.map id clipUnitReward)

Integrate the pointwise next-pair transport over any prefix law.

theorem adversarialClipped_prefixStepLaw {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (sigma : Real) (shift : Fin K -> Real) (n : Nat) (P : Measure (History.FinitePairHistory (Fin K) Real n)) [IsProbabilityMeasure P] : P.map (adversarialClipHistory n) ⊗ₘ Thompson.historyStepKernel algorithm (stationaryBanditHistoryEnvironment (adversarialClippedKernel sigma shift)) n = (P ⊗ₘ Thompson.historyStepKernel (adversarialClipHistoryAlgorithm algorithm) (stationaryBanditHistoryEnvironment (adversarialUnclippedKernel sigma shift)) n).map (Prod.map (adversarialClipHistory n) (Prod.map id clipUnitReward))

Exact transport of the entire finite observed history under the same original policy and its clipped-history lift.

theorem adversarialClippedHistoryLaw_eq_map {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (sigma : Real) (shift : Fin K -> Real) (n : Nat) : adversarialClippedHistoryLaw algorithm sigma shift n = (canonicalBanditHistoryMeasure (adversarialClipHistoryAlgorithm algorithm) (adversarialUnclippedKernel sigma shift) n).map (adversarialClipHistory n)

Pull-count events are preserved by the full history transport.

theorem adversarialClippedHistoryLaw_pullSmall {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (sigma : Real) (shift : Fin K -> Real) (n : Nat) (arm : Fin K) (threshold : Real) : (adversarialClippedHistoryLaw algorithm sigma shift n) {h | finiteHistoryPullCountReal n h arm < threshold} = (canonicalBanditHistoryMeasure (adversarialClipHistoryAlgorithm algorithm) (adversarialUnclippedKernel sigma shift) n) {h | finiteHistoryPullCountReal n h arm < threshold}

Identify the unbounded observation marginal as the exact shifted Gaussian.

theorem adversarialUnclippedKernel_apply {K : Nat} (sigma : Real) (shift : Fin K -> Real) (arm : Fin K) : adversarialUnclippedKernel sigma shift arm = gaussianReal (1 / 2 + shift arm) ⟨sigma ^ 2, sq_nonneg sigma⟩

Equal nonzero variance Gaussian KL, obtained by scaling the unit variance theorem through a measurable equivalence. Mathlib candidate.

theorem klDiv_gaussianReal_common_scale (sigma mu nu : Real) (hs : sigma ≠ 0) : InformationTheory.klDiv (gaussianReal mu ⟨sigma ^ 2, sq_nonneg sigma⟩) (gaussianReal nu ⟨sigma ^ 2, sq_nonneg sigma⟩) = ENNReal.ofReal ((mu - nu) ^ 2 / (2 * sigma ^ 2))

Directed per-arm information for the unbounded hard-family observations.

theorem klDiv_adversarialUnclippedKernel {K : Nat} (sigma : Real) (hs : sigma ≠ 0) (shift referenceShift : Fin K -> Real) (arm : Fin K) : InformationTheory.klDiv (adversarialUnclippedKernel sigma shift arm) (adversarialUnclippedKernel sigma referenceShift arm) = ENNReal.ofReal ((shift arm - referenceShift arm) ^ 2 / (2 * sigma ^ 2))

Exact first-law pull-count information identity for Claim 17.6's unclipped hard family. The same lifted policy is used on both sides.

theorem klDiv_adversarialUnclipped_base_changed_history {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (sigma gap : Real) (hs : sigma ≠ 0) (i : Fin m) (n : Nat) : InformationTheory.klDiv (canonicalBanditHistoryMeasure (adversarialClipHistoryAlgorithm algorithm) (adversarialUnclippedKernel sigma (gaussianMinimaxBaseMean gap)) n) (canonicalBanditHistoryMeasure (adversarialClipHistoryAlgorithm algorithm) (adversarialUnclippedKernel sigma (adversarialHardShift gap i)) n) = canonicalRealizedExpectedPullCountThrough (adversarialClipHistoryAlgorithm algorithm) (adversarialUnclippedKernel sigma (gaussianMinimaxBaseMean gap)) n i.succ * ENNReal.ofReal (2 * gap ^ 2 / sigma ^ 2)

The exact source tuning from Claim 17.6, with `alternatives = k - 1`.

noncomputable def adversarialClaim17_6Gap (horizon alternatives : Nat) (sigma delta : Real) : Real

Include the base instance as arm zero, as required by Claim 17.6.

def adversarialFullHardShift {m : Nat} (gap : Real) (distinguished arm : Fin (m + 1)) : Real

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

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

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

theorem adversarialFullHardShift_succ {m : Nat} (gap : Real) (i : Fin m) : adversarialFullHardShift gap i.succ = adversarialHardShift gap i

Source gap tuning cancels the least-arm information bound exactly.

theorem adversarialClaim17_6Gap_information_calibration {horizon m : Nat} (hn : 0 < horizon) (hm : 0 < m) (sigma delta : Real) (hs : sigma ≠ 0) (hd : 0 < delta) (hd8 : delta < 1 / 8) : ((horizon : Real) / m) * (2 * (adversarialClaim17_6Gap horizon m sigma delta) ^ 2 / sigma ^ 2) = Real.log (1 / (8 * delta))

Conservation of expected pulls for the lifted policy's unbounded law.

theorem sum_adversarialUnclipped_expectedPulls {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (sigma : Real) (shift : Fin K -> Real) (n : Nat) : (∑ arm : Fin K, canonicalRealizedExpectedPullCountThrough (adversarialClipHistoryAlgorithm algorithm) (adversarialUnclippedKernel sigma shift) n arm) = n + 1

Corrected Claim 17.6: the source strict inequality must be non-strict. The witness ranges over the base instance as well as all changed instances.

theorem adversarialClippedHistory_pull_le_half_claim17_6 {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (n : Nat) (sigma delta : Real) (hs : sigma ≠ 0) (hd : 0 < delta) (hd8 : delta < 1 / 8) : ∃ arm : Fin (m + 1), 2 * delta <= (adversarialClippedHistoryLaw algorithm sigma (adversarialFullHardShift (adversarialClaim17_6Gap (n + 1) m sigma delta) arm) n).real {h | finiteHistoryPullCountReal n h arm <= ((n + 1 : Nat) : Real) / 2}

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

theorem adversarialHardShift_distinguished {alternatives : Nat} (gap : Real) (distinguished : Fin alternatives) : adversarialHardShift gap distinguished distinguished.succ = 2 * gap

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

theorem adversarialHardShift_nonneg {alternatives : Nat} (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) (arm : Fin (alternatives + 1)) : 0 <= adversarialHardShift gap distinguished arm

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

theorem adversarialHardShift_le_two_mul {alternatives : Nat} (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) (arm : Fin (alternatives + 1)) : adversarialHardShift gap distinguished arm <= 2 * gap

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

theorem adversarialHardShift_le_gap_of_ne {alternatives : Nat} (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) (arm : Fin (alternatives + 1)) (hne : arm ≠ distinguished.succ) : adversarialHardShift gap distinguished arm <= gap

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

theorem adversarialClippedGaussianReward_distinguished_mono {horizon alternatives : Nat} (eta : Fin horizon -> Real) (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) (t : Fin horizon) (arm : Fin (alternatives + 1)) : adversarialClippedGaussianReward eta gap distinguished t arm <= adversarialClippedGaussianReward eta gap distinguished t distinguished.succ

Away from clipping, the distinguished arm beats every other arm by at least `gap`. This is the pointwise engine of Eq. (17.8).

theorem adversarialClippedGaussianReward_gap_of_not_clipped {horizon alternatives : Nat} (eta : Fin horizon -> Real) (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) (t : Fin horizon) (arm : Fin (alternatives + 1)) (hne : arm ≠ distinguished.succ) (hgood : |eta t| < 1 / 2 - 2 * gap) : gap <= adversarialClippedGaussianReward eta gap distinguished t distinguished.succ - adversarialClippedGaussianReward eta gap distinguished t arm

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

def adversarialPullCountReal {horizon alternatives : Nat} (actions : Fin horizon -> Fin (alternatives + 1)) (distinguished : Fin alternatives) : Real

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

def adversarialClippingCountReal {horizon : Nat} (eta : Fin horizon -> Real) (gap : Real) : Real

The Bernoulli indicator of a clipped round in the construction for Theorem 17.4.

def adversarialClipIndicator (gap x : Real) : Real

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

theorem measurable_adversarialClipIndicator (gap : Real) : Measurable (adversarialClipIndicator gap)

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

theorem adversarialClipIndicator_mem_Icc (gap x : Real) : adversarialClipIndicator gap x ∈ Set.Icc 0 1

The one-dimensional Gaussian tail estimate used in Claim 17.7. It is proved from Mathlib's sub-Gaussian Chernoff bound; the final numerical step is the degree-five lower Taylor bound for `exp (25/8)`.

theorem gaussianReal_tenth_abs_quarter_le_eighth : (gaussianReal 0 ⟨(1 / 10 : Real) ^ 2, sq_nonneg _⟩).real {x : Real | (1 / 4 : Real) <= |x|} <= 1 / 8

Each coordinate under the IID product law has the stated Gaussian marginal, specialized to the clipping indicator needed for Claim 17.7.

theorem integral_adversarialClipIndicator_eq {horizon : Nat} (gap : Real) (t : Fin horizon) : ∫ eta, adversarialClipIndicator gap (eta t) ∂(adversarialCenteredNoiseLaw horizon (1 / 10)) = (gaussianReal 0 ⟨(1 / 10 : Real) ^ 2, sq_nonneg _⟩).real {x : Real | 1 / 2 - 2 * gap <= |x|}

*Claim 17.7.** Under the source variance `sigma = 1/10`, if `gap < 1/8` and `n >= 32 log(1/delta)`, at most a `delta` fraction of noise paths have at least `n/4` clipped rounds.

theorem adversarialClippingCount_tail_claim17_7 {horizon : Nat} (hhorizon : 0 < horizon) (delta gap : Real) (hdelta : 0 < delta) (hdelta1 : delta < 1) (hgap_lt : gap < 1 / 8) (horizon_condition : 32 * Real.log (1 / delta) <= horizon) : (adversarialCenteredNoiseLaw horizon (1 / 10)).real {eta | (horizon : Real) / 4 <= adversarialClippingCountReal eta gap} <= delta

The textbook clipping count: a round is counted when at least one arm has reward at a boundary of the unit interval.

noncomputable def adversarialBoundaryClippingCountReal {horizon alternatives : Nat} (eta : Fin horizon -> Real) (gap : Real) (distinguished : Fin alternatives) : Real

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

theorem adversarialBoundaryClippingCountReal_le {horizon alternatives : Nat} (eta : Fin horizon -> Real) (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) : adversarialBoundaryClippingCountReal eta gap distinguished <= adversarialClippingCountReal eta gap

Claim 17.7 for the literal boundary event in the textbook.

theorem adversarialBoundaryClippingCount_tail_claim17_7 {horizon alternatives : Nat} (hhorizon : 0 < horizon) (delta gap : Real) (hdelta : 0 < delta) (hdelta1 : delta < 1) (hgap : 0 <= gap) (hgap_lt : gap < 1 / 8) (distinguished : Fin alternatives) (horizon_condition : 32 * Real.log (1 / delta) <= horizon) : (adversarialCenteredNoiseLaw horizon (1 / 10)).real {eta | (horizon : Real) / 4 <= adversarialBoundaryClippingCountReal eta gap distinguished} <= delta

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

def adversarialComparatorRegret {horizon alternatives : Nat} (reward : Fin horizon -> Fin (alternatives + 1) -> Real) (actions : Fin horizon -> Fin (alternatives + 1)) (comparator : Fin (alternatives + 1)) : Real

Adversarial random regret: the best fixed arm in hindsight minus the reward collected along the realized action path.

noncomputable def adversarialRandomRegret {horizon alternatives : Nat} (reward : Fin horizon -> Fin (alternatives + 1) -> Real) (actions : Fin horizon -> Fin (alternatives + 1)) : Real

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

theorem adversarialComparatorRegret_le_randomRegret {horizon alternatives : Nat} (reward : Fin horizon -> Fin (alternatives + 1) -> Real) (actions : Fin horizon -> Fin (alternatives + 1)) (comparator : Fin (alternatives + 1)) : adversarialComparatorRegret reward actions comparator <= adversarialRandomRegret reward actions

*Equation (17.8), construction level.** For every realized shared-noise path and every action path, regret against the distinguished arm is bounded below by `gap * (n - T_i(n) - C)`, where `C` counts clipping rounds.

theorem adversarialComparatorRegret_ge_eq17_8 {horizon alternatives : Nat} (eta : Fin horizon -> Real) (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) (actions : Fin horizon -> Fin (alternatives + 1)) : gap * ((horizon : Real) - adversarialPullCountReal actions distinguished - adversarialClippingCountReal eta gap) <= adversarialComparatorRegret (adversarialClippedGaussianReward eta gap distinguished) actions distinguished.succ

Eq. (17.8) in the textbook's actual random-regret form.

theorem adversarialRandomRegret_ge_eq17_8 {horizon alternatives : Nat} (eta : Fin horizon -> Real) (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) (actions : Fin horizon -> Fin (alternatives + 1)) : gap * ((horizon : Real) - adversarialPullCountReal actions distinguished - adversarialClippingCountReal eta gap) <= adversarialRandomRegret (adversarialClippedGaussianReward eta gap distinguished) actions

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

private theorem clipUnitReward_eq_self_of_ne_endpoints (x : Real) (h0 : clipUnitReward x ≠ 0) (h1 : clipUnitReward x ≠ 1) : clipUnitReward x = x

Exact Eq. (17.8), with the textbook's actual boundary count.

theorem adversarialRandomRegret_ge_boundary_eq17_8 {horizon alternatives : Nat} (eta : Fin horizon -> Real) (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) (actions : Fin horizon -> Fin (alternatives + 1)) : gap * ((horizon : Real) - adversarialPullCountReal actions distinguished - adversarialBoundaryClippingCountReal eta gap distinguished) <= adversarialRandomRegret (adversarialClippedGaussianReward eta gap distinguished) actions

The shared-noise matrix for every witness, including the base arm.

def adversarialFullClippedReward {horizon m : Nat} (eta : Fin horizon -> Real) (gap : Real) (i : Fin (m + 1)) (t : Fin horizon) (arm : Fin (m + 1)) : Real

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

theorem adversarialFullHardShift_bounds {m : Nat} (gap : Real) (hg : 0 <= gap) (i arm : Fin (m + 1)) : 0 <= adversarialFullHardShift gap i arm ∧ adversarialFullHardShift gap i arm <= 2 * gap

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

theorem adversarialFullHardShift_separation {m : Nat} (gap : Real) (hg : 0 <= gap) (i arm : Fin (m + 1)) (hi : arm ≠ i) : gap <= adversarialFullHardShift gap i i - adversarialFullHardShift gap i arm

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

theorem adversarialFullClippedReward_best {horizon m : Nat} (eta : Fin horizon -> Real) (gap : Real) (hg : 0 <= gap) (i : Fin (m + 1)) (t : Fin horizon) (arm : Fin (m + 1)) : adversarialFullClippedReward eta gap i t arm <= adversarialFullClippedReward eta gap i t i

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

noncomputable def adversarialFullBoundaryCount {horizon m : Nat} (eta : Fin horizon -> Real) (gap : Real) (i : Fin (m + 1)) : Real

Literal boundary-count Eq. (17.8), now also valid for the base witness.

theorem adversarialFullRandomRegret_ge_boundary_eq17_8 {horizon m : Nat} (eta : Fin horizon -> Real) (gap : Real) (hg : 0 <= gap) (i : Fin (m + 1)) (actions : Fin horizon -> Fin (m + 1)) : gap * ((horizon : Real) - (∑ t, if actions t = i then 1 else 0) - adversarialFullBoundaryCount eta gap i) <= adversarialRandomRegret (adversarialFullClippedReward eta gap i) actions

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

theorem adversarialFullBoundaryCount_le {horizon m : Nat} (eta : Fin horizon -> Real) (gap : Real) (hg : 0 <= gap) (i : Fin (m + 1)) : adversarialFullBoundaryCount eta gap i <= adversarialClippingCountReal eta gap

Claim 17.7 for every member of the corrected Claim 17.6 witness family.

theorem adversarialFullBoundaryCount_tail_claim17_7 {horizon m : Nat} (hn : 0 < horizon) (delta gap : Real) (hd : 0 < delta) (hd1 : delta < 1) (hg : 0 <= gap) (hg8 : gap < 1 / 8) (i : Fin (m + 1)) (horizon_condition : 32 * Real.log (1 / delta) <= horizon) : (adversarialCenteredNoiseLaw horizon (1 / 10)).real {eta | (horizon : Real) / 4 <= adversarialFullBoundaryCount eta gap i} <= delta

A deterministic oblivious reward table. Only its finite prefix is used.

abbrev AdversarialRewardTable (K : Nat)

Feedback from a fixed table, with the table retained as a kernel parameter.

noncomputable def adversarialTableInitialFeedback {K : Nat} : Kernel (AdversarialRewardTable K × Fin K) Real

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

noncomputable def adversarialTableNextFeedback {K : Nat} (n : Nat) : Kernel ((AdversarialRewardTable K × History.FinitePairHistory (Fin K) Real n) × Fin K) Real

The original policy observes exactly its action/reward prefix.

noncomputable def adversarialTableStepKernel {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (n : Nat) : Kernel (AdversarialRewardTable K × History.FinitePairHistory (Fin K) Real n) (Fin K × Real)

Conditional history distribution under each fixed oblivious table. This is a measurable kernel, so averaging over random tables is well-defined.

noncomputable def adversarialTableHistoryKernel {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) : (n : Nat) -> Kernel (AdversarialRewardTable K) (History.FinitePairHistory (Fin K) Real n) | 0 => ((Kernel.const (AdversarialRewardTable K) algorithm.initialAction) ⊗ₖ adversarialTableInitialFeedback).map (pairHistoryZeroMeasurableEquiv (Fin K) Real) | n + 1 => ((adversarialTableHistoryKernel algorithm n) ⊗ₖ adversarialTableStepKernel algorithm n).map (pairHistorySuccMeasurableEquiv (Fin K) Real n) instance adversarialTableHistoryKernel_isMarkov {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (n : Nat) : IsMarkovKernel (adversarialTableHistoryKernel algorithm n)

Fixing the table gives exactly the original policy and deterministic feedback.

theorem adversarialTableStepKernel_apply {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (n : Nat) (table : AdversarialRewardTable K) (history : History.FinitePairHistory (Fin K) Real n) : adversarialTableStepKernel algorithm n (table, history) = algorithm.policy n history ⊗ₘ Kernel.deterministic (table (n + 1)) (measurable_of_countable _)

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

theorem adversarialTableHistoryKernel_zero {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (table : AdversarialRewardTable K) : adversarialTableHistoryKernel algorithm 0 table = (algorithm.initialAction ⊗ₘ Kernel.deterministic (table 0) (measurable_of_countable _)).map (pairHistoryZeroMeasurableEquiv (Fin K) Real)

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

theorem adversarialTableHistoryKernel_succ {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (n : Nat) (table : AdversarialRewardTable K) : adversarialTableHistoryKernel algorithm (n + 1) table = ((adversarialTableHistoryKernel algorithm n table) ⊗ₘ Kernel.sectR (adversarialTableStepKernel algorithm n) table).map (pairHistorySuccMeasurableEquiv (Fin K) Real n)

Future reward rows cannot affect an already observed history.

theorem adversarialTableHistoryKernel_prefix_congr {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (n : Nat) (table other : AdversarialRewardTable K) (heq : ∀ t, t <= n -> table t = other t) : adversarialTableHistoryKernel algorithm n table = adversarialTableHistoryKernel algorithm n other

Extend the finite shared-noise matrix by zero rows after its horizon.

def adversarialFullRewardTable {horizon m : Nat} (eta : Fin horizon -> Real) (gap : Real) (i : Fin (m + 1)) : AdversarialRewardTable (m + 1)

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

theorem measurable_adversarialFullRewardTable {horizon m : Nat} (gap : Real) (i : Fin (m + 1)) : Measurable (fun eta : Fin horizon -> Real => adversarialFullRewardTable eta gap i)

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

theorem adversarialFullRewardTable_at {horizon m : Nat} (eta : Fin horizon -> Real) (gap : Real) (i : Fin (m + 1)) (t : Fin horizon) : adversarialFullRewardTable eta gap i t = adversarialFullClippedReward eta gap i t

Conditional policy history kernel parameterized by the finite noise path.

noncomputable def adversarialNoiseHistoryKernel {horizon m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (i : Fin (m + 1)) (n : Nat) : Kernel (Fin horizon -> Real) (History.FinitePairHistory (Fin (m + 1)) Real n)

Shared-noise matrix and the original randomized policy on one joint space.

noncomputable def adversarialNoiseHistoryJoint {horizon m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (sigma gap : Real) (i : Fin (m + 1)) (n : Nat) : Measure ((Fin horizon -> Real) × History.FinitePairHistory (Fin (m + 1)) Real n)

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

theorem adversarialNoiseHistoryJoint_noise_marginal {horizon m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (sigma gap : Real) (i : Fin (m + 1)) (n : Nat) : (adversarialNoiseHistoryJoint (horizon := horizon) algorithm sigma gap i n).fst = adversarialCenteredNoiseLaw horizon sigma

Resampling an unobserved noise coordinate leaves the prefix law unchanged.

theorem adversarialNoiseHistoryKernel_update_future {horizon m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (i : Fin (m + 1)) (n : Nat) (eta : Fin horizon -> Real) (j : Fin horizon) (hj : n < j.val) (x : Real) : adversarialNoiseHistoryKernel algorithm gap i n (Function.update eta j x) = adversarialNoiseHistoryKernel algorithm gap i n eta

Isolate any coordinate of the shared Gaussian noise as a product factor.

theorem adversarialCenteredNoiseLaw_split {N : Nat} (sigma : Real) (j : Fin (N + 1)) : MeasurePreserving (MeasurableEquiv.piFinSuccAbove (fun _ : Fin (N + 1) => Real) j) (adversarialCenteredNoiseLaw (N + 1) sigma) ((gaussianReal 0 ⟨sigma ^ 2, sq_nonneg sigma⟩).prod (adversarialCenteredNoiseLaw N sigma))

In split coordinates, the prefix history law is independent of the future factor.

theorem adversarialNoiseHistoryKernel_split_future {N m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (i : Fin (m + 1)) (n : Nat) (j : Fin (N + 1)) (hj : n < j.val) (rest : Fin N -> Real) (x y : Real) : adversarialNoiseHistoryKernel algorithm gap i n (j.insertNth x rest) = adversarialNoiseHistoryKernel algorithm gap i n (j.insertNth y rest)

Tonelli in the independent-coordinate representation of the hard noise law.

theorem lintegral_adversarialCenteredNoiseLaw_split {N : Nat} (sigma : Real) (j : Fin (N + 1)) (f : (Fin (N + 1) -> Real) -> ENNReal) (hf : Measurable f) : (∫⁻ eta, f eta ∂adversarialCenteredNoiseLaw (N + 1) sigma) = ∫⁻ x, ∫⁻ rest, f (j.insertNth x rest) ∂adversarialCenteredNoiseLaw N sigma ∂gaussianReal 0 ⟨sigma ^ 2, sq_nonneg sigma⟩

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

theorem adversarialCenteredNoiseLaw_full_reward_marginal {horizon m : Nat} (sigma gap : Real) (i : Fin (m + 1)) (t : Fin horizon) (arm : Fin (m + 1)) : (adversarialCenteredNoiseLaw horizon sigma).map (fun eta => adversarialFullClippedReward eta gap i t arm) = adversarialClippedArmLaw sigma (adversarialFullHardShift gap i arm)

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

theorem lintegral_adversarialTableHistoryKernel_zero {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (table : AdversarialRewardTable K) (f : History.FinitePairHistory (Fin K) Real 0 -> ENNReal) (hf : Measurable f) : (∫⁻ h, f h ∂adversarialTableHistoryKernel algorithm 0 table) = ∫⁻ arm, f (pairHistoryZeroMeasurableEquiv (Fin K) Real (arm, table 0 arm)) ∂algorithm.initialAction

The initial matrix mixture has exactly the canonical clipped observation law.

theorem lintegral_adversarialNoiseHistoryKernel_zero {N m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (sigma gap : Real) (i : Fin (m + 1)) (f : History.FinitePairHistory (Fin (m + 1)) Real 0 -> ENNReal) (hf : Measurable f) : (∫⁻ eta, ∫⁻ h, f h ∂adversarialNoiseHistoryKernel (horizon := N + 1) algorithm gap i 0 eta ∂adversarialCenteredNoiseLaw (N + 1) sigma) = ∫⁻ h, f h ∂adversarialClippedHistoryLaw algorithm sigma (adversarialFullHardShift gap i) 0

Initial case of the joint-space history marginal identification.

theorem adversarialNoiseHistoryJoint_history_marginal_zero {N m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (sigma gap : Real) (i : Fin (m + 1)) : (adversarialNoiseHistoryJoint (horizon := N + 1) algorithm sigma gap i 0).snd = adversarialClippedHistoryLaw algorithm sigma (adversarialFullHardShift gap i) 0

Conditional table-history recursion, with deterministic feedback integrated out.

theorem lintegral_adversarialTableHistoryKernel_succ {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (table : AdversarialRewardTable K) (n : Nat) (f : History.FinitePairHistory (Fin K) Real (n + 1) -> ENNReal) (hf : Measurable f) : (∫⁻ h, f h ∂adversarialTableHistoryKernel algorithm (n + 1) table) = ∫⁻ h, ∫⁻ arm, f (pairHistorySuccMeasurableEquiv (Fin K) Real n (h, (arm, table (n + 1) arm))) ∂algorithm.policy n h ∂adversarialTableHistoryKernel algorithm n table

Integrate fresh shared noise against a fixed prefix law and the same policy.

theorem lintegral_adversarialFreshNoise_step {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (n : Nat) (P : Measure (History.FinitePairHistory (Fin K) Real n)) [IsProbabilityMeasure P] (sigma : Real) (shift : Fin K -> Real) (f : History.FinitePairHistory (Fin K) Real n × (Fin K × Real) -> ENNReal) (hf : Measurable f) : (∫⁻ x, ∫⁻ h, ∫⁻ arm, f (h, (arm, clipUnitReward (1 / 2 + x + shift arm))) ∂algorithm.policy n h ∂P ∂gaussianReal 0 ⟨sigma ^ 2, sq_nonneg sigma⟩) = ∫⁻ h, ∫⁻ pair, f (h, pair) ∂Thompson.historyStepKernel algorithm (stationaryBanditHistoryEnvironment (adversarialClippedKernel sigma shift)) n h ∂P

Successor history integration on each fixed remaining-noise slice.

theorem lintegral_adversarialNoiseHistoryKernel_succ_slice {N m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (sigma gap : Real) (i : Fin (m + 1)) (n : Nat) (hn : n + 1 < N + 1) (rest : Fin N -> Real) (f : History.FinitePairHistory (Fin (m + 1)) Real (n + 1) -> ENNReal) (hf : Measurable f) : (∫⁻ x, ∫⁻ h, f h ∂adversarialNoiseHistoryKernel algorithm gap i (n + 1) ((⟨n + 1, hn⟩ : Fin (N + 1)).insertNth x rest) ∂gaussianReal 0 ⟨sigma ^ 2, sq_nonneg sigma⟩) = ∫⁻ h, ∫⁻ pair, f (pairHistorySuccMeasurableEquiv (Fin (m + 1)) Real n (h, pair)) ∂Thompson.historyStepKernel algorithm (stationaryBanditHistoryEnvironment (adversarialClippedKernel sigma (adversarialFullHardShift gap i))) n h ∂adversarialNoiseHistoryKernel algorithm gap i n ((⟨n + 1, hn⟩ : Fin (N + 1)).insertNth 0 rest)

Full-noise successor recursion after integrating the independent next coordinate.

theorem lintegral_adversarialNoiseHistoryKernel_succ {N m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (sigma gap : Real) (i : Fin (m + 1)) (n : Nat) (hn : n + 1 < N + 1) (f : History.FinitePairHistory (Fin (m + 1)) Real (n + 1) -> ENNReal) (hf : Measurable f) : (∫⁻ eta, ∫⁻ h, f h ∂adversarialNoiseHistoryKernel (horizon := N + 1) algorithm gap i (n + 1) eta ∂adversarialCenteredNoiseLaw (N + 1) sigma) = ∫⁻ eta, ∫⁻ h, ∫⁻ pair, f (pairHistorySuccMeasurableEquiv (Fin (m + 1)) Real n (h, pair)) ∂Thompson.historyStepKernel algorithm (stationaryBanditHistoryEnvironment (adversarialClippedKernel sigma (adversarialFullHardShift gap i))) n h ∂adversarialNoiseHistoryKernel algorithm gap i n eta ∂adversarialCenteredNoiseLaw (N + 1) sigma

All observed finite prefixes have the canonical clipped history law.

theorem lintegral_adversarialNoiseHistoryKernel_eq_clipped {N m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (sigma gap : Real) (i : Fin (m + 1)) (n : Nat) (hn : n < N + 1) (f : History.FinitePairHistory (Fin (m + 1)) Real n -> ENNReal) (hf : Measurable f) : (∫⁻ eta, ∫⁻ h, f h ∂adversarialNoiseHistoryKernel (horizon := N + 1) algorithm gap i n eta ∂adversarialCenteredNoiseLaw (N + 1) sigma) = ∫⁻ h, f h ∂adversarialClippedHistoryLaw algorithm sigma (adversarialFullHardShift gap i) n

Full matrix-policy coupling: its history marginal is exactly Claim 17.6's law.

theorem adversarialNoiseHistoryJoint_history_marginal {N m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (sigma gap : Real) (i : Fin (m + 1)) (n : Nat) (hn : n < N + 1) : (adversarialNoiseHistoryJoint (horizon := N + 1) algorithm sigma gap i n).snd = adversarialClippedHistoryLaw algorithm sigma (adversarialFullHardShift gap i) n

Corrected Claim 17.6 on the shared-noise matrix and policy joint space.

theorem adversarialNoiseHistoryJoint_pull_le_half_claim17_6 {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (n : Nat) (sigma delta : Real) (hs : sigma ≠ 0) (hd : 0 < delta) (hd8 : delta < 1 / 8) : ∃ i : Fin (m + 1), 2 * delta <= (adversarialNoiseHistoryJoint (horizon := n + 1) algorithm sigma (adversarialClaim17_6Gap (n + 1) m sigma delta) i n).real {p | finiteHistoryPullCountReal n p.2 i <= ((n + 1 : Nat) : Real) / 2}

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

theorem measurable_adversarialClippingCountReal {horizon : Nat} (gap : Real) : Measurable (fun eta : Fin horizon -> Real => adversarialClippingCountReal eta gap)

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

theorem adversarialNoiseHistoryJoint_clipping_tail {horizon m : Nat} (hn : 0 < horizon) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (delta gap : Real) (hd : 0 < delta) (hd1 : delta < 1) (hg8 : gap < 1 / 8) (i : Fin (m + 1)) (n : Nat) (horizon_condition : 32 * Real.log (1 / delta) <= horizon) : (adversarialNoiseHistoryJoint (horizon := horizon) algorithm (1 / 10) gap i n).real {p | (horizon : Real) / 4 <= adversarialClippingCountReal p.1 gap} <= delta

Pull-small and literally few clipped rounds hold jointly with probability at least delta.

theorem adversarialNoiseHistoryJoint_good_event {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (n : Nat) (delta : Real) (hd : 0 < delta) (hd8 : delta < 1 / 8) (hg8 : adversarialClaim17_6Gap (n + 1) m (1 / 10) delta < 1 / 8) (horizon_condition : 32 * Real.log (1 / delta) <= ((n + 1 : Nat) : Real)) : ∃ i : Fin (m + 1), delta <= (adversarialNoiseHistoryJoint (horizon := n + 1) algorithm (1 / 10) (adversarialClaim17_6Gap (n + 1) m (1 / 10) delta) i n).real {p | finiteHistoryPullCountReal n p.2 i <= ((n + 1 : Nat) : Real) / 2 ∧ adversarialFullBoundaryCount p.1 (adversarialClaim17_6Gap (n + 1) m (1 / 10) delta) i < ((n + 1 : Nat) : Real) / 4}

The realized action path, indexed by the actual number of observations.

def adversarialHistoryActions {K : Nat} (n : Nat) (h : History.FinitePairHistory (Fin K) Real n) : Fin (n + 1) -> Fin K

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

theorem adversarialHistoryActions_pullCountENNReal {K : Nat} (n : Nat) (h : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : finiteHistoryPullCountENNReal n h arm = ∑ t, if adversarialHistoryActions n h t = arm then (1 : ENNReal) else 0

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

theorem adversarialHistoryActions_pullCountReal {K : Nat} (n : Nat) (h : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : finiteHistoryPullCountReal n h arm = ∑ t, if adversarialHistoryActions n h t = arm then (1 : Real) else 0

Eq. (17.8) on the same history coordinates as the joint good event.

theorem adversarialHistory_randomRegret_ge_quarter {m : Nat} (n : Nat) (eta : Fin (n + 1) -> Real) (gap : Real) (hg : 0 <= gap) (i : Fin (m + 1)) (h : History.FinitePairHistory (Fin (m + 1)) Real n) (hp : finiteHistoryPullCountReal n h i <= ((n + 1 : Nat) : Real) / 2) (hc : adversarialFullBoundaryCount eta gap i <= ((n + 1 : Nat) : Real) / 4) : gap * (((n + 1 : Nat) : Real) / 4) <= adversarialRandomRegret (adversarialFullClippedReward eta gap i) (adversarialHistoryActions n h)

Random-regret tail on the coupled hard matrix, before final constant calibration.

theorem adversarialNoiseHistoryJoint_randomRegret_tail {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (n : Nat) (delta : Real) (hd : 0 < delta) (hd8 : delta < 1 / 8) (hg8 : adversarialClaim17_6Gap (n + 1) m (1 / 10) delta < 1 / 8) (horizon_condition : 32 * Real.log (1 / delta) <= ((n + 1 : Nat) : Real)) : ∃ i : Fin (m + 1), delta <= (adversarialNoiseHistoryJoint (horizon := n + 1) algorithm (1 / 10) (adversarialClaim17_6Gap (n + 1) m (1 / 10) delta) i n).real {p | adversarialClaim17_6Gap (n + 1) m (1 / 10) delta * (((n + 1 : Nat) : Real) / 4) <= adversarialRandomRegret (adversarialFullClippedReward p.1 (adversarialClaim17_6Gap (n + 1) m (1 / 10) delta) i) (adversarialHistoryActions n p.2)}

First-moment extraction for a measurable kernel event. Mathlib candidate.

theorem exists_kernel_section_mass_ge {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (μ : Measure X) [IsProbabilityMeasure μ] (κ : Kernel X Y) [IsMarkovKernel κ] (E : Set (X × Y)) (hE : MeasurableSet E) (delta : Real) (hd : delta <= (μ ⊗ₘ κ).real E) : ∃ x, delta <= (κ x).real (Prod.mk x ⁻¹' E)

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

theorem measurable_adversarialRandomRegret {horizon m : Nat} (actions : Fin horizon -> Fin (m + 1)) : Measurable (fun reward : Fin horizon -> Fin (m + 1) -> Real => adversarialRandomRegret reward actions)

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

theorem measurable_adversarialJointRandomRegret {m : Nat} (n : Nat) (gap : Real) (i : Fin (m + 1)) : Measurable (fun p : (Fin (n + 1) -> Real) × History.FinitePairHistory (Fin (m + 1)) Real n => adversarialRandomRegret (adversarialFullClippedReward p.1 gap i) (adversarialHistoryActions n p.2))

A deterministic bounded reward table realizes the uncalibrated random-regret tail.

theorem exists_adversarialTable_randomRegret_tail {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (n : Nat) (delta : Real) (hd : 0 < delta) (hd8 : delta < 1 / 8) (hg8 : adversarialClaim17_6Gap (n + 1) m (1 / 10) delta < 1 / 8) (horizon_condition : 32 * Real.log (1 / delta) <= ((n + 1 : Nat) : Real)) : ∃ table : AdversarialRewardTable (m + 1), (∀ t arm, table t arm ∈ Set.Icc (0 : Real) 1) ∧ delta <= (adversarialTableHistoryKernel algorithm n table).real {h | adversarialClaim17_6Gap (n + 1) m (1 / 10) delta * (((n + 1 : Nat) : Real) / 4) <= adversarialRandomRegret (fun t : Fin (n + 1) => table t.val) (adversarialHistoryActions n h)}

Explicit logarithmic comparison on the corrected confidence domain.

theorem adversarialConfidence_log_calibration (delta : Real) (hd : 0 < delta) (hd32 : delta <= 1 / 32) : 0 < Real.log (1 / (2 * delta)) ∧ Real.log (1 / (2 * delta)) / 2 <= Real.log (1 / (8 * delta)) ∧ Real.log (1 / delta) <= 2 * Real.log (1 / (2 * delta)) ∧ Real.log (1 / (8 * delta)) <= Real.log (1 / (2 * delta))

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

theorem adversarialClaim17_6Gap_tenth_sq {N m : Nat} (hN : 0 < N) (hm : 0 < m) (delta : Real) (hd : 0 < delta) (hd8 : delta < 1 / 8) : (adversarialClaim17_6Gap N m (1 / 10) delta) ^ 2 = (m : Real) * Real.log (1 / (8 * delta)) / (200 * N)

The source clipping and gap conditions follow from a source-form horizon bound.

theorem adversarialHorizon_calibration {N m : Nat} (hN : 0 < N) (hm : 0 < m) (delta : Real) (hd : 0 < delta) (hd32 : delta <= 1 / 32) (horizon : 64 * ((m + 1 : Nat) : Real) * Real.log (1 / (2 * delta)) <= N) : adversarialClaim17_6Gap N m (1 / 10) delta < 1 / 8 ∧ 32 * Real.log (1 / delta) <= N

Strict slack converts the construction's non-strict event to a CDF-complement event.

theorem adversarialThreshold_calibration {N m : Nat} (hN : 0 < N) (hm : 0 < m) (delta : Real) (hd : 0 < delta) (hd32 : delta <= 1 / 32) : adversarialHighProbabilityThreshold N (m + 1) (1 / 160) delta < adversarialClaim17_6Gap N m (1 / 10) delta * ((N : Real) / 4)

*Corrected Theorem 17.4.** Explicit constants and confidence domain; the event is strict random regret, for a deterministic bounded reward table.

theorem exists_adversarialTable_randomRegret_gt_theorem17_4 {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (n : Nat) (delta : Real) (hd : 0 < delta) (hd32 : delta <= 1 / 32) (horizon : 64 * ((m + 1 : Nat) : Real) * Real.log (1 / (2 * delta)) <= ((n + 1 : Nat) : Real)) : ∃ table : AdversarialRewardTable (m + 1), (∀ t arm, table t arm ∈ Set.Icc (0 : Real) 1) ∧ delta <= (adversarialTableHistoryKernel algorithm n table).real {h | adversarialHighProbabilityThreshold (n + 1) (m + 1) (1 / 160) delta < adversarialRandomRegret (fun t : Fin (n + 1) => table t.val) (adversarialHistoryActions n h)}

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

def adversarialTableRandomRegret {m : Nat} (table : AdversarialRewardTable (m + 1)) (n : Nat) (h : History.FinitePairHistory (Fin (m + 1)) Real n) : Real

Deterministic expectation, separate from the pathwise random-regret variable.

noncomputable def adversarialTableExpectedRegret {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (table : AdversarialRewardTable (m + 1)) (n : Nat) : Real

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

noncomputable def adversarialTableCDF {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (table : AdversarialRewardTable (m + 1)) (n : Nat) (u : Real) : Real

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

theorem measurable_adversarialTableRandomRegret {m : Nat} (table : AdversarialRewardTable (m + 1)) (n : Nat) : Measurable (adversarialTableRandomRegret table n)

A fixed finite reward table has only finitely many possible action-path regrets, so its expectation is a genuine integrable random variable.

theorem integrable_adversarialTableRandomRegret {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (table : AdversarialRewardTable (m + 1)) (n : Nat) : Integrable (adversarialTableRandomRegret table n) (adversarialTableHistoryKernel algorithm n table)

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

theorem adversarialTable_strictTail_eq_one_sub_CDF {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (table : AdversarialRewardTable (m + 1)) (n : Nat) (u : Real) : (adversarialTableHistoryKernel algorithm n table).real {h | u < adversarialTableRandomRegret table n h} = 1 - adversarialTableCDF algorithm table n u

Corrected Theorem 17.4 in the source's CDF-complement notation.

theorem adversarialRandomRegret_ge_theorem17_4 {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (n : Nat) (delta : Real) (hd : 0 < delta) (hd32 : delta <= 1 / 32) (horizon : 64 * ((m + 1 : Nat) : Real) * Real.log (1 / (2 * delta)) <= ((n + 1 : Nat) : Real)) : ∃ table : AdversarialRewardTable (m + 1), (∀ t arm, table t arm ∈ Set.Icc (0 : Real) 1) ∧ delta <= 1 - adversarialTableCDF algorithm table n (adversarialHighProbabilityThreshold (n + 1) (m + 1) (1 / 160) delta)