Finite suprema of convex functions

[UPSTREAM] candidates for Mathlib/Analysis/Convex/ (likely Jensen.lean: the binary lemmas''s home Function.lean is deliberately Finset-free, and the ContinuousAt.finset_sup'' family likewise lives downstream in Topology/Order/Lattice.lean): the finite (Finset.sup') generalization of ConvexOn.sup, and its concave dual. The support function of a finite family of affine functionals — the "max of affine is convex" fact underlying decision values, Bayes risk, and Blackwell comparison — is the instance over a Finset` of linear maps.

theorem ConvexOn.finset_sup' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {ι : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {t : Finset ι} (ht : t.Nonempty) {f : ι → E → β} (hf : ∀ i ∈ t, ConvexOn 𝕜 s (f i)) : ConvexOn 𝕜 s (t.sup' ht f)

The supremum of a nonempty finite family of convex functions is convex: the Finset.sup' generalization of ConvexOn.sup.

theorem ConvexOn.finset_sup'_apply {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {ι : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {t : Finset ι} (ht : t.Nonempty) {f : ι → E → β} (hf : ∀ i ∈ t, ConvexOn 𝕜 s (f i)) : ConvexOn 𝕜 s fun (x : E) => t.sup' ht fun (x_1 : ι) => f x_1 x

Pointwise form of ConvexOn.finset_sup'.

theorem ConcaveOn.finset_inf' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {ι : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {t : Finset ι} (ht : t.Nonempty) {f : ι → E → β} (hf : ∀ i ∈ t, ConcaveOn 𝕜 s (f i)) : ConcaveOn 𝕜 s (t.inf' ht f)

The infimum of a nonempty finite family of concave functions is concave: the Finset.inf' generalization of ConcaveOn.inf.

theorem ConcaveOn.finset_inf'_apply {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {ι : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {t : Finset ι} (ht : t.Nonempty) {f : ι → E → β} (hf : ∀ i ∈ t, ConcaveOn 𝕜 s (f i)) : ConcaveOn 𝕜 s fun (x : E) => t.inf' ht fun (x_1 : ι) => f x_1 x

Pointwise form of ConcaveOn.finset_inf'.