Measurable argmax function

theorem measurable_encode {α : Type u_1} {x✝ : MeasurableSpace α} [Encodable α] [MeasurableSingletonClass α] : Measurable Encodable.encode

theorem measurableEmbedding_encode (α : Type u_1) {x✝ : MeasurableSpace α} [Encodable α] [MeasurableSingletonClass α] : MeasurableEmbedding Encodable.encode

theorem measurableSet_isMax {𝓧 : Type u_1} {𝓨 : Type u_2} {α : Type u_3} {m𝓧 : MeasurableSpace 𝓧} {mα : MeasurableSpace α} [TopologicalSpace α] [LinearOrder α] [OpensMeasurableSpace α] [OrderClosedTopology α] [SecondCountableTopology α] [Countable 𝓨] {f : 𝓧 → 𝓨 → α} (hf : ∀ (y : 𝓨), Measurable fun (x : 𝓧) => f x y) (y : 𝓨) : MeasurableSet {x : 𝓧 | ∀ (z : 𝓨), f x z ≤ f x y}

theorem exists_isMaxOn' {𝓧 : Type u_1} {𝓨 : Type u_2} {α : Type u_4} [LinearOrder α] [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] (f : 𝓧 → 𝓨 → α) (x : 𝓧) : ∃ (n : ℕ) (y : 𝓨), n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y

noncomputable def measurableArgmax {𝓧 : Type u_1} {𝓨 : Type u_2} {α : Type u_3} {m𝓨 : MeasurableSpace 𝓨} [LinearOrder α] [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨] (f : 𝓧 → 𝓨 → α) [(x : 𝓧) → DecidablePred fun (n : ℕ) => ∃ (y : 𝓨), n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y] (x : 𝓧) : 𝓨

A measurable argmax function.

Equations

• measurableArgmax f x = ⋯.invFun (Nat.find ⋯)

theorem measurable_measurableArgmax {𝓧 : Type u_1} {𝓨 : Type u_2} {α : Type u_3} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {mα : MeasurableSpace α} [TopologicalSpace α] [LinearOrder α] [OpensMeasurableSpace α] [OrderClosedTopology α] [SecondCountableTopology α] [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨] {f : 𝓧 → 𝓨 → α} [(x : 𝓧) → DecidablePred fun (n : ℕ) => ∃ (y : 𝓨), n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y] (hf : ∀ (y : 𝓨), Measurable fun (x : 𝓧) => f x y) : Measurable (measurableArgmax f)

theorem isMaxOn_measurableArgmax {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} {α : Type u_4} [LinearOrder α] [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨] (f : 𝓧 → 𝓨 → α) [(x : 𝓧) → DecidablePred fun (n : ℕ) => ∃ (y : 𝓨), n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y] (x : 𝓧) (z : 𝓨) : f x z ≤ f x (measurableArgmax f x)