BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovExplicitTuning

The five-way confidence allocation has logarithmic budget `log (5 / delta)`.

theorem log_one_div_fifth_eq_log_five_div (delta : Real) (hdelta : 0 < delta) : Real.log (1 / (delta / 5)) = Real.log (5 / delta)

Closed form of the sparse-loss Markov predictable-variance budget.

theorem sparseLossPredictableVarianceBudget_eq {Action : Type v} (arms : Finset Action) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon sparsity : Nat) (delta : Real) (hdelta : 0 < delta) : sparseLossPredictableVarianceBudget arms gamma horizon sparsity delta = 5 * (arms.card : Real) * (sparsity : Real) * (horizon : Real) / (gamma * delta)

Under the sparse base, fifth-power Markov, and cubic confidence contracts, the log-weighted mixed-square radius is at most `3 * gamma^2 * T^2`.

theorem log_mul_sparseLossPredictableVarianceRadius_le_three_mul_sq_mul_horizon_sq {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hbase : (sparsity : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : 5 * (arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (5 / delta) <= gamma ^ 5 * delta * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (5 / delta) <= gamma ^ 3 * (horizon : Real)) : Real.log (arms.card : Real) * sampledMixedSquaredPredictableVarianceRadius arms gamma (sparseLossPredictableVarianceBudget arms gamma horizon sparsity delta) (delta / 5) <= 3 * gamma ^ 2 * (horizon : Real) ^ 2

The sparse base term and Markov predictable-variance radius make the learning-rate-balanced square root at most `2 * gamma * T`.

theorem sparseLossPredictableVarianceBalancedSqrt_le_two_mul_gamma_mul_horizon {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hbase : (sparsity : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : 5 * (arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (5 / delta) <= gamma ^ 5 * delta * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (5 / delta) <= gamma ^ 3 * (horizon : Real)) : Real.sqrt (Real.log (arms.card : Real) * sparseLossPredictableVarianceHighProbabilityScale arms gamma horizon sparsity delta) <= 2 * gamma * (horizon : Real)

Explicit sparse-loss realized-regret threshold after exploration tuning.

noncomputable def sparseLossPredictableVarianceRealizedMarkovExplicitThreshold {Action : Type v} (_arms : Finset Action) (gamma : Real) (horizon _sparsity : Nat) (_delta : Real) : Real

The four algebraic exploration contracts reduce the eta-tuned threshold to `14 * gamma * T`.

theorem sparseLossPredictableVarianceRealizedMarkovTunedThreshold_le_explicitThreshold {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 <= arms.card) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (gamma delta : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hbase : (sparsity : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : 5 * (arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (5 / delta) <= gamma ^ 5 * delta * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (5 / delta) <= gamma ^ 3 * (horizon : Real)) (hrealized : 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (5 / delta) <= gamma ^ 2 * (horizon : Real)) : sparseLossPredictableVarianceRealizedMarkovTunedThreshold arms gamma horizon sparsity delta <= sparseLossPredictableVarianceRealizedMarkovExplicitThreshold arms gamma horizon sparsity delta

Generated sparse-loss realized-regret tail under four algebraic exploration contracts.

theorem sampledPredictable_gammaCharacterizedSparseLossPredictableVarianceRealizedMarkovRegret_tail {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hbase : (sparsity : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : 5 * (arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (5 / delta) <= gamma ^ 5 * delta * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (5 / delta) <= gamma ^ 3 * (horizon : Real)) (hrealized : 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (5 / delta) <= gamma ^ 2 * (horizon : Real)) (hsparse : ∀ sample t, t < horizon → (sampledPredictableLossSupport arms loss t sample).card <= sparsity) : let eta := sparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma <= 1) loss.environment mu {sample | sparseLossPredictableVarianceRealizedMarkovExplicitThreshold arms gamma horizon sparsity delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta

Square-root component required by the pathwise sparse-loss base term.

noncomputable def sparseLossPredictableVarianceArmExplorationScale (K S T : Real) : Real

Fifth-root component forced by the sparse-loss Markov variance threshold.

noncomputable def sparseLossPredictableVarianceMarkovExplorationScale (K S T delta : Real) : Real

Cube-root component required by both Bernstein confidence radii.

noncomputable def sparseLossPredictableVarianceConfidenceExplorationScale (K T delta : Real) : Real

Square-root component required by the bounded realized-deviation radius.

noncomputable def sparseLossPredictableVarianceRealizedExplorationScale (T delta : Real) : Real

Unclipped maximum of the four sparse-loss exploration scales.

noncomputable def sparseLossPredictableVarianceRawExplorationRate (K S T delta : Real) : Real

Explicit exploration schedule clipped into the Hedge stability regime.

noncomputable def sparseLossPredictableVarianceClippedExplorationRate (K S T delta : Real) : Real

A nonnegative fifth-root scale is at most one half when its numerator is at most one thirty-second of its positive denominator.

theorem rpow_inv_five_le_half_of_thirtytwo_mul_le (numerator denominator : Real) (hnumerator : 0 <= numerator) (hdenominator : 0 < denominator) (hlarge : 32 * numerator <= denominator) : (numerator / denominator) ^ (5 : Real)⁻¹ <= 1 / 2

If a fifth-root scale is below `gamma`, its numerator satisfies the corresponding fifth-power dominance contract.

theorem numerator_le_pow_five_mul_of_rpow_inv_five_le (numerator denominator gamma : Real) (hnumerator : 0 <= numerator) (hdenominator : 0 < denominator) (hroot : (numerator / denominator) ^ (5 : Real)⁻¹ <= gamma) : numerator <= gamma ^ 5 * denominator

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

theorem sparseLossPredictableVarianceClippedExplorationRate_le_half (K S T delta : Real) : sparseLossPredictableVarianceClippedExplorationRate K S T delta <= 1 / 2

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

theorem sparseLossPredictableVarianceClippedExplorationRate_eq_raw (K S T delta : Real) (hraw : sparseLossPredictableVarianceRawExplorationRate K S T delta <= 1 / 2) : sparseLossPredictableVarianceClippedExplorationRate K S T delta = sparseLossPredictableVarianceRawExplorationRate K S T delta

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

theorem sparseLossPredictableVarianceRawExplorationRate_pos (K S T delta : Real) (hK_one : 1 < K) (hS : 0 < S) (hT : 0 < T) : 0 < sparseLossPredictableVarianceRawExplorationRate K S T delta

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

theorem sparseLossPredictableVarianceClippedExplorationRate_pos (K S T delta : Real) (hK_one : 1 < K) (hS : 0 < S) (hT : 0 < T) : 0 < sparseLossPredictableVarianceClippedExplorationRate K S T delta

Four transparent horizon contracts ensure every raw schedule component is at most one half, so clipping is inactive.

theorem sparseLossPredictableVarianceRawExplorationRate_le_half_of_horizon_contracts (K S T delta : Real) (hK_one : 1 < K) (hS : 0 < S) (hT : 0 < T) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge_arm : 4 * (S * Real.log K) <= T) (hlarge_mixed : 32 * (5 * K * S * Real.log K ^ 2 * Real.log (5 / delta)) <= delta * T ^ 3) (hlarge_confidence : 8 * (K * Real.log (5 / delta)) <= T) (hlarge_realized : 8 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (5 / delta) <= T) : sparseLossPredictableVarianceRawExplorationRate K S T delta <= 1 / 2

The clipped maximum satisfies exactly the four contracts consumed by the gamma-characterized sparse-loss theorem.

theorem sparseLossPredictableVarianceClippedExplorationRate_contracts (K S T delta : Real) (hK_one : 1 < K) (hS : 0 < S) (hT : 0 < T) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge_arm : 4 * (S * Real.log K) <= T) (hlarge_mixed : 32 * (5 * K * S * Real.log K ^ 2 * Real.log (5 / delta)) <= delta * T ^ 3) (hlarge_confidence : 8 * (K * Real.log (5 / delta)) <= T) (hlarge_realized : 8 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (5 / delta) <= T) : let gamma := sparseLossPredictableVarianceClippedExplorationRate K S T delta 0 < gamma ∧ gamma <= 1 / 2 ∧ S * Real.log K <= gamma ^ 2 * T ∧ 5 * K * S * Real.log K ^ 2 * Real.log (5 / delta) <= gamma ^ 5 * delta * T ^ 3 ∧ K * Real.log (5 / delta) <= gamma ^ 3 * T ∧ 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (5 / delta) <= gamma ^ 2 * T

Fully explicit generated sparse-loss realized-regret tail for the clipped maximum of the four exploration scales.

theorem sampledPredictable_explicitSparseLossPredictableVarianceRealizedMarkovRegret_tail {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge_arm : 4 * ((sparsity : Real) * Real.log (arms.card : Real)) <= (horizon : Real)) (hlarge_mixed : 32 * (5 * (arms.card : Real) * (sparsity : Real) * Real.log (arms.card : Real) ^ 2 * Real.log (5 / delta)) <= delta * (horizon : Real) ^ 3) (hlarge_confidence : 8 * ((arms.card : Real) * Real.log (5 / delta)) <= (horizon : Real)) (hlarge_realized : 8 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (5 / delta) <= (horizon : Real)) (hsparse : ∀ sample t, t < horizon → (sampledPredictableLossSupport arms loss t sample).card <= sparsity) : let gamma := sparseLossPredictableVarianceClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) delta let eta := sparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (sparseLossPredictableVarianceClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) delta (by exact_mod_cast hcard_two) (by exact_mod_cast hsparsity) (by exact_mod_cast hhorizon)).le (by exact (sparseLossPredictableVarianceClippedExplorationRate_le_half (arms.card : Real) (sparsity : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu {sample | sparseLossPredictableVarianceRealizedMarkovExplicitThreshold arms gamma horizon sparsity delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta