BanditRLProof.Exp3MixedSquarePredictableVarianceRealizedMarkovHighProbabilityRegret

Cumulative predictable mixed-square variance on a generated trajectory.

noncomputable def sampledPredictableMixedSquaredVarianceSum {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (horizon : Nat) : Env × ((k : Nat) → Action × Real) → Real

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

theorem measurable_sampledPredictableMixedSquaredVarianceSum {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) : Measurable (sampledPredictableMixedSquaredVarianceSum arms eta gamma loss horizon)

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

theorem sampledPredictableMixedSquaredVarianceSum_nonneg {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 ≤ gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) : 0 ≤ sampledPredictableMixedSquaredVarianceSum arms eta gamma loss horizon sample

`lintegral` form of the cumulative predictable mixed-square variance.

noncomputable def sampledPredictableMixedSquaredVarianceLIntegral {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) → Action × Real))) (arms : Finset Action) (eta gamma : Real) (loss : PredictableLossVector Env Action) (horizon : Nat) : ENNReal

Mathlib-backed Markov tail for cumulative predictable mixed-square variance. The measure need not be finite.

theorem measure_sampledPredictableMixedSquaredVarianceSum_gt_le_lintegral_div {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) → Action × Real))) (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) (varianceBudget : Real) (hvarianceBudget : 0 < varianceBudget) : mu {sample | varianceBudget < sampledPredictableMixedSquaredVarianceSum arms eta gamma loss horizon sample} ≤ sampledPredictableMixedSquaredVarianceLIntegral mu arms eta gamma loss horizon / ENNReal.ofReal varianceBudget

Consume a cumulative predictable-variance `lintegral` budget in the realized-regret residual theorem.

theorem sampledPredictable_predictableVarianceSquareRealizedHighProbabilityRegret_tail_of_lintegral_variance_le {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) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (hhorizon : 0 < horizon) (varianceBudget deltaSquare deltaConfidence deltaRealized : Real) (hvarianceBudget : 0 < varianceBudget) (hdeltaSquare : 0 < deltaSquare) (hdeltaConfidence : 0 < deltaConfidence) (hdeltaRealized : 0 < deltaRealized) (varianceMeanBudget : Real) (hvarianceLIntegral : sampledPredictableMixedSquaredVarianceLIntegral (prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment) arms eta gamma loss horizon ≤ ENNReal.ofReal varianceMeanBudget) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareRealizedHighProbabilityRegretBudget arms eta gamma horizon varianceBudget deltaSquare deltaConfidence deltaRealized ≤ (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} ≤ (((ENNReal.ofReal deltaSquare + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaConfidence) + ENNReal.ofReal deltaRealized) + ENNReal.ofReal varianceMeanBudget / ENNReal.ofReal varianceBudget

Five-event realized-regret budget: four confidence failures and one Markov predictable-variance overflow failure.

noncomputable def sampledPredictableVarianceSquareRealizedMarkovHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon : Nat) (varianceMeanBudget delta : Real) : Real

Primary Markov-closed realized-regret theorem. A cumulative predictable variance `lintegral` bound is allocated the fifth failure probability.

theorem sampledPredictable_predictableVarianceSquareRealizedMarkovHighProbabilityRegret_tail_total_delta {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) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (hhorizon : 0 < horizon) (varianceMeanBudget delta : Real) (hvarianceMeanBudget : 0 < varianceMeanBudget) (hdelta : 0 < delta) (hvarianceLIntegral : sampledPredictableMixedSquaredVarianceLIntegral (prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment) arms eta gamma loss horizon ≤ ENNReal.ofReal varianceMeanBudget) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareRealizedMarkovHighProbabilityRegretBudget arms eta gamma horizon varianceMeanBudget delta ≤ (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} ≤ ENNReal.ofReal delta