Numeraire E-variables

This file defines numeraire e-variables, which are e-variables that maximize the expected logarithmic utility among all e-variables in a given set.

Main definitions

• IsNumeraire X S μ: A random variable X is the numeraire for a set of measures S and a measure μ if it is an e-variable for S and the expectation of the ratio of any e-variable Y over X is at most the measure of the finite support of X under μ.

Main statements

• ae_unique: The numeraire is almost-everywhere unique under finite measures.
• eintegral_log_div_nonpos: A numeraire is log-optimal: the expected log of the ratio of any e-variable to the numeraire is non-positive.
• eintegral_log_le: A numeraire maximizes the expected logarithm among all e-variables.
• eintegrable_log: The logarithm of the numeraire is e-integrable.

Implementation notes

The numeraire optimality is characterized through two equivalent perspectives:

• Direct definition: ∫⁻ ω, Y ω / X ω ∂μ ≤ μ X.fsupport for all e-variables Y
• Log-optimality: ∫ᵉ ω, log(Y ω / X ω) ∂μ ≤ 0 for all e-variables Y

theorem ProbabilityTheory.measure_fsupport_eq_zero_of_ae_eq_top {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {X : 𝓧 → ENNReal} (hX_top : ∀ᵐ (ω : 𝓧) ∂μ, X ω = ⊤) : μ (Function.fsupport X) = 0

theorem ProbabilityTheory.lintegral_div_self_eq_measure_fsupport {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {Y : 𝓧 → ENNReal} (hY : Measurable Y) {P : MeasureTheory.Measure 𝓧} : ∫⁻ (ω : 𝓧), Y ω / Y ω ∂P = P (Function.fsupport Y)

The integral of Y / Y equals the measure of the finite support of Y.

structure ProbabilityTheory.IsNumeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (X : 𝓧 → ENNReal) (S : Set (MeasureTheory.Measure 𝓧)) (μ : MeasureTheory.Measure 𝓧) extends ProbabilityTheory.IsEVar X S : Prop

A random variable X is the numeraire for a set of measures S and a measure μ if it is an e-variable for S and the expectation of the ratio of any e-variable Y over X is at most the measure under μ of the finite support of X.

• measurable : Measurable X
• eintegral_ne_bot (μ : MeasureTheory.Measure 𝓧) : μ ∈ S → ∫ᵉ (ω : 𝓧), ↑(X ω) - 1 ∂μ ≠ ⊥
• eintegral_nonpos (μ : MeasureTheory.Measure 𝓧) : μ ∈ S → ∫ᵉ (ω : 𝓧), ↑(X ω) - 1 ∂μ ≤ 0
• lintegral_div_le_measure_fsupport ⦃Y : 𝓧 → ENNReal⦄ : IsEVar Y S → ∫⁻ (ω : 𝓧), Y ω / X ω ∂μ ≤ μ (Function.fsupport X)

theorem ProbabilityTheory.lintegral_div_self_le_iff_IsNumeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {Y : 𝓧 → ENNReal} (hY_evar : IsEVar Y S) : (∀ (X : 𝓧 → ENNReal), IsEVar X S → ∫⁻ (ω : 𝓧), X ω / Y ω ∂P ≤ ∫⁻ (ω : 𝓧), Y ω / Y ω ∂P) ↔ IsNumeraire Y S P

For a given e-variable Y, the property of being a numeraire is equivalent to the property that the expectation of the ratio of any e-variable X over Y is less than the expectation of the ratio of Y over itself.

theorem ProbabilityTheory.IsNumeraire.smul {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (hX : IsNumeraire X S μ) (c : ENNReal) : IsNumeraire X S (c • μ)

theorem ProbabilityTheory.IsNumeraire.lintegral_inv_le_measure_fsupport {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (hX : IsNumeraire X S μ) : ∫⁻ (ω : 𝓧), (X ω)⁻¹ ∂μ ≤ μ (Function.fsupport X)

theorem ProbabilityTheory.IsNumeraire.lintegral_div_le_measure_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫⁻ (ω : 𝓧), Y ω / X ω ∂μ ≤ μ Set.univ

theorem ProbabilityTheory.IsNumeraire.lintegral_div_le_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫⁻ (ω : 𝓧), Y ω / X ω ∂μ ≤ 1

theorem ProbabilityTheory.IsNumeraire.ae_pos {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) : ∀ᵐ (ω : 𝓧) ∂μ, 0 < X ω

theorem ProbabilityTheory.IsNumeraire.ae_ne_zero {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) : ∀ᵐ (ω : 𝓧) ∂μ, X ω ≠ 0

theorem ProbabilityTheory.isNumeraire_of_isEmpty {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {f : 𝓧 → ENNReal} (hf : Measurable f) (hf_top : ∀ᵐ (x : 𝓧) ∂μ, f x = ⊤) (hS : IsEmpty ↑S) : IsNumeraire f S μ

theorem ProbabilityTheory.IsNumeraire.lintegral_eq_setLIntegral_fsupport {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫⁻ (ω : 𝓧), Y ω / X ω ∂μ = ∫⁻ (ω : 𝓧) in Function.fsupport X, Y ω / X ω ∂μ

theorem ProbabilityTheory.IsNumeraire.ae_top_implies_numeraire_top {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∀ᵐ (ω : 𝓧) ∂μ, Y ω = ⊤ → X ω = ⊤

If an e-variable Y is ae-infinite at a point, then the numeraire X must also be ae-infinite.

theorem ProbabilityTheory.IsNumeraire.lintegral_eq_setLIntegral_fsupport' {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫⁻ (ω : 𝓧), Y ω / X ω ∂μ = ∫⁻ (ω : 𝓧) in Function.fsupport Y, Y ω / X ω ∂μ

theorem ProbabilityTheory.IsNumeraire.measure_fsupport_ne_zero_or_ae_top {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) : μ (Function.fsupport X) ≠ 0 ∨ X =ᵐ[μ] fun (x : 𝓧) => ⊤

theorem ProbabilityTheory.IsNumeraire.measure_fsupport_eq_measure_fsupport {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsNumeraire Y S μ) : μ (Function.fsupport X) = μ (Function.fsupport Y)

Two numeraires have equal finite support measures.

theorem ProbabilityTheory.IsNumeraire.setLIntegral_fsupport_inv_le_measure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsNumeraire Y S μ) : ∫⁻ (ω : 𝓧) in Function.fsupport X, (Y ω / X ω)⁻¹ ∂μ ≤ μ (Function.fsupport X)

theorem ProbabilityTheory.IsNumeraire.measure_fsupport_mul_inv_lintegral_div_eq_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsNumeraire Y S μ) (h : μ (Function.fsupport X) ≠ 0) : μ (Function.fsupport X) * (∫⁻ (ω : 𝓧) in Function.fsupport X, Y ω / X ω ∂μ)⁻¹ = 1

theorem ProbabilityTheory.IsNumeraire.inv_measure_fsupport_mul_lintegral_div_eq_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsNumeraire Y S μ) (h : μ (Function.fsupport X) ≠ 0) : (μ (Function.fsupport X))⁻¹ * ∫⁻ (ω : 𝓧) in Function.fsupport X, Y ω / X ω ∂μ = 1

theorem ProbabilityTheory.IsNumeraire.ae_unique {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsNumeraire Y S μ) : X =ᵐ[μ] Y

Uniqueness Theorem: The numeraire is almost-everywhere unique under finite measures.

theorem ProbabilityTheory.IsNumeraire.congr {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (hX : IsNumeraire X S μ) (hY_evar : IsEVar Y S) (hY : Y =ᵐ[μ] X) : IsNumeraire Y S μ

theorem ProbabilityTheory.IsNumeraire.eintegral_log_div_nonpos {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫ᵉ (ω : 𝓧), (Y ω / X ω).log ∂μ ≤ 0

A Numeraire is log-optimal.

theorem ProbabilityTheory.IsNumeraire.eintegral_log_div_nonpos' {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫ᵉ (ω : 𝓧), (Y ω / X ω).log ∂μ ≤ 0

A Numeraire is log-optimal.

theorem ProbabilityTheory.IsNumeraire.eintegral_eq_setEIntegral_of_eq_zero {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {f : 𝓧 → EReal} {s : Set 𝓧} (hs : MeasurableSet s) (h_zero : ∀ᵐ (ω : 𝓧) ∂μ, ω ∈ sᶜ → f ω = 0) : ∫ᵉ (ω : 𝓧), f ω ∂μ = ∫ᵉ (ω : 𝓧) in s, f ω ∂μ

theorem ProbabilityTheory.IsNumeraire.eintegral_div_le_measure_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫ᵉ (ω : 𝓧), ↑(Y ω) / ↑(X ω) ∂μ ≤ ↑(μ Set.univ)

theorem ProbabilityTheory.IsNumeraire.eintegral_div_le_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫ᵉ (ω : 𝓧), ↑(Y ω) / ↑(X ω) ∂μ ≤ 1

theorem ProbabilityTheory.IsNumeraire.setEIntegral_le_eintegral_of_nonneg {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {f : 𝓧 → EReal} (hf_nonneg : ∀ (ω : 𝓧), 0 ≤ f ω) (s : Set 𝓧) : ∫ᵉ (ω : 𝓧) in s, f ω ∂μ ≤ ∫ᵉ (ω : 𝓧), f ω ∂μ

theorem ProbabilityTheory.IsNumeraire.setEIntegral_le_eintegral_of_ae_nonneg {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {f : 𝓧 → EReal} (hf_meas : AEMeasurable f μ) (hf_nonneg : ∀ᵐ (ω : 𝓧) ∂μ, 0 ≤ f ω) (s : Set 𝓧) : ∫ᵉ (ω : 𝓧) in s, f ω ∂μ ≤ ∫ᵉ (ω : 𝓧), f ω ∂μ

theorem ProbabilityTheory.IsNumeraire.eintegral_sub_div_le_measure_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫ᵉ (ω : 𝓧), (↑(Y ω) - ↑(X ω)) / ↑(X ω) ∂μ ≤ ↑(μ Set.univ)

theorem ProbabilityTheory.IsNumeraire.eintegral_sub_div_le_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫ᵉ (ω : 𝓧), (↑(Y ω) - ↑(X ω)) / ↑(X ω) ∂μ ≤ 1

theorem ProbabilityTheory.IsNumeraire.eintegral_log_ge_neg_measure_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) : -↑(μ Set.univ) ≤ ∫ᵉ (ω : 𝓧), (X ω).log ∂μ

theorem ProbabilityTheory.IsNumeraire.eintegral_log_ge_neg_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure μ] (hX : IsNumeraire X S μ) : -1 ≤ ∫ᵉ (ω : 𝓧), (X ω).log ∂μ

theorem ProbabilityTheory.IsNumeraire.eintegral_log_ne_bot {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) : ∫ᵉ (ω : 𝓧), (X ω).log ∂μ ≠ ⊥

theorem ProbabilityTheory.IsNumeraire.neBotUtilityEVar {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) : NeBotUtilityEVar X μ S logUtility

theorem ProbabilityTheory.IsNumeraire.eintegrable_log {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) : MeasureTheory.EIntegrable (fun (ω : 𝓧) => (X ω).log) μ

The logarithm of the numeraire is integrable.

theorem ProbabilityTheory.IsNumeraire.eintegral_log_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) (hY : IsEVar Y S) : ∫ᵉ (ω : 𝓧), (Y ω).log ∂μ ≤ ∫ᵉ (ω : 𝓧), (X ω).log ∂μ

A Numeraire maximizes the integral of the logarithm.

theorem ProbabilityTheory.IsNumeraire.eintegral_log_nonneg {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {μ : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure μ] (hX : IsNumeraire X S μ) : 0 ≤ ∫ᵉ (ω : 𝓧), (X ω).log ∂μ