Data Processing Inequality

This file establishes the data processing inequality (DPI) for e-variables: applying a Markov kernel or measurable function cannot increase the maximum expected utility.

Main definitions

• maxUtility P S U: The maximum expected utility over all e-variables for S under measure P.
• maxRandUtility P S U: The maximum expected utility over randomized e-variables.

Main statements

• maxRandUtility_eq_maxUtility: Randomization does not increase maximum utility.
• maxUtility_comp_le, maxUtility_map_le: Data processing inequalities for kernels and functions.
• MeasurableEmbedding.maxUtility_map_eq: Equality holds for measurable embeddings.
• IsNumeraire.maxUtility_eq_integral: The numeraire attains the maximum log utility.
• convexOn_maxUtility: Maximum utility is convex in the measure.

noncomputable def ProbabilityTheory.maxUtility {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) (U : Utility) : EReal

The maximum utility ∫ᵉ x, (U ∘ X) x ∂P of a measure P over all e-variables X for a set of measures S.

Equations

• ProbabilityTheory.maxUtility P S U = ⨆ (X : 𝓧 → ENNReal), ⨆ (_ : ProbabilityTheory.IsEVar X S), ∫ᵉ (x : 𝓧), (U.toFun ∘ X) x ∂P

noncomputable def ProbabilityTheory.maxRandUtility {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) (U : Utility) : EReal

The maximum randomized utility ∫ᵉ x, U x ∂(η ∘ₘ P) of a measure P over all randomized e-variables η for a set of measures S.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.maxUtility_eq_sSup {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {U : Utility} : maxUtility P S U = sSup {y : EReal | ∃ (X : 𝓧 → ENNReal), IsEVar X S ∧ y = ∫ᵉ (x : 𝓧), (U.toFun ∘ X) x ∂P}

theorem ProbabilityTheory.maxRandUtility_eq_sSup {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {U : Utility} : maxRandUtility P S U = sSup {y : EReal | ∃ (η : Kernel 𝓧 ENNReal), IsMarkovKernel η ∧ IsRandEVar η S ∧ y = ∫ᵉ (x : ENNReal), U.toFun x ∂P.bind ⇑η}

@[simp]

theorem ProbabilityTheory.maxUtility_empty {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {U : Utility} : maxUtility P ∅ U = U.toFun ⊤ * ↑(P Set.univ)

theorem ProbabilityTheory.maxUtility_anti {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S T : Set (MeasureTheory.Measure 𝓧)} {U : Utility} (hS : S ⊆ T) : maxUtility P T U ≤ maxUtility P S U

theorem ProbabilityTheory.maxRandUtility_anti {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S T : Set (MeasureTheory.Measure 𝓧)} {U : Utility} (hS : S ⊆ T) : maxRandUtility P T U ≤ maxRandUtility P S U

theorem ProbabilityTheory.maxRandUtility_eq_maxUtility {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) : maxRandUtility P S U = maxUtility P S U

The maximum randomized utility is the maximum utility.

theorem ProbabilityTheory.maxUtility_eq_iSup_neBotUtilityEVar {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {U : Utility} : maxUtility P S U = ⨆ (X : 𝓧 → ENNReal), ⨆ (_ : NeBotUtilityEVar X P S U), ∫ᵉ (x : 𝓧), (U.toFun ∘ X) x ∂P

The maximum utility over e-variables equals the supremum over e-variables that has eintegral of the composition with the utility function not equal to ⊥.

theorem ProbabilityTheory.maxRandUtility_comp_le {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {U : Utility} (P : MeasureTheory.Measure 𝓧) {S : Set (MeasureTheory.Measure 𝓧)} (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] : maxRandUtility (P.bind ⇑κ) {x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ S, μ.bind ⇑κ = x} U ≤ maxRandUtility P S U

Data Processing Inequality for randomized utility a Markov kernel.

theorem ProbabilityTheory.maxUtility_comp_le {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {U : Utility} (P : MeasureTheory.Measure 𝓧) {S : Set (MeasureTheory.Measure 𝓧)} (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] : maxUtility (P.bind ⇑κ) {x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ S, μ.bind ⇑κ = x} U ≤ maxUtility P S U

Data processing inequality for the maximum utility and a Markov kernel.

theorem ProbabilityTheory.maxUtility_map_le {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {U : Utility} {φ : 𝓧 → 𝓨} (P : MeasureTheory.Measure 𝓧) {S : Set (MeasureTheory.Measure 𝓧)} (hφ : Measurable φ) : maxUtility (MeasureTheory.Measure.map φ P) {x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ S, MeasureTheory.Measure.map φ μ = x} U ≤ maxUtility P S U

Data processing inequality for the maximum utility and a measurable function.

theorem MeasurableEmbedding.maxUtility_map_eq {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {U : ProbabilityTheory.Utility} [Nonempty 𝓧] (φ : 𝓧 → 𝓨) (hφ : MeasurableEmbedding φ) (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) : ProbabilityTheory.maxUtility (MeasureTheory.Measure.map φ P) {x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ S, MeasureTheory.Measure.map φ μ = x} U = ProbabilityTheory.maxUtility P S U

DPI Equality: mapping by a measurable embeddings preserve maximum utility.

theorem ProbabilityTheory.IsNumeraire.maxUtility_eq_integral {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] {X : 𝓧 → ENNReal} (hX : IsNumeraire X S P) : maxUtility P S logUtility = ∫ᵉ (x : 𝓧), (X x).log ∂P

The numeraire attains the maximum logarithmic utility.

theorem ProbabilityTheory.maxUtility_eq_integral_numeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : maxUtility P S logUtility = ∫ᵉ (x : 𝓧), (numeraire P S x).log ∂P

theorem ProbabilityTheory.maxUtility_nonneg {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) : 0 ≤ maxUtility P S logUtility

The maximum log utility is nonnegative.

theorem ProbabilityTheory.convexOn_maxUtility {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} (S : Set (MeasureTheory.Measure 𝓧)) : ConvexOn ENNReal Set.univ fun (P : MeasureTheory.Measure 𝓧) => maxUtility P S U

The maximum utility is a convex function of the measure.

theorem ProbabilityTheory.maxUtility_involutive {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) {φ : 𝓧 → 𝓧} (hφ : Measurable φ) (hφ_inv : φ ∘ φ = id) : maxUtility P {x : MeasureTheory.Measure 𝓧 | ∃ μ ∈ S, MeasureTheory.Measure.map φ μ = x} U = maxUtility (MeasureTheory.Measure.map φ P) S U