BanditRLProof.Algorithms.StochasticGradientBanditTheoremFourContractAudit

The positive scalar margin used in Appendix E after Equation (22).

def theoremFourStepOneMargin (K : Nat) (eta Delta : Real) : Real

The unconditional survival mass required by the audited Step-4 event composition.

def theoremFourStepFourSurvivalLowerBound (pPrime c : Real) : Real

The source learning-rate condition implies that the Equation-(22) drift margin is strictly positive.

theorem theoremFourStepOneMargin_pos (K : Nat) (eta Delta : Real) (hmargin : eta * sourceC eta < 2 * Delta / ((K : Real) + 2)) : 0 < theoremFourStepOneMargin K eta Delta

If `pPrime > 0` and `c < 1/2`, the audited Step-4 survival lower bound is positive.

theorem theoremFourStepFourSurvivalLowerBound_pos (pPrime c : Real) (hpPrime : 0 < pPrime) (hc_half : c < 1 / 2) : 0 < theoremFourStepFourSurvivalLowerBound pPrime c

Finite total-probability contract for Appendix E, Step 4. `bufferedMass` represents the probability of entering the strict buffer `q_{s+1} < c`; `jointSurvivalMass` represents the probability of both entering that buffer and not returning before the audited finite horizon. The two middle hypotheses are the multiplication-free form of `P(buffer) >= pPrime` and `P(survival | buffer) >= 1 - 2*c`.

theorem theoremFourStepFour_survivalMass_ge (pPrime c bufferedMass jointSurvivalMass survivalMass : Real) (hc_half : c < 1 / 2) (hbuffer : pPrime <= bufferedMass) (hconditional : (1 - 2 * c) * bufferedMass <= jointSurvivalMass) (hsubset : jointSurvivalMass <= survivalMass) : theoremFourStepFourSurvivalLowerBound pPrime c <= survivalMass

The audited finite event contract yields a strictly positive survival mass when its buffered event has positive mass.

theorem theoremFourStepFour_survivalMass_pos (pPrime c bufferedMass jointSurvivalMass survivalMass : Real) (hpPrime : 0 < pPrime) (hc_half : c < 1 / 2) (hbuffer : pPrime <= bufferedMass) (hconditional : (1 - 2 * c) * bufferedMass <= jointSurvivalMass) (hsubset : jointSurvivalMass <= survivalMass) : 0 < survivalMass

For `0 < rho <= 1`, the finite geometric phase envelope is at most `1 / rho`. This is the finite statement needed before any infinite expected-phase claim.

theorem theoremFourFiniteGeometricPhaseMass_le_inv (rho : Real) (hrho_pos : 0 < rho) (hrho_le_one : rho <= 1) (phaseCount : Nat) : (Finset.range phaseCount).sum (fun phase => (1 - rho) ^ phase) <= 1 / rho

Any finite transient-phase mass dominated termwise by the geometric return envelope inherits the same `1 / rho` bound.

theorem theoremFourFiniteTransientMass_le_inv (rho : Real) (hrho_pos : 0 < rho) (hrho_le_one : rho <= 1) (phaseMass : Nat -> Real) (hphase : forall phase, phaseMass phase <= (1 - rho) ^ phase) (phaseCount : Nat) : (Finset.range phaseCount).sum phaseMass <= 1 / rho