BanditRLProof.FiniteRealArgmax

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

private theorem 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

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

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

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

private theorem score_le_chooseFin {K : Nat} (hK : 0 < K) (scores : Fin K -> Real) (a : Fin K) : scores a <= scores (chooseFin hK scores)

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

private theorem measurable_selected_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_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))

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

private theorem measurable_chooseFin_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 => chooseFin hK (scores omega))

A fixed-enumeration maximizer on a nonempty finite type.

noncomputable def choose {alpha : Type v} [Fintype alpha] [Nonempty alpha] (scores : alpha -> Real) : alpha

Every score is bounded by the score selected by `choose`.

theorem score_le_choose {alpha : Type v} [Fintype alpha] [Nonempty alpha] (scores : alpha -> Real) (a : alpha) : scores a <= scores (choose scores)

The fixed-enumeration maximizer is measurable in external parameters.

theorem measurable_choose_of_forall_measurable {Omega : Type u} {alpha : Type v} [MeasurableSpace Omega] [MeasurableSpace alpha] [Fintype alpha] [Nonempty alpha] (scores : Omega -> alpha -> Real) (hscores : forall a : alpha, Measurable (fun omega : Omega => scores omega a)) : Measurable (fun omega : Omega => choose (scores omega))

Evaluation at a measurable finite-valued selector preserves measurability.

theorem measurable_selected_score_of_forall_measurable {Omega : Type u} {alpha : Type v} [MeasurableSpace Omega] [MeasurableSpace alpha] [Fintype alpha] [MeasurableSingletonClass alpha] (scores : Omega -> alpha -> Real) (hscores : forall a : alpha, Measurable (fun omega : Omega => scores omega a)) (selected : Omega -> alpha) (hselected : Measurable selected) : Measurable (fun omega : Omega => scores omega (selected omega))