BanditRLProof.Algorithms.ETCExactSubGaussianTail

Over the round-robin exploration horizon, the constant common-proxy pairwise process charges exactly `m` pulls of the candidate arm and `m` pulls of the selected best arm.

theorem sum_centeredPairwiseRewardDiffVarianceProxy_const_eq_two_mul {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (sigma2 : NNReal) (a : Fin K) (hne : a = model.bestArm -> False) : (Finset.range (spec.explorationPulls * K)).sum (fun t => ETC.centeredPairwiseRewardDiffVarianceProxy spec model model.bestArm (fun _ _ => sigma2) a t) = (2 : NNReal) * (spec.explorationPulls : NNReal) * sigma2

The deterministic centered pairwise threshold is `m` times the model gap.

theorem centeredPairwiseGapThreshold_eq_explorationPulls_mul_gap {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (a : Fin K) (hne : a = model.bestArm -> False) : ETC.centeredPairwiseGapThreshold spec model a = (spec.explorationPulls : Real) * ((model.gap a : Rat) : Real)

The canonical direct-MGF pairwise tail equals the exact LML exponential `exp (-m * gap^2 / (4 * sigma2))` for every non-best arm. Only `m > 0` is needed to cancel the exploration multiplicity. The `sigma2 = 0` boundary is handled separately and remains a valid equality in Lean's total division.

theorem canonicalSubGaussianArmPairwiseTailReal_eq_exp_neg_explorationPulls_mul_gap_sq_div_four_mul {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (sigma2 : NNReal) (a : Fin K) (hexplorationPulls_pos : 0 < spec.explorationPulls) (hne : a = model.bestArm -> False) : ETC.canonicalSubGaussianArmPairwiseTailReal spec model sigma2 a = Real.exp (-(spec.explorationPulls : Real) * ((model.gap a : Rat) : Real) ^ 2 / (4 * (sigma2 : Real)))

Exact-LML-constant form of the canonical single-arm commit-fiber probability bound under the existing common-sub-Gaussian `Rat` arm laws. This is a genuine concentration producer, but not yet the native `Real` reward-kernel theorem: the arm laws are measures on `Rat`, their centered casts have a common `NNReal` proxy, and the generated trajectory is the local canonical history process.

theorem real_measure_explorationArgmaxCommit_eq_arm_le_exp_neg_explorationPulls_mul_gap_sq_div_four_mul_of_armLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> MeasureTheory.Measure Rat) (hprob : forall arm, MeasureTheory.IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, MeasureTheory.integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (a : Fin K) (hne : a = model.bestArm -> False) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context := Context) armLaw hprob let policy := fun t => ETC.explorationArgmaxHistoryPolicy spec model t let state := fun t history => ETC.explorationArgmaxHistoryState t history let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext (fun t => ETC.measurable_explorationArgmaxHistoryState t) let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Rat) (armLaw defaultAction) stepKernel trajMeasure.real {trajectory : RewardTrace Rat | ETC.explorationArgmaxCommit spec model trajectory = a} <= Real.exp (-(spec.explorationPulls : Real) * ((model.gap a : Rat) : Real) ^ 2 / (4 * (sigma2 : Real)))

Canonical generated-history per-arm expected pull-count bound with the exact LML exponential constant, under the existing common-sub-Gaussian `Rat` arm laws. This theorem composes the concrete commit-fiber concentration producer with the generic Real/Bochner `actionWithCommit` expected-count consumer. It is the first local theorem with the full `m + (n - K*m) * exp (...)` per-arm shape. Native `Real` reward-kernel transport and external algorithm/environment-law alignment remain downstream.

theorem integral_real_pullCount_explorationArgmaxAction_le_exploration_add_remaining_mul_exp_of_armLaws {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> MeasureTheory.Measure Rat) (hprob : forall arm, MeasureTheory.IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, MeasureTheory.integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (a : Fin K) (n : Nat) (hn : K * spec.explorationPulls <= n) (hne : a = model.bestArm -> False) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context := Context) armLaw hprob let policy := fun t => ETC.explorationArgmaxHistoryPolicy spec model t let state := fun t history => ETC.explorationArgmaxHistoryState t history let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext (fun t => ETC.measurable_explorationArgmaxHistoryState t) let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Rat) (armLaw defaultAction) stepKernel MeasureTheory.integral trajMeasure (fun trajectory : RewardTrace Rat => ((pullCount (ETC.explorationArgmaxAction spec model trajectory) a n : Nat) : Real)) <= (spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * Real.exp (-(spec.explorationPulls : Real) * ((model.gap a : Rat) : Real) ^ 2 / (4 * (sigma2 : Real)))