BanditRLProof.Algorithms.StochasticGradientBanditCorollaryOne

Every realized two-arm gap is at most `Delta` when `Delta` is nonnegative.

theorem twoArmActionGap_le_gap (Delta : Real) (hDelta : 0 <= Delta) (action : Fin 2) : twoArmActionGap Delta action <= Delta

Pathwise trivial regret bound for the actions actually sampled by the generated process.

theorem twoArmSampledPseudoRegret_le_gap_mul_horizon {Env : Type v} (Delta : Real) (hDelta : 0 <= Delta) (horizon : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) : twoArmSampledPseudoRegret Delta horizon sample <= Delta * (horizon : Real)

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

theorem measurable_twoArmSampledPseudoRegret {Env : Type v} [MeasurableSpace Env] (Delta : Real) (horizon : Nat) : Measurable (twoArmSampledPseudoRegret (Env := Env) Delta horizon)

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

theorem integrable_twoArmSampledPseudoRegret {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

Integral form of the pathwise `Delta * T` bound. The measure is the actual generated trajectory measure in the Corollary-1 consumer below.

theorem integral_twoArmSampledPseudoRegret_le_gap_mul_horizon {Env : Type v} [MeasurableSpace Env] (mu : Measure (Env × ((k : Nat) -> Fin 2 × Real))) [IsProbabilityMeasure mu] (Delta : Real) (hDelta : 0 <= Delta) (horizon : Nat) : integral mu (twoArmSampledPseudoRegret (Env := Env) Delta horizon) <= Delta * (horizon : Real)

The horizon-indexed fixed learning rate used in Corollary 1.

noncomputable def corollaryOneEta (horizon : Nat) : Real

The source small-learning-rate branch implies the strict Theorem-1 margin.

theorem sourceTheoremOne_margin_of_two_mul_eta_sourceC_le (eta Delta : Real) (heta : 0 < eta) (hDelta : 0 < Delta) (hsmall : 2 * eta * sourceC eta <= Delta) : eta * sourceC eta < Delta

Under the Corollary-1 small-learning-rate branch, the constant term in Theorem 1 is at most `1 / eta`.

theorem sourceTheoremOne_constant_le_inv_eta (eta Delta : Real) (heta : 0 < eta) (hDelta : 0 < Delta) (hsmall : 2 * eta * sourceC eta <= Delta) : Delta / (2 * eta * (Delta - eta * sourceC eta)) <= 1 / eta

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

theorem corollaryOneEta_pos (horizon : Nat) (hhorizon : 2 <= horizon) : 0 < corollaryOneEta horizon

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

theorem corollaryOneEta_sq (horizon : Nat) (hhorizon : 2 <= horizon) : corollaryOneEta horizon ^ 2 = Real.log (horizon : Real) / (horizon : Real)

The Corollary-1 learning rate stays in the range where `C_eta <= exp 2` is available.

theorem corollaryOneEta_le_one (horizon : Nat) (hhorizon : 2 <= horizon) : corollaryOneEta horizon <= 1

The square-root rate appearing in the explicit Corollary-1 endpoint.

noncomputable def corollaryOneRate (horizon : Nat) : Real

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

theorem corollaryOneRate_nonneg (horizon : Nat) : 0 <= corollaryOneRate horizon

The horizon-indexed learning rate times the horizon is exactly the square-root rate.

theorem corollaryOneEta_mul_horizon_eq_rate (horizon : Nat) (hhorizon : 2 <= horizon) : corollaryOneEta horizon * (horizon : Real) = corollaryOneRate horizon

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

theorem corollaryOneEta_mul_rate_eq_log (horizon : Nat) (hhorizon : 2 <= horizon) : corollaryOneEta horizon * corollaryOneRate horizon = Real.log (horizon : Real)

The inverse learning-rate term is an absolute-constant multiple of the square-root rate. We keep the exact constant `1 / log 2`, avoiding a hidden asymptotic threshold.

theorem corollaryOne_inv_eta_le_inv_log_two_mul_rate (horizon : Nat) (hhorizon : 2 <= horizon) : 1 / corollaryOneEta horizon <= (1 / Real.log 2) * corollaryOneRate horizon

For `T >= 2`, `0 < Delta < 1`, and the Corollary-1 learning rate, the argument of the Theorem-1 logarithm is at most `T^4`.

theorem corollaryOne_log_argument_le_horizon_pow_four (horizon : Nat) (hhorizon : 2 <= horizon) (Delta : Real) (hDelta : 0 < Delta) (hDelta_lt_one : Delta < 1) : 1 + 4 * corollaryOneEta horizon * Delta * (horizon : Real) <= (horizon : Real) ^ 4

The logarithmic term in the Theorem-1 branch is at most twice the square-root rate.

theorem corollaryOne_log_term_le_two_mul_rate (horizon : Nat) (hhorizon : 2 <= horizon) (Delta : Real) (hDelta : 0 < Delta) (hDelta_lt_one : Delta < 1) : Real.log (1 + 4 * corollaryOneEta horizon * Delta * (horizon : Real)) / (2 * corollaryOneEta horizon) <= 2 * corollaryOneRate horizon

On the complementary branch, the pathwise `Delta * T` bound is still a square-root rate because failure of `2 * eta * C_eta <= Delta` forces the gap below the learning-rate scale.

theorem corollaryOne_gap_mul_horizon_le_exp_constant_mul_rate (horizon : Nat) (hhorizon : 2 <= horizon) (Delta : Real) (hlarge : ¬ 2 * corollaryOneEta horizon * sourceC (corollaryOneEta horizon) <= Delta) : Delta * (horizon : Real) <= (2 * Real.exp 2) * corollaryOneRate horizon

An explicit horizon-independent constant for the finite Corollary-1 endpoint.

noncomputable def corollaryOneAbsoluteConstant : Real

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

theorem corollaryOne_piecewise_bound (horizon : Nat) (hhorizon : 2 <= horizon) (Delta : Real) (hDelta : 0 < Delta) (hDelta_lt_one : Delta < 1) : (if 2 * corollaryOneEta horizon * sourceC (corollaryOneEta horizon) <= Delta then Real.log (1 + 4 * corollaryOneEta horizon * Delta * (horizon : Real)) / (2 * corollaryOneEta horizon) + 1 / corollaryOneEta horizon else Delta * (horizon : Real)) <= corollaryOneAbsoluteConstant * corollaryOneRate horizon

Exact finite two-branch version of source Corollary 1. A separate fixed rate is used for each source horizon `T = tailHorizon + 1`.

theorem twoArmFixedIIDDirac_corollaryOne_piecewise (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (mean : Fin 2 -> Real) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, |reward| <= 1) (hmean : forall arm, integral (armLaw arm) id = mean arm) (Delta : Real) (hDelta : 0 < Delta) (hDelta_lt_one : Delta < 1) (hgap : mean 0 - mean 1 = Delta) (tailHorizon : Nat) (horizon_ge_two : 1 <= tailHorizon) : let eta := corollaryOneEta (tailHorizon + 1) integral (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmSampledPseudoRegret (Env := Unit) Delta (tailHorizon + 1)) <= if 2 * eta * sourceC eta <= Delta then Real.log (1 + 4 * eta * Delta * ((tailHorizon + 1 : Nat) : Real)) / (2 * eta) + 1 / eta else Delta * ((tailHorizon + 1 : Nat) : Real)

Source Corollary 1 on the generated two-arm fixed-IID trajectory, with an explicit absolute constant and no asymptotic notation. The learning rate is fixed within each horizon and may vary across the horizon-indexed family.

theorem twoArmFixedIIDDirac_corollaryOne (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (mean : Fin 2 -> Real) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, |reward| <= 1) (hmean : forall arm, integral (armLaw arm) id = mean arm) (Delta : Real) (hDelta : 0 < Delta) (hDelta_lt_one : Delta < 1) (hgap : mean 0 - mean 1 = Delta) (tailHorizon : Nat) (horizon_ge_two : 1 <= tailHorizon) : let eta := corollaryOneEta (tailHorizon + 1) integral (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmSampledPseudoRegret (Env := Unit) Delta (tailHorizon + 1)) <= corollaryOneAbsoluteConstant * corollaryOneRate (tailHorizon + 1)