BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoNthPull

Complete an inclusive finite prefix to an action trace, using arm `0` outside the prefix. Only coordinates through `prefix` are consumed below.

def twoArmPrefixGeneratedAction {Env : Type v} (chron : Nat) (context : Env × History.FinitePairHistory (Fin 2) Real chron) : ActionTrace (Fin 2)

Optimal-arm pulls visible in an inclusive finite prefix.

def twoArmPrefixOptimalPullCount {Env : Type v} (chron : Nat) (context : Env × History.FinitePairHistory (Fin 2) Real chron) : Nat

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

theorem measurable_twoArmPrefixGeneratedAction {Env : Type v} [MeasurableSpace Env] (chron t : Nat) : Measurable (fun context : Env × History.FinitePairHistory (Fin 2) Real chron => twoArmPrefixGeneratedAction chron context t)

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

theorem measurable_twoArmPrefixOptimalPullCount {Env : Type v} [MeasurableSpace Env] (chron : Nat) : Measurable (twoArmPrefixOptimalPullCount (Env := Env) chron)

The finite-prefix count is exactly the chronological count on the ambient trajectory.

@[simp] theorem twoArmPrefixOptimalPullCount_environmentPrefix_eq {Env : Type v} [MeasurableSpace Env] (chron : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) : twoArmPrefixOptimalPullCount chron (twoArmEnvironmentPrefix chron sample) = twoArmOptimalPullCount (chron + 1) sample

Inclusive optimal-arm pull count as a chronological stochastic process.

def twoArmInclusiveOptimalPullCountProcess {Env : Type v} [MeasurableSpace Env] (chron : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) : Nat

The inclusive count process is adapted to the canonical environment and generated-prefix filtration.

theorem adapted_twoArmInclusiveOptimalPullCountProcess {Env : Type v} [MeasurableSpace Env] : Adapted (twoArmPrefixFiltration (Env := Env)) (twoArmInclusiveOptimalPullCountProcess (Env := Env))

Zero-based time of the requested optimal-arm pull. The value is `top` when that pull never occurs.

def twoArmNthOptimalPullTime {Env : Type v} [MeasurableSpace Env] (pullIndex : Nat) : Env × ((k : Nat) -> Fin 2 × Real) -> WithTop Nat

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

theorem isStoppingTime_twoArmNthOptimalPullTime {Env : Type v} [MeasurableSpace Env] (pullIndex : Nat) : IsStoppingTime (twoArmPrefixFiltration (Env := Env)) (twoArmNthOptimalPullTime (Env := Env) pullIndex)

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

theorem measurable_twoArmNthOptimalPullTime {Env : Type v} [MeasurableSpace Env] (pullIndex : Nat) : Measurable (twoArmNthOptimalPullTime (Env := Env) pullIndex)

`top` is precisely the explicit not-yet-pulled case.

theorem twoArmNthOptimalPullTime_eq_top_iff {Env : Type v} [MeasurableSpace Env] (pullIndex : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) : twoArmNthOptimalPullTime pullIndex sample = (⊤ : WithTop Nat) <-> forall chron : Nat, twoArmOptimalPullCount (chron + 1) sample ≠ pullIndex + 1

A missing zero-based requested pull keeps every finite-horizon count below the corresponding positive count level.

theorem twoArmOptimalPullCount_lt_succ_of_nthOptimalPullTime_eq_top {Env : Type v} [MeasurableSpace Env] (pullIndex horizon : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htop : twoArmNthOptimalPullTime pullIndex sample = (⊤ : WithTop Nat)) : twoArmOptimalPullCount horizon sample < pullIndex + 1

If one of the first `m` requested optimal-arm pulls is missing, every finite-horizon optimal-arm count is strictly below `m`.

theorem twoArmOptimalPullCount_lt_of_fin_nthOptimalPullTime_eq_top {Env : Type v} [MeasurableSpace Env] (m horizon : Nat) (i : Fin m) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htop : twoArmNthOptimalPullTime (i : Nat) sample = (⊤ : WithTop Nat)) : twoArmOptimalPullCount horizon sample < m

At every finite nth-pull time, the inclusive count hits its target.

theorem twoArmNthOptimalPullTime_count_succ_eq {Env : Type v} [MeasurableSpace Env] (pullIndex : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (hfinite : twoArmNthOptimalPullTime pullIndex sample ≠ (⊤ : WithTop Nat)) : twoArmOptimalPullCount ((twoArmNthOptimalPullTime pullIndex sample).untopA + 1) sample = pullIndex + 1

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

theorem twoArmNthOptimalPullTime_count_succ_eq_of_eq {Env : Type v} [MeasurableSpace Env] (pullIndex t : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htime : twoArmNthOptimalPullTime pullIndex sample = (t : WithTop Nat)) : twoArmOptimalPullCount (t + 1) sample = pullIndex + 1

A finite nth-pull time is a genuine selection of the optimal arm.

theorem twoArmNthOptimalPullTime_action_eq_zero {Env : Type v} [MeasurableSpace Env] (pullIndex t : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htime : twoArmNthOptimalPullTime pullIndex sample = (t : WithTop Nat)) : twoArmGeneratedAction sample t = 0

Immediately before the finite nth-pull time there are exactly `pullIndex` optimal pulls.

theorem twoArmNthOptimalPullTime_count_eq {Env : Type v} [MeasurableSpace Env] (pullIndex t : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htime : twoArmNthOptimalPullTime pullIndex sample = (t : WithTop Nat)) : twoArmOptimalPullCount t sample = pullIndex

The complete deterministic chronological-to-pull-index bridge.

theorem twoArmNthOptimalPullTime_spec {Env : Type v} [MeasurableSpace Env] (pullIndex t : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htime : twoArmNthOptimalPullTime pullIndex sample = (t : WithTop Nat)) : twoArmOptimalPullCount t sample = pullIndex /\ twoArmGeneratedAction sample t = 0 /\ twoArmOptimalPullCount (t + 1) sample = pullIndex + 1

Reward observed at the requested optimal-arm pull. The value at `top` is Mathlib's totalized stopped-value default and is never used without a finite time witness.

def twoArmNthOptimalPullReward {Env : Type v} [MeasurableSpace Env] (pullIndex : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) : Real

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

theorem adapted_twoArmGeneratedReward {Env : Type v} [MeasurableSpace Env] : Adapted (twoArmPrefixFiltration (Env := Env)) (fun (t : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) => (sample.2 t).2)

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

theorem measurable_twoArmNthOptimalPullReward {Env : Type v} [MeasurableSpace Env] (pullIndex : Nat) : Measurable (twoArmNthOptimalPullReward (Env := Env) pullIndex)

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

@[simp] theorem twoArmNthOptimalPullReward_eq_of_time_eq {Env : Type v} [MeasurableSpace Env] (pullIndex t : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htime : twoArmNthOptimalPullTime pullIndex sample = (t : WithTop Nat)) : twoArmNthOptimalPullReward pullIndex sample = (sample.2 t).2

Post-pull optimal-arm probability at the requested optimal-arm pull.

def twoArmNthOptimalPullSuccessProbability {Env : Type v} [MeasurableSpace Env] (eta : Real) (pullIndex : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) : Real

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

theorem adapted_twoArmSuccessProbability {Env : Type v} [MeasurableSpace Env] (eta : Real) : Adapted (twoArmPrefixFiltration (Env := Env)) (twoArmSuccessProbability (Env := Env) eta)

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

theorem measurable_twoArmNthOptimalPullSuccessProbability {Env : Type v} [MeasurableSpace Env] (eta : Real) (pullIndex : Nat) : Measurable (twoArmNthOptimalPullSuccessProbability (Env := Env) eta pullIndex)

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

@[simp] theorem twoArmNthOptimalPullSuccessProbability_eq_of_time_eq {Env : Type v} [MeasurableSpace Env] (eta : Real) (pullIndex t : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htime : twoArmNthOptimalPullTime pullIndex sample = (t : WithTop Nat)) : twoArmNthOptimalPullSuccessProbability eta pullIndex sample = twoArmSuccessProbability eta t sample