Argmax and argmin functions on finite sets

We prove in particular that those functions are measurable.

@[reducible, inline]

abbrev Function.max {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) : α

The maximum value of a tuple.

Equations

• Function.max f = Finset.univ.sup' ⋯ f

@[reducible, inline]

abbrev Function.min {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) : α

The minimum value of a tuple.

Equations

• Function.min f = Finset.univ.inf' ⋯ f

theorem Function.le_max {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) (x : ι) : f x ≤ max f

theorem Function.min_le {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) (x : ι) : min f ≤ f x

theorem exists_argmax {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) : ∃ (i : ι), f i = Function.max f

theorem exists_argmin {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) : ∃ (i : ι), f i = Function.min f

noncomputable def argmax {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) : ι

The index of the maximum value of a tuple.

Equations

• argmax f = ⋯.choose

noncomputable def argmin {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) : ι

The index of the minimum value of a tuple.

Equations

• argmin f = ⋯.choose

theorem argmax_spec {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) : f (argmax f) = Function.max f

theorem argmin_spec {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) : f (argmin f) = Function.min f

theorem isMaxOn_argmax {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) (x : ι) : f x ≤ f (argmax f)

theorem isMinOn_argmin {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) (x : ι) : f (argmin f) ≤ f x

theorem measurable_max {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] [MeasurableSpace α] [MeasurableSup₂ α] : Measurable fun (t : ι → α) => Function.max t

theorem measurable_min {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] [MeasurableSpace α] [MeasurableInf₂ α] : Measurable fun (t : ι → α) => Function.min t

theorem measurable_argmax {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] [MeasurableSpace α] [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂ α] : Measurable fun (f : ι → α) => argmax f

theorem measurable_argmin {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] [MeasurableSpace α] [MeasurableSpace ι] [MeasurableEq α] [MeasurableInf₂ α] : Measurable fun (f : ι → α) => argmin f

theorem neg_max_eq_min_neg {ι : Type u_1} {α : Type u_2} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) [AddGroup α] [AddLeftMono α] [AddRightMono α] : -Function.max f = Function.min (-f)