BanditRLProof.Algorithms.ETCRealEmpiricalMean

The exploration empirical mean formed directly from a Real reward trace.

noncomputable def realEmpMeanAtExploration {K : Nat} (spec : ETC.Spec K) (baseCommitArm : Fin K) (reward : RewardTrace Real) (a : Fin K) : Real

The deterministic exploration count removes the pull-count denominator.

theorem realEmpMeanAtExploration_eq_sumRewards_div_explorationPulls {K : Nat} (spec : ETC.Spec K) (baseCommitArm : Fin K) (reward : RewardTrace Real) (a : Fin K) : ETC.realEmpMeanAtExploration spec baseCommitArm reward a = sumRewards (ETC.actionWithCommit spec baseCommitArm) reward a (spec.explorationPulls * K) / (spec.explorationPulls : Real)

Real exploration empirical means are measurable from measurable rewards.

theorem measurable_realEmpMeanAtExploration {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (spec : ETC.Spec K) (baseCommitArm a : Fin K) (reward : Omega -> RewardTrace Real) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) : Measurable (fun omega : Omega => ETC.realEmpMeanAtExploration spec baseCommitArm (reward omega) a)

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

private theorem real_score_le_foldl_select {K : Nat} (scores : Fin K -> Real) (init : Fin K) : forall l : List (Fin K), (forall a : Fin K, List.Mem a l -> scores a <= scores (l.foldl (fun best arm : Fin K => if scores best < scores arm then arm else best) init)) /\ scores init <= scores (l.foldl (fun best arm : Fin K => if scores best < scores arm then arm else best) init) | [] => by exact And.intro (by intro _ ha; cases ha) (by simp) | arm :: rest => by let select := fun best arm : Fin K => if scores best < scores arm then arm else best let next := select init arm have ih

A deterministic finite argmax for Real-valued arm scores.

noncomputable def realArgmaxCommit {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) : Fin K

The Real finite argmax dominates every arm score.

theorem realArgmaxCommit_spec {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) (a : Fin K) : scores a <= scores (ETC.realArgmaxCommit hK scores)

On a constant score vector, the tie rule keeps the initial arm `0`.

@[simp] theorem realArgmaxCommit_const {K : Nat} (hK : 0 < K) (c : Real) : ETC.realArgmaxCommit hK (fun _a : Fin K => c) = Fin.mk 0 hK

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

private theorem measurable_selected_real_score {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (scores : Omega -> Fin K -> Real) (hscores : forall a : Fin K, Measurable (fun omega : Omega => scores omega a)) (best : Omega -> Fin K) (hbest : Measurable best) : Measurable (fun omega : Omega => scores omega (best omega))

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

private theorem measurable_foldl_real_select {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (scores : Omega -> Fin K -> Real) (hscores : forall a : Fin K, Measurable (fun omega : Omega => scores omega a)) (best : Omega -> Fin K) (hbest : Measurable best) : forall l : List (Fin K), Measurable (fun omega : Omega => l.foldl (fun best arm : Fin K => if scores omega best < scores omega arm then arm else best) (best omega)) | [] => by simpa using hbest | arm :: rest => by have hselected : Measurable (fun omega : Omega => scores omega (best omega))

The finite Real argmax is measurable when every score coordinate is.

theorem measurable_realArgmaxCommit_of_forall_measurable {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (hK : 0 < K) (scores : Omega -> Fin K -> Real) (hscores : forall a : Fin K, Measurable (fun omega : Omega => scores omega a)) : Measurable (fun omega : Omega => ETC.realArgmaxCommit hK (scores omega))

Commit to the arm maximizing the native Real exploration means.

noncomputable def realExplorationArgmaxCommit {K : Nat} (spec : ETC.Spec K) (baseCommitArm : Fin K) (reward : RewardTrace Real) : Fin K

Native Real ETC trace: round-robin exploration, then Real empirical argmax.

noncomputable def realExplorationArgmaxAction {K : Nat} (spec : ETC.Spec K) (baseCommitArm : Fin K) (reward : RewardTrace Real) : ActionTrace (Fin K)

The reward-dependent native Real ETC commit arm is measurable.

theorem measurable_realExplorationArgmaxCommit {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (spec : ETC.Spec K) (baseCommitArm : Fin K) (reward : Omega -> RewardTrace Real) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) : Measurable (fun omega : Omega => ETC.realExplorationArgmaxCommit spec baseCommitArm (reward omega))

Exact expected pull count for the native Real empirical-argmax ETC trace.

theorem integral_real_pullCount_realExplorationArgmaxAction_eq_exploration_add_remaining_mul_commit_prob {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (spec : ETC.Spec K) (baseCommitArm : Fin K) (reward : Omega -> RewardTrace Real) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (a : Fin K) (n : Nat) (hn : K * spec.explorationPulls <= n) : integral mu (fun omega : Omega => ((pullCount (ETC.realExplorationArgmaxAction spec baseCommitArm (reward omega)) a n : Nat) : Real)) = (spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * mu.real {omega : Omega | ETC.realExplorationArgmaxCommit spec baseCommitArm (reward omega) = a}

A commit-fiber bound immediately yields the native Real expected count bound.

theorem integral_real_pullCount_realExplorationArgmaxAction_le_exploration_add_remaining_mul_of_commit_prob_le {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (spec : ETC.Spec K) (baseCommitArm : Fin K) (reward : Omega -> RewardTrace Real) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (a : Fin K) (n : Nat) (p : Real) (hn : K * spec.explorationPulls <= n) (hprob : mu.real {omega : Omega | ETC.realExplorationArgmaxCommit spec baseCommitArm (reward omega) = a} <= p) : integral mu (fun omega : Omega => ((pullCount (ETC.realExplorationArgmaxAction spec baseCommitArm (reward omega)) a n : Nat) : Real)) <= (spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * p