BanditRLProof.Algorithms.ETCArgmaxOracle

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

private theorem score_le_foldl_select {K : Nat} (scores : Fin K -> Rat) (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

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

private theorem argmax_cons_eq_some_foldl_rat_select {K : Nat} (scores : Fin K -> Rat) (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)

A concrete ETC commit oracle that selects a score-maximizing arm from `Fin K`. The selector scans `List.finRange K` and keeps the previous arm on ties, giving a deterministic total oracle whenever `hK : 0 < K` supplies the initial arm. This is the compiled `ETC-COMMIT-ORACLE-CONCRETE-ARGMAX` leaf.

noncomputable def argmaxCommitOracle {K : Nat} (hK : 0 < K) : ETC.CommitOracle K where

The concrete Rat commit oracle is Mathlib's first-occurrence list argmax. Because `List.finRange K` is ordered by the canonical `Fin` encoding, this identity records the implementation-level tie rule used by the generated ETC policy: strict score improvements replace the current arm and equal scores do not.

theorem argmaxCommitOracle_argmax_finRange {K : Nat} (hK : 0 < K) (scores : Fin K -> Rat) : List.argmax scores (List.finRange K) = some ((ETC.argmaxCommitOracle hK).choose scores)

Among arms tying the concrete Rat commit oracle's maximal score, the oracle chooses the least encoded arm. This is the public tie-semantics certificate for the canonical generated ETC route. It is deterministic and introduces no probability or concentration assumption.

theorem argmaxCommitOracle_encode_le_of_score_le {K : Nat} (hK : 0 < K) (scores : Fin K -> Rat) (a : Fin K) (hscore : scores ((ETC.argmaxCommitOracle hK).choose scores) <= scores a) : Encodable.encode ((ETC.argmaxCommitOracle hK).choose scores) <= Encodable.encode a

The concrete ETC argmax oracle returns an arm whose score dominates every arm. This is the maximality certificate needed by the already compiled abstract commit-oracle wrong-event and probability consumers. It does not introduce measures, empirical-mean construction, concentration, filtration, or final ETC regret.

theorem argmaxCommitOracle_choose_spec {K : Nat} (hK : 0 < K) (scores : Fin K -> Rat) (a : Fin K) : scores a <= scores ((ETC.argmaxCommitOracle hK).choose scores)

Selecting a particular arm with the concrete ETC argmax implies that arm's score is at least the selected model best arm's score. This is a deterministic single-fiber refinement of the existing wrong-commit union reduction. It preserves the candidate arm instead of existentially or union bounding it.

theorem argmaxCommitOracle_eq_arm_subset_empMean_ge_bestArm {Omega : Type u} {K : Nat} (hK : 0 < K) (model : FiniteBanditModel K) (empMean : Omega -> Fin K -> Rat) (a : Fin K) : Set.Subset {omega : Omega | (ETC.argmaxCommitOracle hK).choose (empMean omega) = a} {omega : Omega | empMean omega a >= empMean omega model.bestArm}

The probability of committing to one concrete arm is bounded by any supplied tail bound for that arm's empirical mean exceeding the model best arm's mean. No union bound is taken. The result uses only measure monotonicity and the deterministic concrete-argmax fiber inclusion above.

theorem prob_argmaxCommitOracle_eq_arm_le_pairwise_tail {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (hK : 0 < K) (mu : MeasureTheory.Measure Omega) (model : FiniteBanditModel K) (empMean : Omega -> Fin K -> Rat) (tail : Fin K -> ENNReal) (a : Fin K) (hpair_tail : mu {omega : Omega | empMean omega a >= empMean omega model.bestArm} <= tail a) : mu {omega : Omega | (ETC.argmaxCommitOracle hK).choose (empMean omega) = a} <= tail a

The concrete argmax oracle instantiates the existing deterministic wrong-commit event reduction. This wrapper records that the new concrete oracle feeds directly into the previous abstract `CommitOracle` consumer. It remains a deterministic set inclusion, with no probability or concentration assumptions.

theorem wrong_commit_subset_exists_empMean_ge_bestArm_of_argmaxOracle {Omega : Type u} {K : Nat} (hK : 0 < K) (model : FiniteBanditModel K) (empMean : Omega -> Fin K -> Rat) : Set.Subset {omega : Omega | (ETC.argmaxCommitOracle hK).choose (empMean omega) = model.bestArm -> False} {omega : Omega | exists a : Fin K, (a = model.bestArm -> False) /\ empMean omega a >= empMean omega model.bestArm}

The concrete argmax oracle-selected wrong-commit event is bounded by the filtered finite sum of abstract non-best pairwise tail bounds. This is the `ETC-COMMIT-ORACLE-CONCRETE-FILTERED-SUM-PAIRWISE-TAIL` leaf. It only specializes the already compiled abstract oracle filtered-sum consumer to `ETC.argmaxCommitOracle`; it does not prove pairwise tails, add concentration, introduce filtration, or prove final ETC regret.

theorem prob_argmaxCommitOracle_ne_bestArm_le_filtered_sum_pairwise_tail {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (hK : 0 < K) (mu : MeasureTheory.Measure Omega) (model : FiniteBanditModel K) (empMean : Omega -> Fin K -> Rat) (tail : Fin K -> ENNReal) (hpair_tail : forall a : Fin K, (a = model.bestArm -> False) -> mu {omega : Omega | empMean omega a >= empMean omega model.bestArm} <= tail a) : mu {omega : Omega | (ETC.argmaxCommitOracle hK).choose (empMean omega) = model.bestArm -> False} <= ((Finset.univ : Finset (Fin K)).filter (fun a : Fin K => a = model.bestArm -> False)).sum tail