BanditRLProof.Algorithms.StochasticGradientBanditTwoArmRate

Algorithm 1 preserves the sum of an arbitrary initial parameter vector on every inclusive finite action/reward history.

theorem historyParameter_sum_eq_initial {Action : Type u} [Fintype Action] [DecidableEq Action] [Nonempty Action] (initialTheta : Action -> Real) (eta : Real) : forall n (history : History.FinitePairHistory Action Real n), (∑ coordinate, historyParameter initialTheta eta n history coordinate) = ∑ coordinate, initialTheta coordinate

The source initialization `theta = 0` therefore stays zero-sum pathwise.

theorem historyParameter_zeroInitialization_sum {Action : Type u} [Fintype Action] [DecidableEq Action] [Nonempty Action] (eta : Real) (n : Nat) (history : History.FinitePairHistory Action Real n) : ∑ coordinate, historyParameter (fun _ : Action => 0) eta n history coordinate = 0

Source-time parameter adapter for one infinite two-arm action/reward trace. Lean time `0` is the pre-action source parameter `theta_{.,1} = 0`; Lean time `n + 1` is the parameter after consuming trace pair `n`, namely source `theta_{.,n+2}`.

noncomputable def twoArmParameterAt (eta : Real) (trace : Nat -> Fin 2 × Real) : Nat -> Fin 2 -> Real | 0 => fun _ => 0 | n + 1 => historyParameter (fun _ : Fin 2 => 0) eta n (Preorder.frestrictLe n trace) /-- The two-arm softmax law generated from the source-time parameter adapter. -/ def twoArmProbabilityAt (eta : Real) (trace : Nat -> Fin 2 × Real) (time : Nat) : Fin 2 -> Real

The two-arm softmax law generated from the source-time parameter adapter.

def twoArmProbabilityAt (eta : Real) (trace : Nat -> Fin 2 × Real) (time : Nat) : Fin 2 -> Real

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

theorem twoArmParameterAt_zero (eta : Real) (trace : Nat -> Fin 2 × Real) (arm : Fin 2) : twoArmParameterAt eta trace 0 arm = 0

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

theorem twoArmParameterAt_succ (eta : Real) (trace : Nat -> Fin 2 × Real) (n : Nat) (arm : Fin 2) : twoArmParameterAt eta trace (n + 1) arm = historyParameter (fun _ : Fin 2 => 0) eta n (Preorder.frestrictLe n trace) arm

The source-time two-arm parameter stays zero-sum on every path.

theorem twoArmParameterAt_sum_eq_zero (eta : Real) (trace : Nat -> Fin 2 × Real) (time : Nat) : ∑ arm, twoArmParameterAt eta trace time arm = 0

Hence source arm `2` has the negative parameter of source arm `1`.

theorem twoArmParameterAt_one_eq_neg_zero (eta : Real) (trace : Nat -> Fin 2 × Real) (time : Nat) : twoArmParameterAt eta trace time 1 = -twoArmParameterAt eta trace time 0

Algorithm 1's zero initialization gives the uniform two-arm law before the first action.

theorem twoArmProbabilityAt_zero (eta : Real) (trace : Nat -> Fin 2 × Real) (arm : Fin 2) : twoArmProbabilityAt eta trace 0 arm = 1 / 2

On two arms, normalization identifies the second softmax probability with the failure probability of the first arm.

theorem softmaxProbability_one_eq_one_sub_zero (theta : Fin 2 -> Real) : softmaxProbability theta 1 = 1 - softmaxProbability theta 0

The exact two-arm softmax odds before using the zero-sum invariant.

theorem softmaxProbability_zero_div_one (theta : Fin 2 -> Real) : softmaxProbability theta 0 / softmaxProbability theta 1 = Real.exp (theta 0 - theta 1)

A zero-sum two-arm parameter has opposite coordinates.

theorem finTwo_one_eq_neg_zero_of_sum_eq_zero (theta : Fin 2 -> Real) (hsum : ∑ coordinate, theta coordinate = 0) : theta 1 = -theta 0

The printed division form of Equation (11). Lean arm `0` is source arm `1`, and strict softmax positivity makes the denominator nonzero.

theorem softmaxProbability_zero_div_one_sub_zero_eq_exp_two_mul (theta : Fin 2 -> Real) (hsum : ∑ coordinate, theta coordinate = 0) : softmaxProbability theta 0 / (1 - softmaxProbability theta 0) = Real.exp (2 * theta 0)

The multiplication form of Equation (11) used in the source Theorem 1 proof: `exp(2 theta_1) (1 - p_1) = p_1`. Lean arm `0` is source arm `1`.

theorem exp_two_mul_zero_mul_one_sub_softmaxProbability_zero (theta : Fin 2 -> Real) (hsum : ∑ coordinate, theta coordinate = 0) : Real.exp (2 * theta 0) * (1 - softmaxProbability theta 0) = softmaxProbability theta 0

The inverse-odds form used for the failure-mass telescoping potential in the second half of the source Theorem 1 proof.

theorem exp_neg_two_mul_zero_mul_softmaxProbability_zero (theta : Fin 2 -> Real) (hsum : ∑ coordinate, theta coordinate = 0) : Real.exp (-2 * theta 0) * softmaxProbability theta 0 = 1 - softmaxProbability theta 0

Source-time Equation (11) on every infinite action/reward trace.

theorem twoArmProbabilityAt_exp_two_mul_failure_eq_success (eta : Real) (trace : Nat -> Fin 2 × Real) (time : Nat) : Real.exp (2 * twoArmParameterAt eta trace time 0) * (1 - twoArmProbabilityAt eta trace time 0) = twoArmProbabilityAt eta trace time 0

The printed Equation (11) on the explicitly fenced source-time trace.

theorem twoArmProbabilityAt_zero_div_failure_eq_exp_two_mul (eta : Real) (trace : Nat -> Fin 2 × Real) (time : Nat) : twoArmProbabilityAt eta trace time 0 / (1 - twoArmProbabilityAt eta trace time 0) = Real.exp (2 * twoArmParameterAt eta trace time 0)

Finite-history multiplication form of Equation (11) under Algorithm 1's source initialization.

theorem historyParameter_exp_two_mul_zero_eq_odds (eta : Real) (n : Nat) (history : History.FinitePairHistory (Fin 2) Real n) : Real.exp (2 * historyParameter (fun _ : Fin 2 => 0) eta n history 0) * (1 - softmaxProbability (historyParameter (fun _ : Fin 2 => 0) eta n history) 0) = softmaxProbability (historyParameter (fun _ : Fin 2 => 0) eta n history) 0