BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoSelectedIID

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

private theorem twoArmHistoryEnvironment_ext (environment₁ environment₂ : Thompson.HistoryEnvironment (Fin 2) Real) (hfeedback : environment₁.feedback = environment₂.feedback) (hinitial : environment₁.initialFeedback = environment₂.initialFeedback) : environment₁ = environment₂

The first `m` optimal-arm pull records on an observable trajectory. The time coordinate is part of the value, so `top` remains visible. The reward coordinate has source semantics only when that time is finite.

def twoArmOptimalPullTimeRewardBlock {Env : Type u} [MeasurableSpace Env] (m : Nat) : Env × ((t : Nat) -> Fin 2 × Real) -> ((i : Fin m) -> WithTop Nat × Real)

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

theorem measurable_twoArmOptimalPullTimeRewardBlock {Env : Type u} [MeasurableSpace Env] (m : Nat) : Measurable (twoArmOptimalPullTimeRewardBlock (Env := Env) m)

The latent comparison block. A finite pull reads its corresponding arm-`0` stream coordinate. A missing pull retains the stopped-value fallback rather than silently turning an absent observation into an IID reward.

def twoArmLatentMaskedOptimalPullBlock (m : Nat) : UCB.ArmRewardStream 2 × ((t : Nat) -> Fin 2 × Real) -> ((i : Fin m) -> WithTop Nat × Real)

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

theorem measurable_twoArmLatentMaskedOptimalPullBlock (m : Nat) : Measurable (twoArmLatentMaskedOptimalPullBlock m)

On the latent coupling, the observable finite pull block agrees almost surely with the missing-pull-aware latent block.

theorem twoArmOptimalPullTimeRewardBlock_eq_latentMasked_ae (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (m : Nat) : (fun sample : UCB.ArmRewardStream 2 × ((t : Nat) -> Fin 2 × Real) => twoArmOptimalPullTimeRewardBlock (Env := Unit) m ((), sample.2)) =ᵐ[ twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta] twoArmLatentMaskedOptimalPullBlock m

Exact finite selected-block law on the native stationary fixed-IID SGB process. The right side is a masked latent-coupling law, not a product law; this retained dependence is what makes the statement valid under adaptive selection and possible missing pulls.

theorem twoArmNativeOptimalPullTimeRewardBlock_map_eq_latentMasked (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (m : Nat) : letI : IsMarkovKernel (UCB.finiteArmRealRewardKernel armLaw)

The source-shaped `Unit`-environment trajectory measure has the same observable marginal as the native stationary history construction.

theorem twoArmFixedIIDTrajectoryMeasure_map_snd_eq_nativeStationary (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) : letI : IsMarkovKernel (UCB.finiteArmRealRewardKernel armLaw)

The latent coupling and the source-generated fixed-IID trajectory have exactly the same visible `Unit`-environment marginal. This is a full trajectory-law transport; it does not identify selected rewards as IID or condition on occurrence of any pull.

theorem twoArmFixedIIDLatentTrajectoryMeasure_map_visible_eq_generated (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) : Measure.map (fun sample : UCB.ArmRewardStream 2 × ((t : Nat) -> Fin 2 × Real) => ((), sample.2)) (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) = twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)

Source-facing finite selected-block transport on the actual generated two-arm trajectory measure. Missing pulls remain visible in the `WithTop` time coordinates; the theorem does not promote the masked block to IID.

theorem twoArmFixedIIDTrajectoryMeasure_map_optimalPullTimeRewardBlock_eq_latentMasked (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (m : Nat) : Measure.map (twoArmOptimalPullTimeRewardBlock (Env := Unit) m) (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) = Measure.map (twoArmLatentMaskedOptimalPullBlock m) (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta)

The running reward sum inside Appendix C's recovery phase. The index `k : Fin (n1 + 1)` permits every prefix length from `0` through `n1`. The ambient reward block contains the unlucky phase of length `n0` followed by the recovery phase of length `n1`.

def twoArmAppendixCPhaseOnePrefixSum (n0 n1 : Nat) (rewardBlock : Fin (n0 + n1) -> Real) (k : Fin (n1 + 1)) : Real

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

theorem measurable_twoArmAppendixCPhaseOnePrefixSum (n0 n1 : Nat) (k : Fin (n1 + 1)) : Measurable (fun rewardBlock : Fin (n0 + n1) -> Real => twoArmAppendixCPhaseOnePrefixSum n0 n1 rewardBlock k)

The exact finite reward event used by the two phases in Appendix C. Phase `S0` consists of `n0` rewards equal to `-1`. Phase `S1` consists only of `{-1, 1}` rewards, has the specified exact terminal sum, and has running sum at most zero at every prefix. The later arithmetic layer will instantiate `phaseOneTotal` with the rounded Rademacher count selected by the source; this definition itself contains no probability or IID premise.

def twoArmAppendixCRewardPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : Set (Fin (n0 + n1) -> Real)

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

theorem measurableSet_twoArmAppendixCRewardPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : MeasurableSet (twoArmAppendixCRewardPhaseEvent n0 n1 phaseOneTotal)

Every requested optimal-arm pull in a finite block has occurred. This set is kept separate from the reward pattern because occurrence depends on the adaptive trajectory.

def twoArmAppendixCAllPullsPresent (m : Nat) : Set ((i : Fin m) -> WithTop Nat × Real)

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

theorem measurableSet_twoArmAppendixCAllPullsPresent (m : Nat) : MeasurableSet (twoArmAppendixCAllPullsPresent m)

Observable Appendix-C phase event on a pull-time/reward block. It requires the full block to occur and only then reads the phase reward pattern.

def twoArmAppendixCObservedPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : Set ((i : Fin (n0 + n1)) -> WithTop Nat × Real)

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

theorem measurableSet_twoArmAppendixCObservedPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : MeasurableSet (twoArmAppendixCObservedPhaseEvent n0 n1 phaseOneTotal)

The latent Appendix-C event without occurrence conditioning. The first conjunct still depends on the generated visible trajectory and says that all requested pulls occur. The second conjunct reads the unconditional latent arm-`0` stream. Keeping both in the same event avoids the invalid step of declaring the reward block IID after conditioning on occurrence.

def twoArmAppendixCLatentPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : Set (UCB.ArmRewardStream 2 × ((t : Nat) -> Fin 2 × Real))

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

theorem measurableSet_twoArmAppendixCLatentPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : MeasurableSet (twoArmAppendixCLatentPhaseEvent n0 n1 phaseOneTotal)

On the all-pulls-present boundary, the masked block reads exactly the latent arm-`0` prefix.

theorem twoArmLatentMaskedOptimalPullBlock_preimage_appendixCObservedPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : (twoArmLatentMaskedOptimalPullBlock (n0 + n1)) ⁻¹' twoArmAppendixCObservedPhaseEvent n0 n1 phaseOneTotal = twoArmAppendixCLatentPhaseEvent n0 n1 phaseOneTotal

Source-shaped generated-process event corresponding to the finite Appendix-C pull-ordered phase.

def twoArmAppendixCGeneratedPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : Set (Unit × ((t : Nat) -> Fin 2 × Real))

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

theorem measurableSet_twoArmAppendixCGeneratedPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : MeasurableSet (twoArmAppendixCGeneratedPhaseEvent n0 n1 phaseOneTotal)

Exact transport of the finite Appendix-C phase event to the source-shaped generated SGB trajectory. The right side is an intersection of the latent reward pattern with the adaptive all-pulls-present event. This theorem does not assert a product law, selected IID, a probability lower bound, future no-return, or Theorem 2.

theorem twoArmFixedIIDTrajectoryMeasure_appendixCGeneratedPhaseEvent_eq_latent (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (n0 n1 : Nat) (phaseOneTotal : Real) : (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmAppendixCGeneratedPhaseEvent n0 n1 phaseOneTotal) = (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) (twoArmAppendixCLatentPhaseEvent n0 n1 phaseOneTotal)

The pure latent Appendix-C reward pattern, before intersecting it with the adaptive event that all requested optimal-arm pulls occur.

def twoArmAppendixCPureLatentRewardEvent (n0 n1 : Nat) (phaseOneTotal : Real) : Set (UCB.ArmRewardStream 2 × ((t : Nat) -> Fin 2 × Real))

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

theorem measurableSet_twoArmAppendixCPureLatentRewardEvent (n0 n1 : Nat) (phaseOneTotal : Real) : MeasurableSet (twoArmAppendixCPureLatentRewardEvent n0 n1 phaseOneTotal)

The pure latent reward pattern together with failure of at least one requested optimal-arm pull to occur. This is the complementary branch to the existing all-present latent phase event, not yet a fixed-cutoff starvation event.

def twoArmAppendixCMissingPullLatentPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : Set (UCB.ArmRewardStream 2 × ((t : Nat) -> Fin 2 × Real))

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

theorem measurableSet_twoArmAppendixCMissingPullLatentPhaseEvent (n0 n1 : Nat) (phaseOneTotal : Real) : MeasurableSet (twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal)

Membership in the missing branch exposes an actual `WithTop.top` pull-time coordinate while retaining the pure latent reward pattern.

theorem mem_twoArmAppendixCMissingPullLatentPhaseEvent_iff (n0 n1 : Nat) (phaseOneTotal : Real) (sample : UCB.ArmRewardStream 2 × ((t : Nat) -> Fin 2 × Real)) : sample ∈ twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal ↔ (fun i : Fin (n0 + n1) => sample.1 (i : Nat) 0) ∈ twoArmAppendixCRewardPhaseEvent n0 n1 phaseOneTotal ∧ ∃ i : Fin (n0 + n1), twoArmNthOptimalPullTime (Env := Unit) (i : Nat) ((), sample.2) = (⊤ : WithTop Nat)

Every missing-pull Appendix-C phase lies in the finite-horizon below-threshold count event, at every chosen finite horizon. This is the deterministic missing-pull-to-starvation bridge; it asserts neither the source trigger inequality nor a probability lower bound.

theorem twoArmAppendixCMissingPullLatentPhaseEvent_subset_terminalCountBelow (n0 n1 : Nat) (phaseOneTotal : Real) (horizon : Nat) : twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal ⊆ (fun sample : UCB.ArmRewardStream 2 × ((t : Nat) -> Fin 2 × Real) => ((), sample.2)) ⁻¹' twoArmOptimalPullCountBelowEvent (Env := Unit) (n0 + n1) horizon

The latent missing-pull phase mass is bounded by the probability of the visible generated trajectory having fewer than the requested block of optimal-arm pulls. The inequality transports existing mass only; it does not prove that the missing branch has positive probability.

theorem twoArmFixedIIDMissingPullLatentPhase_probability_le_countBelow (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (n0 n1 : Nat) (phaseOneTotal : Real) (horizon : Nat) : (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta).real (twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal) ≤ (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)).real (twoArmOptimalPullCountBelowEvent (Env := Unit) (n0 + n1) horizon)

Finite-horizon expected-regret consumer for the latent missing-pull branch. Nonnegative gap times the horizon-minus-block-size charge times the existing missing-branch probability is bounded by expected sampled pseudo-regret on the actual generated trajectory. This theorem supplies no lower bound on that probability and no source trigger, selected-IID, future/no-return, ballot, asymptotic, or Theorem-2 conclusion.

theorem twoArmFixedIIDMissingPullLatentPhase_charge_mul_probability_le_integral (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta Delta : Real) (hDelta : 0 ≤ Delta) (n0 n1 : Nat) (phaseOneTotal : Real) (horizon : Nat) : Delta * ((horizon - (n0 + n1) : Nat) : Real) * (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta).real (twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal) ≤ integral (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmSampledPseudoRegret (Env := Unit) Delta horizon)

The unconditional latent reward event is exactly the union of the all-present phase and the missing-pull phase.

theorem twoArmAppendixCPureLatentRewardEvent_eq_union_phase_missing (n0 n1 : Nat) (phaseOneTotal : Real) : twoArmAppendixCPureLatentRewardEvent n0 n1 phaseOneTotal = twoArmAppendixCLatentPhaseEvent n0 n1 phaseOneTotal ∪ twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal

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

theorem disjoint_twoArmAppendixCLatentPhaseEvent_missing (n0 n1 : Nat) (phaseOneTotal : Real) : Disjoint (twoArmAppendixCLatentPhaseEvent n0 n1 phaseOneTotal) (twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal)

The pure latent phase probability is evaluated under the already compiled finite arm-0 product law.

theorem twoArmFixedIIDLatentTrajectoryMeasure_purePhaseEvent_eq_pi (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (n0 n1 : Nat) (phaseOneTotal : Real) : (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) (twoArmAppendixCPureLatentRewardEvent n0 n1 phaseOneTotal) = (Measure.pi (fun _ : Fin (n0 + n1) => armLaw 0) : Measure (Fin (n0 + n1) -> Real)) (twoArmAppendixCRewardPhaseEvent n0 n1 phaseOneTotal)

Probability additivity for the disjoint all-present and missing-pull branches of the pure latent phase event.

theorem twoArmFixedIIDLatentTrajectoryMeasure_purePhaseEvent_eq_phase_add_missing (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (n0 n1 : Nat) (phaseOneTotal : Real) : (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) (twoArmAppendixCPureLatentRewardEvent n0 n1 phaseOneTotal) = (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) (twoArmAppendixCLatentPhaseEvent n0 n1 phaseOneTotal) + (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) (twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal)

Source-facing missing-pull/all-present dichotomy. The unconditional product-law probability of the pure finite reward phase is the sum of the generated all-present phase probability and the latent missing-pull branch probability. This theorem does not identify the missing branch with a fixed-cutoff starvation event, condition rewards on occurrence, or prove a positive phase bound, future no-return, ballot asymptotics, or Theorem 2.

theorem twoArmAppendixCRewardPhaseProbability_eq_generated_add_missing (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (n0 n1 : Nat) (phaseOneTotal : Real) : (Measure.pi (fun _ : Fin (n0 + n1) => armLaw 0) : Measure (Fin (n0 + n1) -> Real)) (twoArmAppendixCRewardPhaseEvent n0 n1 phaseOneTotal) = (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmAppendixCGeneratedPhaseEvent n0 n1 phaseOneTotal) + (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) (twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal)

A zero-sum two-arm softmax vector reaches the source Step-1 threshold once its exact odds are at most `1 / (2 * T - 1)`. This is the final algebraic implication in Appendix C's deterministic trigger. It does not supply the preceding phase-to-parameter or phase-to-odds bound.

theorem softmaxProbability_zero_le_one_div_two_mul_nat_of_exp_two_mul_le (theta : Fin 2 -> Real) (horizon : Nat) (hhorizon : 1 <= horizon) (hsum : ∑ coordinate, theta coordinate = 0) (hexp : Real.exp (2 * theta 0) <= 1 / (2 * (horizon : Real) - 1)) : softmaxProbability theta 0 <= 1 / (2 * (horizon : Real))

Generated-trajectory specialization of the exact two-arm odds threshold.

theorem twoArmSuccessProbability_le_one_div_two_mul_nat_of_exp_parameter_le {Env : Type v} [MeasurableSpace Env] (eta : Real) (time horizon : Nat) (hhorizon : 1 <= horizon) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (hexp : Real.exp (2 * twoArmTrajectoryParameterZero eta time sample) <= 1 / (2 * (horizon : Real) - 1)) : twoArmSuccessProbability eta time sample <= 1 / (2 * (horizon : Real))

At a finite requested optimal-arm pull, the generated parameter odds cap transfers to the stopped post-pull probability used by Appendix C.

theorem twoArmNthOptimalPullSuccessProbability_le_one_div_two_mul_nat_of_time_eq {Env : Type v} [MeasurableSpace Env] (eta : Real) (pullIndex time horizon : Nat) (hhorizon : 1 <= horizon) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htime : twoArmNthOptimalPullTime pullIndex sample = (time : WithTop Nat)) (hexp : Real.exp (2 * twoArmTrajectoryParameterZero eta time sample) <= 1 / (2 * (horizon : Real) - 1)) : twoArmNthOptimalPullSuccessProbability eta pullIndex sample <= 1 / (2 * (horizon : Real))

The two-arm optimal-arm probability is bounded by the exponential of twice its zero-sum parameter coordinate. This is the deterministic softmax terminal used in Appendix C. It does not derive a parameter bound from the reward phase.

theorem twoArmSuccessProbability_le_exp_two_mul_parameter {Env : Type u} [MeasurableSpace Env] (eta : Real) (n : Nat) (sample : Env × ((t : Nat) -> Fin 2 × Real)) : twoArmSuccessProbability eta n sample <= Real.exp (2 * twoArmTrajectoryParameterZero eta n sample)

A sufficiently negative post-prefix parameter implies the exact `1/(2*T)` optimal-arm probability threshold used by source Lemma 9. The hard phase-recurrence obligation is deliberately a producer for `hparameter`; this theorem only closes the final softmax/exponential step.

theorem twoArmSuccessProbability_le_one_div_two_mul_horizon_of_parameter {Env : Type u} [MeasurableSpace Env] (eta : Real) (n T : Nat) (sample : Env × ((t : Nat) -> Fin 2 × Real)) (hT : 0 < T) (hparameter : 2 * twoArmTrajectoryParameterZero eta n sample <= -Real.log (2 * (T : Real))) : twoArmSuccessProbability eta n sample <= 1 / (2 * (T : Real))

Membership in the generated all-present Appendix-C phase exposes the finite chronological time of its last requested optimal-arm pull. The zero-based pull index is `n0+n1-1`; the conclusion records the exact before/action/after count specification at the same cutoff. This theorem is only the occurrence bridge and makes no probability or recurrence claim.

theorem twoArmAppendixCGeneratedPhaseEvent_exists_lastPullTime (n0 n1 : Nat) (phaseOneTotal : Real) (hpositive : 0 < n0 + n1) (sample : Unit × ((t : Nat) -> Fin 2 × Real)) (hphase : sample ∈ twoArmAppendixCGeneratedPhaseEvent n0 n1 phaseOneTotal) : exists cutoff : Nat, twoArmNthOptimalPullTime (n0 + n1 - 1) sample = (cutoff : WithTop Nat) /\ twoArmOptimalPullCount cutoff sample = n0 + n1 - 1 /\ twoArmGeneratedAction sample cutoff = 0 /\ twoArmOptimalPullCount (cutoff + 1) sample = n0 + n1