Utility Functions

This file defines utility functions for use in probability theory and e-value theory.

Main definitions

• Utility: A structure representing a concave, monotone, and differentiable function from ℝ≥0∞ to EReal, which is finite on (0, ∞).
• Utility.deriv: The derivative of a utility function.
• logUtility: The logarithmic utility function.

Main statements

• Utility.eintegral_le_map: Jensen's inequality for utility functions.
• Utility.le_add_deriv_mul: The utility function is upper-bounded by its first-order Taylor approximation (a consequence of concavity).
• deriv_logUtility: The derivative of the logarithmic utility function.

structure ProbabilityTheory.Utility : Type

A utility function is a concave, monotone and differentiable function from ℝ≥0∞ to EReal, which is finite on (0, ∞).

• toFun : ENNReal → EReal

  The function itself.

• eq_coe' (x : ENNReal) : x ≠ 0 → x ≠ ⊤ → self.toFun x ≠ ⊥ ∧ self.toFun x ≠ ⊤
• monotone' : Monotone self.toFun
• continuous' : Continuous self.toFun
• concave' : ConcaveOn NNReal Set.univ self.toFun
• differentiable' : ContDiffOn ℝ 1 (fun (x : ℝ) => (self.toFun (ENNReal.ofReal x)).toReal) (Set.Ioi 0)

@[implicit_reducible]

instance ProbabilityTheory.instCoeFunUtilityForallENNRealEReal : CoeFun Utility fun (x : Utility) => ENNReal → EReal

Equations

• ProbabilityTheory.instCoeFunUtilityForallENNRealEReal = { coe := ProbabilityTheory.Utility.toFun }

theorem ProbabilityTheory.Utility.eq_coe (U : Utility) {x : ENNReal} (hx0 : x ≠ 0) (hx_top : x ≠ ⊤) : U.toFun x ≠ ⊥ ∧ U.toFun x ≠ ⊤

theorem ProbabilityTheory.Utility.monotone (U : Utility) : Monotone U.toFun

theorem ProbabilityTheory.Utility.continuous (U : Utility) : Continuous U.toFun

theorem ProbabilityTheory.Utility.measurable (U : Utility) : Measurable U.toFun

theorem ProbabilityTheory.Utility.aemeasurable {μ : MeasureTheory.Measure ENNReal} (U : Utility) : AEMeasurable U.toFun μ

theorem ProbabilityTheory.Utility.concave (U : Utility) : ConcaveOn NNReal Set.univ U.toFun

theorem ProbabilityTheory.Utility.ne_top (U : Utility) {x : ENNReal} (hx_top : x ≠ ⊤) : U.toFun x ≠ ⊤

theorem ProbabilityTheory.Utility.ne_bot (U : Utility) {x : ENNReal} (hx0 : x ≠ 0) : U.toFun x ≠ ⊥

def ProbabilityTheory.Utility.real (U : Utility) : ℝ → ℝ

The real-valued representation of a utility function.

Equations

• U.real x = (U.toFun (ENNReal.ofReal x)).toReal

theorem ProbabilityTheory.Utility.real_toReal (U : Utility) {x : ENNReal} (hx_top : x ≠ ⊤) : U.real x.toReal = (U.toFun x).toReal

theorem ProbabilityTheory.Utility.coe_real_toReal' (U : Utility) {x : ENNReal} (hx0 : U.toFun x ≠ ⊥) (hx_top : x ≠ ⊤) : ↑(U.real x.toReal) = U.toFun x

theorem ProbabilityTheory.Utility.coe_real_toReal (U : Utility) {x : ENNReal} (hx0 : x ≠ 0) (hx_top : x ≠ ⊤) : ↑(U.real x.toReal) = U.toFun x

theorem ProbabilityTheory.Utility.contDiffOn (U : Utility) : ContDiffOn ℝ 1 U.real (Set.Ioi 0)

theorem ProbabilityTheory.Utility.differentiableOn (U : Utility) : DifferentiableOn ℝ U.real (Set.Ioi 0)

theorem ProbabilityTheory.Utility.monotoneOn_Ioi_real (U : Utility) : MonotoneOn U.real (Set.Ioi 0)

theorem ProbabilityTheory.Utility.monotoneOn_Ici_real (U : Utility) (hU0 : U.toFun 0 ≠ ⊥) : MonotoneOn U.real (Set.Ici 0)

theorem ProbabilityTheory.Utility.concaveOn_Ioi_real (U : Utility) : ConcaveOn ℝ (Set.Ioi 0) U.real

The utility function is concave on (0, ∞) when viewed as a real-valued function.

theorem ProbabilityTheory.Utility.concaveOn_Ici_real (U : Utility) (h0 : U.toFun 0 ≠ ⊥) : ConcaveOn ℝ (Set.Ici 0) U.real

The utility function is concave on [0, ∞) when viewed as a real-valued function.

noncomputable def ProbabilityTheory.Utility.deriv (U : Utility) (x : ENNReal) : EReal

The derivative of a utility function. At x ∈ (0, ∞), this is the derivative of the real-valued representation. At 0 or ∞, this is defined as a limit.

Equations

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

theorem ProbabilityTheory.Utility.deriv_nonneg (U : Utility) {x : ENNReal} (hx0 : x ≠ 0) (hx_top : x ≠ ⊤) : 0 ≤ U.deriv x

theorem ProbabilityTheory.Utility.le_add_deriv_mul (U : Utility) {x y : ENNReal} (hx_top : x ≠ ⊤) (hy_zero : y ≠ 0) (hy_top : y ≠ ⊤) : U.toFun x ≤ U.toFun y + U.deriv y * (↑x - ↑y)

theorem ProbabilityTheory.Utility.eintegral_le_map {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (U : Utility) {X : α → ENNReal} (hX_meas : AEMeasurable X μ) : ∫ᵉ (x : α), U.toFun (X x) ∂μ ≤ U.toFun (∫⁻ (x : α), X x ∂μ)

Jensen's inequality.

noncomputable def ProbabilityTheory.logUtility : Utility

The logarithmic utility function.

Equations

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

@[simp]

theorem ProbabilityTheory.logUtility_zero : logUtility.toFun 0 = ⊥

@[simp]

theorem ProbabilityTheory.logUtility_top : logUtility.toFun ⊤ = ⊤

@[simp]

theorem ProbabilityTheory.real_logUtility {x : ℝ} (hx : 0 < x) : logUtility.real x = Real.log x

theorem ProbabilityTheory.deriv_real_logUtility {x : ℝ} (hx : 0 < x) : deriv logUtility.real x = x⁻¹

theorem ProbabilityTheory.deriv_logUtility (x : ENNReal) : logUtility.deriv x = ↑(if x = 0 then ⊤ else 1 / x)

theorem ProbabilityTheory.deriv_logUtility_eq_ennreal (x : ENNReal) : logUtility.deriv x = ↑(1 / x)