Existence of the Numeraire

theorem ProbabilityTheory.komlos_ennreal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : ℕ → Ω → ENNReal} (hX : ∀ (n : ℕ), Measurable (X n)) (P : MeasureTheory.Measure Ω) [MeasureTheory.SFinite P] : ∃ (Y : ℕ → Ω → ENNReal) (Y_lim : Ω → ENNReal), (∀ (n : ℕ), Y n ∈ (convexHull ENNReal) (Set.range fun (m : ℕ) => X (n + m))) ∧ Measurable Y_lim ∧ ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ℕ) => Y x ω) Filter.atTop (nhds (Y_lim ω))

theorem ProbabilityTheory.convex_eintegral_utility_ge {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {U : ENNReal → EReal} [MeasureTheory.IsFiniteMeasure P] (u : EReal) (hU_ccv : ConcaveOn NNReal Set.univ U) (hU_meas : Measurable U) {B : EReal} (hU_le : ∀ (x : ENNReal), U x ≤ B) (hB : B ≠ ⊤) : Convex ENNReal {Z : 𝓧 → ENNReal | Measurable Z ∧ u ≤ ∫ᵉ (ω : 𝓧), U (Z ω) ∂P}

theorem ProbabilityTheory.exists_eq_iSup_eintegral_of_le' {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : ENNReal → EReal} (hU_ccv : ConcaveOn NNReal Set.univ U) {B : ℝ} (hU_cont : Continuous U) (hU_le : ∀ (x : ENNReal), U x ≤ ↑B) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] (S : Set (MeasureTheory.Measure 𝓧)) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : ∃ (Y : 𝓧 → ENNReal), IsEVar Y S ∧ ∀ (X : 𝓧 → ENNReal), IsEVar X S → ∫ᵉ (x : 𝓧), U (X x) ∂P ≤ ∫ᵉ (x : 𝓧), U (Y x) ∂P

There exists a utility-maximizing e-variable which is infinite whenever another e-variable is infinite.

theorem ProbabilityTheory.exists_eq_iSup_eintegral_of_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : ENNReal → EReal} (hU_ccv : ConcaveOn NNReal Set.univ U) {b : ℝ} (hU_cont : Continuous U) (hU_mono : Monotone U) (hU_le : ∀ (x : ENNReal), U x ≤ ↑b) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] (S : Set (MeasureTheory.Measure 𝓧)) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : ∃ (Y : 𝓧 → ENNReal), IsEVar Y S ∧ ∀ (X : 𝓧 → ENNReal), IsEVar X S → ∫ᵉ (x : 𝓧), U (X x) ∂P ≤ ∫ᵉ (x : 𝓧), U (Y x) ∂P ∧ ∀ᵐ (x : 𝓧) ∂P, Y x < ⊤ → X x < ⊤

There exists a utility-maximizing e-variable which is infinite whenever another e-variable is infinite.

noncomputable def ProbabilityTheory.numeraireOfBounded {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : 𝓧 → ENNReal

The numeraire associated with a bounded utility function.

Equations

• ProbabilityTheory.numeraireOfBounded hU_le P hS = ⋯.choose

theorem ProbabilityTheory.isEVar_numeraireOfBounded {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : IsEVar (numeraireOfBounded hU_le P hS) S

theorem ProbabilityTheory.eintegral_le_numeraireOfBounded {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} (hX_evar : IsEVar X S) : ∫ᵉ (x : 𝓧), U.toFun (X x) ∂P ≤ ∫ᵉ (x : 𝓧), U.toFun (numeraireOfBounded hU_le P hS x) ∂P

theorem ProbabilityTheory.eintegral_numeraireOfBounded_ge {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : U.toFun 1 * ↑(P Set.univ) ≤ ∫ᵉ (x : 𝓧), U.toFun (numeraireOfBounded hU_le P hS x) ∂P

theorem ProbabilityTheory.eintegral_numeraireOfBounded_ne_bot {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : ∫ᵉ (x : 𝓧), U.toFun (numeraireOfBounded hU_le P hS x) ∂P ≠ ⊥

theorem ProbabilityTheory.eintegrable_utility_numeraireOfBounded {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : MeasureTheory.EIntegrable (fun (x : 𝓧) => U.toFun (numeraireOfBounded hU_le P hS x)) P

theorem ProbabilityTheory.lt_top_of_numeraireOfBounded_lt_top {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {U : Utility} {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} (hX_evar : IsEVar X S) : ∀ᵐ (x : 𝓧) ∂P, numeraireOfBounded hU_le P hS x < ⊤ → X x < ⊤

@[implicit_reducible]

noncomputable instance ProbabilityTheory.inst_smul_I_ENNReal : SMul (↑unitInterval) ENNReal

Equations

• ProbabilityTheory.inst_smul_I_ENNReal = { smul := fun (a : ↑unitInterval) (x : ENNReal) => ENNReal.ofReal ↑a * x }

@[simp]

theorem ProbabilityTheory.smul_I_ENNReal (a : ↑unitInterval) (x : ENNReal) : a • x = ENNReal.ofReal ↑a * x

instance ProbabilityTheory.instMeasurableConstSMulElemRealUnitIntervalENNReal_eValues : MeasurableConstSMul (↑unitInterval) ENNReal

theorem ProbabilityTheory.eintegral_deriv_mul_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (U : Utility) {b : ℝ} (hU_le : ∀ (x : ENNReal), U.toFun x ≤ ↑b) (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] (S : Set (MeasureTheory.Measure 𝓧)) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {Y : 𝓧 → ENNReal} (hY : IsEVar Y S) : ∫ᵉ (x : 𝓧), U.deriv (numeraireOfBounded hU_le P hS x) * (↑(Y x) - ↑(numeraireOfBounded hU_le P hS x)) ∂P ≤ 0

theorem ProbabilityTheory.eintegral_deriv_log_mul_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : ∃ (Y : 𝓧 → ENNReal), IsEVar Y S ∧ ∀ (X : 𝓧 → ENNReal), IsEVar X S → ∫ᵉ (x : 𝓧), logUtility.deriv (Y x) * (↑(X x) - ↑(Y x)) ∂P ≤ 0

theorem ProbabilityTheory.exists_numeraire' {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] (S : Set (MeasureTheory.Measure 𝓧)) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : ∃ (Y : 𝓧 → ENNReal), IsEVar Y S ∧ ∀ (X : 𝓧 → ENNReal), IsEVar X S → ∫ᵉ (x : 𝓧), ↑(X x / Y x) - ↑(Y x / Y x) ∂P ≤ 0

theorem ProbabilityTheory.exists_numeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] (S : Set (MeasureTheory.Measure 𝓧)) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : ∃ (Y : 𝓧 → ENNReal), IsEVar Y S ∧ ∀ (X : 𝓧 → ENNReal), IsEVar X S → ∫⁻ (x : 𝓧), X x / Y x ∂P ≤ ∫⁻ (x : 𝓧), Y x / Y x ∂P

noncomputable def ProbabilityTheory.numeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) : 𝓧 → ENNReal

The numeraire e-variable.

Equations

• ProbabilityTheory.numeraire P S = if x : MeasureTheory.IsFiniteMeasure P then if hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ then ⋯.choose else 1 else 1

theorem ProbabilityTheory.isEVar_numeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) : IsEVar (numeraire P S) S

theorem ProbabilityTheory.measurable_numeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) : Measurable (numeraire P S)

theorem ProbabilityTheory.lintegral_div_numeraire_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} (hX_evar : IsEVar X S) : ∫⁻ (x : 𝓧), X x / numeraire P S x ∂P ≤ ∫⁻ (x : 𝓧), numeraire P S x / numeraire P S x ∂P

theorem ProbabilityTheory.lintegral_div_numeraire_le_measure_fsupport {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} (hX_evar : IsEVar X S) : ∫⁻ (x : 𝓧), X x / numeraire P S x ∂P ≤ P (Function.fsupport (numeraire P S))

theorem ProbabilityTheory.lintegral_div_numeraire_le_measure_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} (hX_evar : IsEVar X S) : ∫⁻ (x : 𝓧), X x / numeraire P S x ∂P ≤ P Set.univ

theorem ProbabilityTheory.lintegral_div_numeraire_le_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsProbabilityMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} (hX_evar : IsEVar X S) : ∫⁻ (x : 𝓧), X x / numeraire P S x ∂P ≤ 1

theorem ProbabilityTheory.isNumeraire_numeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : IsNumeraire (numeraire P S) S P

The canonical numeraire numeraire P S is indeed a numeraire for S and P.

theorem ProbabilityTheory.IsNumeraire.ae_eq_numeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} (hX : IsNumeraire X S P) : X =ᵐ[P] numeraire P S

theorem ProbabilityTheory.neBotUtilityEVar_numeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : NeBotUtilityEVar (numeraire P S) P S logUtility

theorem ProbabilityTheory.eintegrable_log_numeraire {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : MeasureTheory.EIntegrable (fun (x : 𝓧) => (numeraire P S x).log) P