BanditRLProof.Algorithms.ETCRealArgmaxTie

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

private theorem argmax_cons_eq_some_foldl_real_select {K : Nat} (scores : Fin K -> Real) (init : Fin K) (l : List (Fin K)) : List.argmax scores (init :: l) = some (l.foldl (fun best arm : Fin K => if scores best < scores arm then arm else best) init)

The native strict-update fold is Mathlib's first-occurrence list argmax.

theorem realArgmaxCommit_argmax_finRange {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) : List.argmax scores (List.finRange K) = some (ETC.realArgmaxCommit hK scores)

Among score maximizers, the native fold chooses the least encoded arm.

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

A natural number encodes a maximizing arm for the supplied score vector.

def RealEncodedArgmaxCandidate {K : Nat} (scores : Fin K -> Real) (n : Nat) : Prop

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

theorem exists_realEncodedArgmaxCandidate {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) : Exists fun n : Nat => ETC.RealEncodedArgmaxCandidate scores n

The least encoded natural-number witness of a maximizing arm.

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

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

theorem realLeastEncodedArgmaxIndex_candidate {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) : ETC.RealEncodedArgmaxCandidate scores (ETC.realLeastEncodedArgmaxIndex hK scores)

The maximizing arm decoded from the least `Nat.find` witness.

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

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

theorem realLeastEncodedArgmax_encode_eq_index {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) : Encodable.encode (ETC.realLeastEncodedArgmax hK scores) = ETC.realLeastEncodedArgmaxIndex hK scores

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

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

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

theorem realLeastEncodedArgmax_encode_le_of_isMax {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) (a : Fin K) (ha : forall z : Fin K, scores z <= scores a) : Encodable.encode (ETC.realLeastEncodedArgmax hK scores) <= Encodable.encode a

The LML-shaped least-encoded selector equals the native strict fold.

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

Round-robin exploration, least-encoded commit, and persistence determine the native Real ETC action trace. The boundary is written as `K * m` to match the upstream ETC behavior lemmas; the local trace uses the definitionally equivalent `m * K` boundary.

theorem eventually_realExplorationArgmaxAction_eq_of_roundRobin_leastEncodedCommit_persist {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (spec : ETC.Spec K) (baseCommitArm : Fin K) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (hactionExplore : forall t, t < K * spec.explorationPulls -> Filter.EventuallyEq (ae mu) (fun omega => action omega t) (fun _omega => ETC.exploreArm spec t)) (hactionCommit : Filter.EventuallyEq (ae mu) (fun omega => action omega (K * spec.explorationPulls)) (fun omega => ETC.realLeastEncodedArgmax spec.hK (fun arm => ETC.realEmpMeanAtExploration spec baseCommitArm (reward omega) arm))) (hactionPersist : forall t, K * spec.explorationPulls <= t -> Filter.EventuallyEq (ae mu) (fun omega => action omega t) (fun omega => action omega (K * spec.explorationPulls))) : Filter.Eventually (fun omega => forall t, action omega t = ETC.realExplorationArgmaxAction spec baseCommitArm (reward omega) t) (ae mu)

Exact native Real ETC regret from upstream-shaped feedback laws and the three ETC action behavior fields. Unlike the lower source adapter, callers do not provide a preassembled horizon action equality: exploration, least-encoded commit, and persistence construct it here.

theorem integral_realKernelRegret_externalAction_le_exact_sum_of_actionDependent_actionRewardHistory_condDistrib_of_leastEncodedCommit_persist {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (spec : ETC.Spec K) (nu : ProbabilityTheory.Kernel (Fin K) Real) [ProbabilityTheory.IsMarkovKernel nu] (sigma2 : NNReal) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward => reward - realKernelMean nu arm) sigma2 (nu arm)) (hm : 0 < spec.explorationPulls) (n : Nat) (hn : K * spec.explorationPulls <= n) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (hactionExplore : forall t, t < K * spec.explorationPulls -> Filter.EventuallyEq (ae mu) (fun omega => action omega t) (fun _omega => ETC.exploreArm spec t)) (hactionCommit : Filter.EventuallyEq (ae mu) (fun omega => action omega (K * spec.explorationPulls)) (fun omega => ETC.realLeastEncodedArgmax spec.hK (fun arm => ETC.realEmpMeanAtExploration spec (ETC.realKernelBestArm spec.hK nu) (reward omega) arm))) (hactionPersist : forall t, K * spec.explorationPulls <= t -> Filter.EventuallyEq (ae mu) (fun omega => action omega t) (fun omega => action omega (K * spec.explorationPulls))) (hzero : ProbabilityTheory.condDistrib (fun omega => reward omega 0) (fun omega => action omega 0) mu =ᵐ[mu.map (fun omega => action omega 0)] ProbabilityTheory.Kernel.ofFunOfCountable (fun arm : Fin K => nu arm)) (hcond : forall i, i < spec.explorationPulls * K - 1 -> let fullCondition := fun omega : Omega => (History.finitePairHistoryOfTrace (action omega) (reward omega) i, action omega (i + 1)) ProbabilityTheory.condDistrib (fun omega => reward omega (i + 1)) fullCondition mu =ᵐ[mu.map fullCondition] (RewardKernel.contextIndependentOfActionLaws (Context