BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoStarvation

The action coordinate of the canonical SGB trajectory.

def twoArmGeneratedAction {Env : Type v} (sample : Env × ((k : Nat) → Fin 2 × Real)) : ActionTrace (Fin 2)

Number of optimal-arm (`0`) pulls in the first `horizon` generated rounds.

def twoArmOptimalPullCount {Env : Type v} (horizon : Nat) (sample : Env × ((k : Nat) → Fin 2 × Real)) : Nat

The source Step-1 threshold `1 / (2*T)`.

def twoArmStepOneThreshold (horizon : Nat) : Real

At a chronological prefix ending at `prefix`, the source Step-1 trigger says that the next optimal-arm probability is at most `1/(2*T)` and that exactly `n` optimal-arm pulls have occurred through that prefix. The distinction between chronological `prefix` and pull index `n` is intentional and source-critical.

def twoArmStepOneTriggerEvent {Env : Type v} [MeasurableSpace Env] (eta : Real) (cutoff n horizon : Nat) : Set (Env × ((k : Nat) → Fin 2 × Real))

The measurable part of the Appendix-C Step-1 starvation event: a trigger prefix occurs and the total number of optimal-arm pulls by `horizon` remains exactly `n`. Equality of the two pull counts is the finite-trace statement that there is no later optimal-arm selection.

def twoArmStepOneStarvationEvent {Env : Type v} [MeasurableSpace Env] (eta : Real) (cutoff n horizon : Nat) : Set (Env × ((k : Nat) → Fin 2 × Real))

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

theorem measurable_twoArmGeneratedAction {Env : Type v} [MeasurableSpace Env] (t : Nat) : Measurable (fun sample : Env × ((k : Nat) → Fin 2 × Real) => twoArmGeneratedAction sample t)

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

theorem measurable_twoArmOptimalPullCount {Env : Type v} [MeasurableSpace Env] (horizon : Nat) : Measurable (twoArmOptimalPullCount (Env := Env) horizon)

The exact terminal optimal-arm count fiber at a finite horizon.

def twoArmTerminalOptimalPullCountEvent {Env : Type v} [MeasurableSpace Env] (n horizon : Nat) : Set (Env × ((k : Nat) → Fin 2 × Real))

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

theorem measurableSet_twoArmTerminalOptimalPullCountEvent {Env : Type v} [MeasurableSpace Env] (n horizon : Nat) : MeasurableSet (twoArmTerminalOptimalPullCountEvent (Env := Env) n horizon)

The finite-horizon event that fewer than `m` optimal-arm pulls occurred.

def twoArmOptimalPullCountBelowEvent {Env : Type v} [MeasurableSpace Env] (m horizon : Nat) : Set (Env × ((k : Nat) → Fin 2 × Real))

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

theorem measurableSet_twoArmOptimalPullCountBelowEvent {Env : Type v} [MeasurableSpace Env] (m horizon : Nat) : MeasurableSet (twoArmOptimalPullCountBelowEvent (Env := Env) m horizon)

The below-threshold count event is the finite disjoint-by-value partition into its exact terminal-count fibers.

theorem twoArmOptimalPullCountBelowEvent_eq_iUnion_terminalCount {Env : Type v} [MeasurableSpace Env] (m horizon : Nat) : twoArmOptimalPullCountBelowEvent (Env := Env) m horizon = ⋃ n : Fin m, twoArmTerminalOptimalPullCountEvent (Env := Env) (n : Nat) horizon

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

theorem measurableSet_twoArmStepOneTriggerEvent {Env : Type v} [MeasurableSpace Env] (eta : Real) (cutoff n horizon : Nat) : MeasurableSet (twoArmStepOneTriggerEvent (Env := Env) eta cutoff n horizon)

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

theorem measurableSet_twoArmStepOneStarvationEvent {Env : Type v} [MeasurableSpace Env] (eta : Real) (cutoff n horizon : Nat) : MeasurableSet (twoArmStepOneStarvationEvent (Env := Env) eta cutoff n horizon)

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

private theorem finTwo_eq_zero_or_one (action : Fin 2) : action = 0 ∨ action = 1

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

theorem twoArmSampledPseudoRegret_nonneg {Env : Type v} (Delta : Real) (hDelta : 0 ≤ Delta) (horizon : Nat) (sample : Env × ((k : Nat) → Fin 2 × Real)) : 0 ≤ twoArmSampledPseudoRegret Delta horizon sample

The two-arm sampled pseudo-regret is exactly the gap times arm-`1` pulls.

theorem twoArmSampledPseudoRegret_eq_gap_mul_suboptimalPullCount {Env : Type v} (Delta : Real) (horizon : Nat) (sample : Env × ((k : Nat) → Fin 2 × Real)) : twoArmSampledPseudoRegret Delta horizon sample = Delta * (pullCount (twoArmGeneratedAction sample) 1 horizon : Real)

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

theorem twoArmOptimalPullCount_add_suboptimalPullCount_eq_horizon {Env : Type v} (horizon : Nat) (sample : Env × ((k : Nat) → Fin 2 × Real)) : twoArmOptimalPullCount horizon sample + pullCount (twoArmGeneratedAction sample) 1 horizon = horizon

Exactly `n` optimal pulls force the exact source starvation charge.

theorem twoArmSampledPseudoRegret_eq_gap_mul_horizon_sub_of_optimalPullCount_eq {Env : Type v} (Delta : Real) (n horizon : Nat) (sample : Env × ((k : Nat) → Fin 2 × Real)) (hcount : twoArmOptimalPullCount horizon sample = n) : twoArmSampledPseudoRegret Delta horizon sample = Delta * ((horizon - n : Nat) : Real)

On one terminal-count fiber, sampled pseudo-regret has the exact charge used by the Appendix-C starvation consumer.

theorem twoArmTerminalOptimalPullCountEvent_sampledPseudoRegret_eq {Env : Type v} [MeasurableSpace Env] (Delta : Real) (n horizon : Nat) (sample : Env × ((k : Nat) → Fin 2 × Real)) (hcount : sample ∈ twoArmTerminalOptimalPullCountEvent (Env := Env) n horizon) : twoArmSampledPseudoRegret Delta horizon sample = Delta * ((horizon - n : Nat) : Real)

The explicit chronological no-return premise constructs membership in the measurable starvation event. This is the pathwise half of Appendix-C Step 1; it does not assign a probability to the event.

theorem mem_twoArmStepOneStarvationEvent_of_lowProbability_noFurtherOptimalPull {Env : Type v} [MeasurableSpace Env] (eta : Real) (cutoff n horizon : Nat) (sample : Env × ((k : Nat) → Fin 2 × Real)) (hcutoff : cutoff + 1 ≤ horizon) (hlow : twoArmSuccessProbability eta cutoff sample ≤ twoArmStepOneThreshold horizon) (hcount : twoArmOptimalPullCount (cutoff + 1) sample = n) (hnoFurther : ∀ t, cutoff + 1 ≤ t → t < horizon → twoArmGeneratedAction sample t ≠ 0) : sample ∈ twoArmStepOneStarvationEvent (Env := Env) eta cutoff n horizon

Every path in the measurable starvation event has the exact Step-1 charge.

theorem twoArmStepOneStarvationEvent_sampledPseudoRegret_eq {Env : Type v} [MeasurableSpace Env] (eta Delta : Real) (cutoff n horizon : Nat) (sample : Env × ((k : Nat) → Fin 2 × Real)) (hstarve : sample ∈ twoArmStepOneStarvationEvent (Env := Env) eta cutoff n horizon) : twoArmSampledPseudoRegret Delta horizon sample = Delta * ((horizon - n : Nat) : Real)

Integrability of finite-horizon sampled regret under any finite trace law.

theorem integrable_twoArmSampledPseudoRegret_of_finiteMeasure {Env : Type v} [MeasurableSpace Env] (mu : Measure (Env × ((k : Nat) → Fin 2 × Real))) [IsFiniteMeasure mu] (Delta : Real) (horizon : Nat) : Integrable (twoArmSampledPseudoRegret (Env := Env) Delta horizon) mu

Fewer than `m` optimal-arm pulls at `horizon` force at least the uniform `Delta * (horizon - m)` sampled-pseudo-regret charge. This is the finite-horizon consumer for a below-count event; it does not provide any positive-mass lower bound for that event. The measure need only be finite; probability and expectation terminology is reserved for probability-measure wrappers such as the fixed-IID consumer below.

theorem twoArmOptimalPullCountBelowEvent_charge_mul_probability_le_integral {Env : Type v} [MeasurableSpace Env] (mu : Measure (Env × ((k : Nat) → Fin 2 × Real))) [IsFiniteMeasure mu] (Delta : Real) (hDelta : 0 ≤ Delta) (m horizon : Nat) : Delta * ((horizon - m : Nat) : Real) * mu.real (twoArmOptimalPullCountBelowEvent (Env := Env) m horizon) ≤ integral mu (twoArmSampledPseudoRegret (Env := Env) Delta horizon)

Expectation-level deterministic Step-1 consumer. It lower-bounds expected sampled regret by the exact starvation charge times the probability of the actual generated starvation event. The missing source producer is precisely the separate lower bound on this event probability from the trigger event.

theorem twoArmStepOneStarvationEvent_charge_mul_probability_le_integral {Env : Type v} [MeasurableSpace Env] (mu : Measure (Env × ((k : Nat) → Fin 2 × Real))) [IsFiniteMeasure mu] (eta Delta : Real) (hDelta : 0 ≤ Delta) (cutoff n horizon : Nat) : Delta * ((horizon - n : Nat) : Real) * mu.real (twoArmStepOneStarvationEvent (Env := Env) eta cutoff n horizon) ≤ integral mu (twoArmSampledPseudoRegret (Env := Env) Delta horizon)

The same deterministic Step-1 consumer specialized to the canonical generated fixed-IID trajectory with a Dirac environment prior. This wrapper covers the paper's Rademacher/Dirac arm-law instance once that explicit arm-law adapter is supplied; it still does not lower-bound the starvation-event probability.

theorem twoArmFixedIIDStepOneStarvationEvent_charge_mul_probability_le_integral (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta Delta : Real) (hDelta : 0 <= Delta) (cutoff n horizon : Nat) : Delta * ((horizon - n : Nat) : Real) * (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)).real (twoArmStepOneStarvationEvent (Env := Unit) eta cutoff n horizon) <= integral (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmSampledPseudoRegret (Env := Unit) Delta horizon)