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.
• harmonicTrunc: The harmonic truncation harmonicTrunc n x = n x / (n + x).
• boundedLogUtility: Bounded approximations x ↦ log (N x / (N + x)) of the logarithmic utility function, and harmonicDeriv, their derivative in ℝ≥0∞ form.

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).
• Utility.antitone_deriv, Utility.continuous_deriv: the derivative of a utility function is antitone and continuous on all of ℝ≥0∞, including at 0 and at ∞.
• Utility.deriv_mul_sub_le_liminf: the difference quotients of a utility function along a segment are eventually at least the directional derivative.
• deriv_logUtility: The derivative of the logarithmic utility function.
• deriv_boundedLogUtility: The derivative of boundedLogUtility, in ℝ≥0∞ form.

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.differentiableAt_real (U : Utility) {x : ℝ} (hx : 0 < x) : DifferentiableAt ℝ U.real x

theorem ProbabilityTheory.Utility.deriv_real_nonneg (U : Utility) {x : ℝ} (hx : 0 < x) : 0 ≤ deriv U.real x

theorem ProbabilityTheory.Utility.antitoneOn_deriv_real (U : Utility) : AntitoneOn (deriv U.real) (Set.Ioi 0)

theorem ProbabilityTheory.Utility.continuousOn_deriv_real (U : Utility) : ContinuousOn (deriv U.real) (Set.Ioi 0)

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

theorem ProbabilityTheory.Utility.deriv_zero_eq (U : Utility) : U.deriv 0 = Filter.limsup (fun (y : ENNReal) => ↑(deriv U.real y.toReal)) (nhdsWithin 0 (Set.Ioi 0))

theorem ProbabilityTheory.Utility.deriv_top_eq (U : Utility) : U.deriv ⊤ = Filter.limsup (fun (y : ENNReal) => ↑(deriv U.real y.toReal)) (nhdsWithin ⊤ (Set.Iio ⊤))

theorem ProbabilityTheory.Utility.deriv_nonneg (U : Utility) (x : ENNReal) : 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.deriv_top_le (U : Utility) {x : ENNReal} (hx0 : x ≠ 0) : U.deriv ⊤ ≤ U.deriv x

theorem ProbabilityTheory.Utility.deriv_le_deriv_zero (U : Utility) (x : ENNReal) : U.deriv x ≤ U.deriv 0

theorem ProbabilityTheory.Utility.antitone_deriv (U : Utility) : Antitone U.deriv

The derivative of a utility function is antitone on all of ℝ≥0∞, including at 0 and at ∞.

theorem ProbabilityTheory.Utility.tendsto_deriv_real_atTop (U : Utility) {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) : Filter.Tendsto (deriv U.real) Filter.atTop (nhds 0)

theorem ProbabilityTheory.Utility.tendsto_deriv (U : Utility) {α : ENNReal} (hα_top : α ≠ ⊤) {ι : Type u_1} {l : Filter ι} {z : ι → ENNReal} (hz : Filter.Tendsto z l (nhds α)) : Filter.Tendsto (fun (n : ι) => U.deriv (z n)) l (nhds (U.deriv α))

The derivative of a utility function is continuous at every α ≠ ∞: this is a continuity statement on (0, ∞) and a monotone limit statement at 0. See Utility.tendsto_deriv_top for the case α = ∞ and Utility.continuous_deriv for the combination of the two.

theorem ProbabilityTheory.Utility.tendsto_deriv_top (U : Utility) {ι : Type u_1} {l : Filter ι} {z : ι → ENNReal} (hz : Filter.Tendsto z l (nhds ⊤)) : Filter.Tendsto (fun (n : ι) => U.deriv (z n)) l (nhds (U.deriv ⊤))

The derivative of a utility function is continuous at ∞.

theorem ProbabilityTheory.Utility.continuous_deriv (U : Utility) : Continuous U.deriv

The derivative of a utility function is continuous on ℝ≥0∞, including at 0 and at ∞.

theorem ProbabilityTheory.Utility.measurable_deriv (U : Utility) : Measurable U.deriv

theorem ProbabilityTheory.Utility.deriv_top_eq_zero (U : Utility) {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) : U.deriv ⊤ = 0

theorem ProbabilityTheory.Utility.deriv_mul_sub_le (U : Utility) {α Z : ENNReal} (hα_top : α ≠ ⊤) (hZ0 : Z ≠ 0) (hZ_top : Z ≠ ⊤) : U.deriv Z * (↑Z - ↑α) ≤ U.toFun Z - U.toFun α

The first-order Taylor inequality, in the form of a lower bound on the increment of U.

theorem ProbabilityTheory.Utility.sub_le_inv_mul_sub (U : Utility) {α β : ENNReal} (hβ0 : β ≠ 0) {t : ℝ} (ht0 : 0 < t) (ht1 : t ≤ 1) : U.toFun β - U.toFun α ≤ (↑t)⁻¹ * (U.toFun (ENNReal.ofReal t * β + ENNReal.ofReal (1 - t) * α) - U.toFun α)

A convex combination inequality: the difference quotient of U along the segment from α to β is bounded below by U β - U α.

theorem ProbabilityTheory.Utility.sub_le_deriv_mul_sub (U : Utility) {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) {α β : ENNReal} (hα0 : α ≠ 0) (hαβ : α ≠ ⊤ → β ≠ ⊤) : U.toFun β - U.toFun α ≤ U.deriv α * (↑β - ↑α)

The increment of U is dominated by its first order Taylor approximation.

theorem ProbabilityTheory.Utility.deriv_mul_sub_convex (U : Utility) {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) {α β : ENNReal} (hαβ : α ≠ ⊤ → β ≠ ⊤) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) : U.deriv α * (↑(ENNReal.ofReal δ * 1 + ENNReal.ofReal (1 - δ) * β) - ↑α) = ↑(1 - δ) * (U.deriv α * (↑β - ↑α)) + ↑δ * (U.deriv α * (1 - ↑α))

The map y ↦ U.deriv α * (y - α) is affine: it turns a convex combination of 1 and β into the corresponding convex combination of its values.

theorem ProbabilityTheory.Utility.deriv_mul_sub_le_liminf (U : Utility) {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) {α β : ENNReal} (hβ0 : β ≠ 0) (hαβ : α ≠ ⊤ → β ≠ ⊤) {t : ℕ → ℝ} (ht0 : ∀ (n : ℕ), 0 < t n) (ht1 : ∀ (n : ℕ), t n < 1) (ht : Filter.Tendsto t Filter.atTop (nhds 0)) : U.deriv α * (↑β - ↑α) ≤ Filter.liminf (fun (n : ℕ) => (↑(t n))⁻¹ * (U.toFun (ENNReal.ofReal (t n) * β + ENNReal.ofReal (1 - t n) * α) - U.toFun α)) Filter.atTop

The key pointwise estimate for the first order optimality condition: along a sequence t n → 0, the difference quotients of U between α and β are eventually at least the directional derivative U.deriv α * (β - α).

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)

Bounded approximations of the logarithmic utility

We introduce the bounded approximations x ↦ log (n x / (n + x)) of the logarithm, obtained by composing the logarithm with the harmonic truncation harmonicTrunc n x = (x⁻¹ + n⁻¹)⁻¹.

noncomputable def ProbabilityTheory.harmonicTrunc (n x : ENNReal) : ENNReal

The harmonic truncation harmonicTrunc n x = n x / (n + x), written in a form that behaves well at 0 and ∞. It is concave, increasing, bounded above by n, and converges to x as n → ∞.

Equations

• ProbabilityTheory.harmonicTrunc n x = (x⁻¹ + n⁻¹)⁻¹

@[simp]

theorem ProbabilityTheory.harmonicTrunc_zero (n : ENNReal) : harmonicTrunc n 0 = 0

@[simp]

theorem ProbabilityTheory.harmonicTrunc_top (n : ENNReal) : harmonicTrunc n ⊤ = n

theorem ProbabilityTheory.harmonicTrunc_le_left (n x : ENNReal) : harmonicTrunc n x ≤ x

theorem ProbabilityTheory.harmonicTrunc_le_right (n x : ENNReal) : harmonicTrunc n x ≤ n

theorem ProbabilityTheory.harmonicTrunc_ne_zero {n x : ENNReal} (hn0 : n ≠ 0) (hx0 : x ≠ 0) : harmonicTrunc n x ≠ 0

theorem ProbabilityTheory.harmonicTrunc_ne_top {n : ENNReal} (hn_top : n ≠ ⊤) (x : ENNReal) : harmonicTrunc n x ≠ ⊤

theorem ProbabilityTheory.monotone_harmonicTrunc (n : ENNReal) : Monotone (harmonicTrunc n)

theorem ProbabilityTheory.continuous_harmonicTrunc (n : ENNReal) : Continuous (harmonicTrunc n)

theorem ProbabilityTheory.harmonicTrunc_ofReal {N x : ℝ} (hN : 0 < N) (hx : 0 < x) : harmonicTrunc (ENNReal.ofReal N) (ENNReal.ofReal x) = ENNReal.ofReal (x⁻¹ + N⁻¹)⁻¹

The harmonic truncation of a real number, computed in ℝ.

theorem ProbabilityTheory.toReal_harmonicTrunc {n x : ENNReal} (hn0 : n ≠ 0) (hx0 : x ≠ 0) : (harmonicTrunc n x).toReal = (x.toReal⁻¹ + n.toReal⁻¹)⁻¹

theorem ProbabilityTheory.harmonicTrunc_le_sq_add {n : ENNReal} (hn0 : n ≠ 0) (hn_top : n ≠ ⊤) (w : ENNReal) {s t : ENNReal} (hst : s + t = 1) : harmonicTrunc n w ≤ s ^ 2 * w + t ^ 2 * n

harmonicTrunc n is the pointwise infimum of the affine maps w ↦ s ^ 2 * w + t ^ 2 * n over s + t = 1: this is one half of that statement.

theorem ProbabilityTheory.exists_sq_add_le_harmonicTrunc {n : ENNReal} (hn0 : n ≠ 0) (hn_top : n ≠ ⊤) (z : ENNReal) : ∃ (s : ENNReal) (t : ENNReal), s + t = 1 ∧ s ^ 2 * z + t ^ 2 * n ≤ harmonicTrunc n z

The infimum in harmonicTrunc_le_sq_add is attained.

theorem ProbabilityTheory.concaveOn_harmonicTrunc {n : ENNReal} (hn0 : n ≠ 0) (hn_top : n ≠ ⊤) : ConcaveOn ENNReal Set.univ (harmonicTrunc n)

theorem ProbabilityTheory.concaveOn_log_harmonicTrunc' {n : ENNReal} (hn0 : n ≠ 0) (hn_top : n ≠ ⊤) : ConcaveOn ENNReal Set.univ fun (x : ENNReal) => (harmonicTrunc n x).log

theorem ProbabilityTheory.concaveOn_log_harmonicTrunc {n : ENNReal} (hn0 : n ≠ 0) (hn_top : n ≠ ⊤) : ConcaveOn NNReal Set.univ fun (x : ENNReal) => (harmonicTrunc n x).log

noncomputable def ProbabilityTheory.boundedLogUtility {N : ℝ} (hN : 0 < N) : Utility

Bounded approximation of the logarithmic utility at level N: boundedLogUtility hN x = log (N x / (N + x)).

Equations

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

theorem ProbabilityTheory.boundedLogUtility_apply {N : ℝ} (hN : 0 < N) (x : ENNReal) : (boundedLogUtility hN).toFun x = (harmonicTrunc (ENNReal.ofReal N) x).log

theorem ProbabilityTheory.boundedLogUtility_le {N : ℝ} (hN : 0 < N) (x : ENNReal) : (boundedLogUtility hN).toFun x ≤ ↑(Real.log N)

theorem ProbabilityTheory.boundedLogUtility_real {N : ℝ} (hN : 0 < N) {x : ℝ} (hx : 0 < x) : (boundedLogUtility hN).real x = Real.log x + Real.log N - Real.log (x + N)

theorem ProbabilityTheory.deriv_boundedLogUtility_real {N : ℝ} (hN : 0 < N) {x : ℝ} (hx : 0 < x) : deriv (boundedLogUtility hN).real x = x⁻¹ - (x + N)⁻¹

noncomputable def ProbabilityTheory.harmonicDeriv (N : ℝ) (y : ENNReal) : ENNReal

The derivative of boundedLogUtility hN, as an ℝ≥0∞-valued function.

Equations

• ProbabilityTheory.harmonicDeriv N y = y⁻¹ - (y + ENNReal.ofReal N)⁻¹

theorem ProbabilityTheory.harmonicDeriv_add_inv (N : ℝ) (y : ENNReal) : harmonicDeriv N y + (y + ENNReal.ofReal N)⁻¹ = y⁻¹

theorem ProbabilityTheory.inv_le_harmonicDeriv_add (N : ℝ) (y : ENNReal) : y⁻¹ ≤ harmonicDeriv N y + (ENNReal.ofReal N)⁻¹

@[simp]

theorem ProbabilityTheory.harmonicDeriv_top (N : ℝ) : harmonicDeriv N ⊤ = 0

theorem ProbabilityTheory.harmonicDeriv_le_inv (N : ℝ) (y : ENNReal) : harmonicDeriv N y ≤ y⁻¹

theorem ProbabilityTheory.harmonicDeriv_mul_le_one (N : ℝ) (y : ENNReal) : harmonicDeriv N y * y ≤ 1

theorem ProbabilityTheory.harmonicDeriv_eq_top_iff {N : ℝ} (hN : 0 < N) {y : ENNReal} : harmonicDeriv N y = ⊤ ↔ y = 0

theorem ProbabilityTheory.measurable_harmonicDeriv (N : ℝ) : Measurable (harmonicDeriv N)

theorem ProbabilityTheory.toReal_harmonicDeriv {N : ℝ} (hN : 0 < N) {y : ENNReal} (hy0 : y ≠ 0) (hy_top : y ≠ ⊤) : (harmonicDeriv N y).toReal = y.toReal⁻¹ - (y.toReal + N)⁻¹

theorem ProbabilityTheory.deriv_boundedLogUtility_zero {N : ℝ} (hN : 0 < N) : (boundedLogUtility hN).deriv 0 = ⊤

theorem ProbabilityTheory.deriv_boundedLogUtility {N : ℝ} (hN : 0 < N) (y : ENNReal) : (boundedLogUtility hN).deriv y = ↑(harmonicDeriv N y)

The derivative of the bounded logarithmic utility, in ℝ≥0∞ form.

theorem ProbabilityTheory.harmonicDeriv_ne_zero {N : ℝ} (hN : 0 < N) {y : ENNReal} (hy : y ≠ ⊤) : harmonicDeriv N y ≠ 0