Lean module · Foundations
BanditRLProof.FiniteRealArgmax
# Measurable finite Real argmax This module provides a fixed-enumeration maximizer for Real-valued scores on a nonempty finite type. Unlike a bare `Classical.choose` over existence of a maximum, the explicit fold remains measurable when every score coordinate is measurable in an external parameter.
Module map
Imports
BanditRLProof.MeasurableLocalQuantities
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteRealArgmax.score_le_foldl_select
Compiled Internal helper
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
def
BanditRLProof.FiniteRealArgmax.chooseFin
Compiled Internal helper
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
theorem
BanditRLProof.FiniteRealArgmax.score_le_chooseFin
Compiled Internal helper
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)
theorem
BanditRLProof.FiniteRealArgmax.measurable_selected_score
Compiled Internal helper
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))
theorem
BanditRLProof.FiniteRealArgmax.measurable_foldl_select
Compiled Internal helper
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))
theorem
BanditRLProof.FiniteRealArgmax.measurable_chooseFin_of_forall_measurable
Compiled Internal helper
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))
def
BanditRLProof.FiniteRealArgmax.choose
Compiled
A fixed-enumeration maximizer on a nonempty finite type.
noncomputable def choose {alpha : Type v} [Fintype alpha] [Nonempty alpha] (scores : alpha -> Real) : alpha
theorem
BanditRLProof.FiniteRealArgmax.score_le_choose
Compiled
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)
theorem
BanditRLProof.FiniteRealArgmax.measurable_choose_of_forall_measurable
Compiled
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))
theorem
BanditRLProof.FiniteRealArgmax.measurable_selected_score_of_forall_measurable
Compiled
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))