E-variables

This file defines e-variables and randomized e-variables, which are fundamental objects in e-value theory.

Main definitions

• IsEVar X S: A random variable X is an e-variable for a set of measures S if it has expected value at most 1 under all measures in S.
• IsRandEVar κ S: A kernel κ is a randomized e-variable for S if its mean function is an e-variable.
• NeBotUtilityEVar X P S U: An e-variable X for which the composed utility integral is not ⊥.

Main statements

• isRandEVar_iff_isEVar: A kernel is a randomized e-variable iff its mean function is an e-variable.
• convex_isEVar: The set of e-variables is convex.
• IsEVar.mono: Monotonicity: if Y is an e-variable and X ≤ Y, then X is also an e-variable.
• IsRandEVar.mono: Monotonicity for randomized e-variables: if η is a randomized e-variable and κ ≤ η, then κ is also a randomized e-variable.

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

A random variable X is an e-variable for a set of measures S if it is measurable and its expectation is at most one for all measures in S. This is formulated via the condition that ∫ᵉ ω, X ω - 1 ∂μ ≤ 0 for all μ ∈ S.

• measurable : Measurable X
• eintegral_ne_bot (μ : MeasureTheory.Measure 𝓧) : μ ∈ S → ∫ᵉ (ω : 𝓧), ↑(X ω) - 1 ∂μ ≠ ⊥
• eintegral_nonpos (μ : MeasureTheory.Measure 𝓧) : μ ∈ S → ∫ᵉ (ω : 𝓧), ↑(X ω) - 1 ∂μ ≤ 0

theorem ProbabilityTheory.eintegral_sub_one_ne_bot_of_isFiniteMeasure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {μ : MeasureTheory.Measure 𝓧} (hμ : μ ∈ S) : ∫ᵉ (ω : 𝓧), ↑(X ω) - 1 ∂μ ≠ ⊥

theorem ProbabilityTheory.IsEVar.eintegrable_sub_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {X : 𝓧 → ENNReal} (hX : IsEVar X S) (μ : MeasureTheory.Measure 𝓧) (hμ : μ ∈ S) : MeasureTheory.EIntegrable (fun (ω : 𝓧) => ↑(X ω) - 1) μ

theorem ProbabilityTheory.IsEVar.lintegral_le_measure_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {X : 𝓧 → ENNReal} (hX : IsEVar X S) (μ : MeasureTheory.Measure 𝓧) (hμ : μ ∈ S) : ∫⁻ (ω : 𝓧), X ω ∂μ ≤ μ Set.univ

An e-variable has expected value at most the total measure.

theorem ProbabilityTheory.eintegral_sub_one_eq_lintegral_sub {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {X : 𝓧 → ENNReal} (hX : Measurable X) [MeasureTheory.IsFiniteMeasure μ] : ∫ᵉ (ω : 𝓧), ↑(X ω) - 1 ∂μ = ↑(∫⁻ (ω : 𝓧), X ω ∂μ) - ↑(μ Set.univ)

theorem ProbabilityTheory.eintegral_sub_one_nonpos_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {X : 𝓧 → ENNReal} (hX : Measurable X) [MeasureTheory.IsFiniteMeasure μ] : ∫ᵉ (ω : 𝓧), ↑(X ω) - 1 ∂μ ≤ 0 ↔ ∫⁻ (ω : 𝓧), X ω ∂μ ≤ μ Set.univ

theorem ProbabilityTheory.IsEVar.of_lintegral_le_measure_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} (hX_meas : Measurable X) (hX : ∀ μ ∈ S, ∫⁻ (ω : 𝓧), X ω ∂μ ≤ μ Set.univ) : IsEVar X S

theorem ProbabilityTheory.IsEVar.of_lintegral_le_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsProbabilityMeasure μ) {X : 𝓧 → ENNReal} (hX_meas : Measurable X) (hX : ∀ μ ∈ S, ∫⁻ (ω : 𝓧), X ω ∂μ ≤ 1) : IsEVar X S

structure ProbabilityTheory.IsRandEVar {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (κ : Kernel 𝓧 ENNReal) (S : Set (MeasureTheory.Measure 𝓧)) : Prop

A random variable X is a randomized e-variable for a set of measures S if it is a Markov kernel and its mean function is at most 1 under all measures in S.

• markov : IsMarkovKernel κ
• eintegral_ne_bot (μ : MeasureTheory.Measure 𝓧) : μ ∈ S → ∫ᵉ (ω : 𝓧), ↑(∫⁻ (x : ENNReal), x ∂κ ω) - 1 ∂μ ≠ ⊥
• eintegral_nonpos (μ : MeasureTheory.Measure 𝓧) : μ ∈ S → ∫ᵉ (ω : 𝓧), ↑(∫⁻ (x : ENNReal), x ∂κ ω) - 1 ∂μ ≤ 0

theorem ProbabilityTheory.IsRandEVar.lintegral_le_measure_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {κ : Kernel 𝓧 ENNReal} (hκ : IsRandEVar κ S) (μ : MeasureTheory.Measure 𝓧) (hμ : μ ∈ S) : ∫⁻ (ω : 𝓧), ∫⁻ (x : ENNReal), x ∂κ ω ∂μ ≤ μ Set.univ

theorem ProbabilityTheory.IsRandEVar.lintegral_le_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {κ : Kernel 𝓧 ENNReal} (hκ : IsRandEVar κ S) (μ : MeasureTheory.Measure 𝓧) (hμ : μ ∈ S) [MeasureTheory.IsProbabilityMeasure μ] : ∫⁻ (ω : 𝓧), ∫⁻ (x : ENNReal), x ∂κ ω ∂μ ≤ 1

theorem ProbabilityTheory.isRandEVar_iff_isEVar {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel 𝓧 ENNReal} [IsMarkovKernel κ] {S : Set (MeasureTheory.Measure 𝓧)} : IsRandEVar κ S ↔ IsEVar (fun (x : 𝓧) => ∫⁻ (y : ENNReal), y ∂κ x) S

A kernel κ is a randomized e-variable iff its mean function x ↦ ∫⁻ y, y ∂κ x is an e-variable.

theorem ProbabilityTheory.IsEVar.isRandEVar_deterministic {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {S : Set (MeasureTheory.Measure 𝓧)} (hX : IsEVar X S) : IsRandEVar (Kernel.deterministic X ⋯) S

@[simp]

theorem ProbabilityTheory.isEVar_empty {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} (hX : Measurable X) : IsEVar X ∅

theorem ProbabilityTheory.isEVar_zero {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : IsEVar 0 S

theorem ProbabilityTheory.isEVar_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (S : Set (MeasureTheory.Measure 𝓧)) : IsEVar 1 S

theorem ProbabilityTheory.isEVar_fun_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (S : Set (MeasureTheory.Measure 𝓧)) : IsEVar (fun (x : 𝓧) => 1) S

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

theorem ProbabilityTheory.IsEVar.ae_lt_top {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {S : Set (MeasureTheory.Measure 𝓧)} (hX : IsEVar X S) {μ : MeasureTheory.Measure 𝓧} (hμ : μ ∈ S) : ∀ᵐ (ω : 𝓧) ∂μ, X ω < ⊤

theorem ProbabilityTheory.IsEVar.ae_ne_top {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {S : Set (MeasureTheory.Measure 𝓧)} (hX : IsEVar X S) {μ : MeasureTheory.Measure 𝓧} (hμ : μ ∈ S) : ∀ᵐ (ω : 𝓧) ∂μ, X ω ≠ ⊤

theorem Measurable.measurable_fsupport {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} (hX : Measurable X) : MeasurableSet (Function.fsupport X)

theorem ProbabilityTheory.IsEVar.measurable_fsupport {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {S : Set (MeasureTheory.Measure 𝓧)} (hX : IsEVar X S) : MeasurableSet (Function.fsupport X)

theorem ProbabilityTheory.IsEVar.mono {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X Y : 𝓧 → ENNReal} {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (hY : IsEVar Y S) (hX : Measurable X) (hXY : X ≤ Y) : IsEVar X S

theorem ProbabilityTheory.IsRandEVar.mono {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {κ η : Kernel 𝓧 ENNReal} [IsMarkovKernel κ] {S : Set (MeasureTheory.Measure 𝓧)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (hη : IsRandEVar η S) (hκη : κ ≤ η) : IsRandEVar κ S

theorem ProbabilityTheory.IsEVar.anti_set {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {S T : Set (MeasureTheory.Measure 𝓧)} (hST : S ⊆ T) (hX : IsEVar X T) : IsEVar X S

theorem ProbabilityTheory.IsRandEVar.anti_set {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel 𝓧 ENNReal} [IsMarkovKernel κ] {S T : Set (MeasureTheory.Measure 𝓧)} (hST : S ⊆ T) (hκ : IsRandEVar κ T) : IsRandEVar κ S

theorem ProbabilityTheory.IsEVar.union {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {S T : Set (MeasureTheory.Measure 𝓧)} (hXS : IsEVar X S) (hXT : IsEVar X T) : IsEVar X (S ∪ T)

theorem ProbabilityTheory.isEVar_union_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {S T : Set (MeasureTheory.Measure 𝓧)} : IsEVar X (S ∪ T) ↔ IsEVar X S ∧ IsEVar X T

theorem ProbabilityTheory.IsEVar.comp {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {Y : 𝓨 → ENNReal} {S : Set (MeasureTheory.Measure 𝓧)} {φ : 𝓧 → 𝓨} (hφ : Measurable φ) (h : IsEVar Y {x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ S, MeasureTheory.Measure.map φ μ = x}) : IsEVar (Y ∘ φ) S

theorem ProbabilityTheory.IsRandEVar.comp {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ξ : Kernel 𝓨 ENNReal} {S : Set (MeasureTheory.Measure 𝓧)} {κ : Kernel 𝓧 𝓨} [IsMarkovKernel κ] (h : IsRandEVar ξ {x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ S, μ.bind ⇑κ = x}) : IsRandEVar (ξ.comp κ) S

theorem ProbabilityTheory.convex_isEVar {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (S : Set (MeasureTheory.Measure 𝓧)) : Convex ENNReal {Z : 𝓧 → ENNReal | IsEVar Z S}

The set of e-variables is convex.

structure ProbabilityTheory.NeBotUtilityEVar {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (X : 𝓧 → ENNReal) (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) (U : Utility) extends ProbabilityTheory.IsEVar X S : Prop

An e-variable for which the eintegral of the composition with a utility function is not ⊥.

• measurable : Measurable X
• eintegral_ne_bot (μ : MeasureTheory.Measure 𝓧) : μ ∈ S → ∫ᵉ (ω : 𝓧), ↑(X ω) - 1 ∂μ ≠ ⊥
• eintegral_nonpos (μ : MeasureTheory.Measure 𝓧) : μ ∈ S → ∫ᵉ (ω : 𝓧), ↑(X ω) - 1 ∂μ ≤ 0
• utility_ne_bot : ∫ᵉ (x : 𝓧), (U.toFun ∘ X) x ∂P ≠ ⊥

theorem ProbabilityTheory.NeBotUtilityEVar.eintegrable {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (X : 𝓧 → ENNReal) (P : MeasureTheory.Measure 𝓧) (S : Set (MeasureTheory.Measure 𝓧)) (U : Utility) (hX : NeBotUtilityEVar X P S U) : MeasureTheory.EIntegrable (U.toFun ∘ X) P

theorem ProbabilityTheory.IsEVar.neBotUtilityEVar_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {X : 𝓧 → ENNReal} {S : Set (MeasureTheory.Measure 𝓧)} (hX : IsEVar X S) {P : MeasureTheory.Measure 𝓧} {U : Utility} : NeBotUtilityEVar X P S U ↔ ∫ᵉ (x : 𝓧), (U.toFun ∘ X) x ∂P ≠ ⊥

theorem ProbabilityTheory.isEVar_liminf {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {X : ℕ → 𝓧 → ENNReal} (hX : ∀ (n : ℕ), IsEVar (X n) S) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : IsEVar (fun (ω : 𝓧) => Filter.liminf (fun (n : ℕ) => X n ω) Filter.atTop) S