Expectations in [−∞, ∞]

This file develops the integral eIntegral μ g of a function g with values in [−∞, ∞], the integral of its positive part minus the integral of its negative part. It is the expectation of Section S1 of the paper whenever one of the two parts is integrable.

• eIntegral_congr_ae, eIntegral_mono_ae, eIntegral_const, and eIntegral_nonneg_of_ae: the integral is invariant under μ-almost sure equality, monotone, and equal to c for the constant c under a probability measure;
• eIntegral_coe: for an integrable real function, eIntegral is the Bochner integral;
• integrable_ereal_toReal, eIntegral_eq_integral_toReal: a function with integrable positive and negative parts is finite almost everywhere, and eIntegral is the Bochner integral of its real part;
• eIntegral_coe_add: E(r + g) = E(r) + E(g) for an integrable real function r;
• eIntegral_neg: E(−g) = −E(g) when the positive part or the negative part of g is integrable;
• eIntegral_log_le_log_lintegral: Jensen's inequality for the logarithm, E(log f) ≤ log E(f) under a probability measure, from the tangent line log x ≤ x − 1.

Positive and negative parts in [−∞, ∞]

theorem LogOptimal.toENNReal_sub_toENNReal_neg (x : EReal) : ↑x.toENNReal - ↑(-x).toENNReal = x

theorem LogOptimal.toENNReal_coe_add_add (x : ℝ) (y : EReal) : (↑x + y).toENNReal + (-↑x).toENNReal + (-y).toENNReal = (-(↑x + y)).toENNReal + (↑x).toENNReal + y.toENNReal

The positive and negative parts of x + y, x, and y, for a real x, satisfy (x + y)⁺ + x⁻ + y⁻ = (x + y)⁻ + x⁺ + y⁺ in [0, ∞].

theorem LogOptimal.coe_sub_coe_eq_of_add_eq {a b p n u v : ENNReal} (hp : p ≠ ⊤) (hn : n ≠ ⊤) (h : a + n + v = b + p + u) (ha : a ≤ p + u) (hb : b ≤ n + v) (hv : v ≤ b + p) : ↑a - ↑b = ↑p - ↑n + (↑u - ↑v)

An identity in [0, ∞] between the integrals a, b of the positive and negative parts of r + g, p, n of those of r, and u, v of those of g gives a − b = (p − n) + (u − v) in [−∞, ∞], when p and n are finite.

theorem LogOptimal.toENNReal_log_le (y : ENNReal) : y.log.toENNReal ≤ y

The positive part of log y is at most y, since log y ≤ y − 1.

theorem LogOptimal.enorm_toReal_le (x : EReal) : ‖x.toReal‖ₑ ≤ x.toENNReal + (-x).toENNReal

The absolute value of the real part of x ∈ [−∞, ∞] is at most x⁺ + x⁻.

Basic properties of eIntegral

theorem LogOptimal.eIntegral_congr_ae {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {g h : Ω → EReal} (hgh : g =ᵐ[μ] h) : eIntegral μ g = eIntegral μ h

theorem LogOptimal.eIntegral_mono_ae {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {g h : Ω → EReal} (hgh : g ≤ᵐ[μ] h) : eIntegral μ g ≤ eIntegral μ h

theorem LogOptimal.eIntegral_const {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (c : EReal) : (eIntegral μ fun (x : Ω) => c) = c

theorem LogOptimal.eIntegral_nonneg_of_ae {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {g : Ω → EReal} (hg : ∀ᵐ (ω : Ω) ∂μ, 0 ≤ g ω) : 0 ≤ eIntegral μ g

theorem LogOptimal.eIntegral_coe {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {r : Ω → ℝ} (hr : MeasureTheory.Integrable r μ) : (eIntegral μ fun (ω : Ω) => ↑(r ω)) = ↑(∫ (ω : Ω), r ω ∂μ)

theorem LogOptimal.integrable_ereal_toReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {g : Ω → EReal} (hg : AEMeasurable g μ) (h₁ : ∫⁻ (ω : Ω), (g ω).toENNReal ∂μ ≠ ⊤) (h₂ : ∫⁻ (ω : Ω), (-g ω).toENNReal ∂μ ≠ ⊤) : MeasureTheory.Integrable (fun (ω : Ω) => (g ω).toReal) μ

A function with values in [−∞, ∞] with integrable positive and negative parts has an integrable real part.

theorem LogOptimal.eIntegral_eq_integral_toReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {g : Ω → EReal} (hg : AEMeasurable g μ) (h₁ : ∫⁻ (ω : Ω), (g ω).toENNReal ∂μ ≠ ⊤) (h₂ : ∫⁻ (ω : Ω), (-g ω).toENNReal ∂μ ≠ ⊤) : (∀ᵐ (ω : Ω) ∂μ, g ω ≠ ⊥ ∧ g ω ≠ ⊤) ∧ eIntegral μ g = ↑(∫ (ω : Ω), (g ω).toReal ∂μ)

A function with values in [−∞, ∞] with integrable positive and negative parts is finite almost everywhere, and eIntegral is the Bochner integral of its real part.

theorem LogOptimal.eIntegral_coe_add {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {r : Ω → ℝ} (hr : MeasureTheory.Integrable r μ) {g : Ω → EReal} (hg : AEMeasurable g μ) : (eIntegral μ fun (ω : Ω) => ↑(r ω) + g ω) = ↑(∫ (ω : Ω), r ω ∂μ) + eIntegral μ g

theorem LogOptimal.eIntegral_neg {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {g : Ω → EReal} (hg : ∫⁻ (ω : Ω), (g ω).toENNReal ∂μ ≠ ⊤ ∨ ∫⁻ (ω : Ω), (-g ω).toENNReal ∂μ ≠ ⊤) : (eIntegral μ fun (ω : Ω) => -g ω) = -eIntegral μ g

Jensen's inequality for the logarithm

theorem LogOptimal.toENNReal_log_add_one_le (y : ENNReal) : y.log.toENNReal + 1 ≤ y + (-y.log).toENNReal

The tangent line log x ≤ x − 1 in [0, ∞], written with positive and negative parts: (log y)⁺ + 1 ≤ y + (log y)⁻.

theorem LogOptimal.eIntegral_log_nonpos {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ENNReal} (hf : AEMeasurable f μ) (h : ∫⁻ (ω : Ω), f ω ∂μ ≤ 1) : (eIntegral μ fun (ω : Ω) => (f ω).log) ≤ 0

theorem LogOptimal.eIntegral_log_le_log_lintegral {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ENNReal} (hf : AEMeasurable f μ) : (eIntegral μ fun (ω : Ω) => (f ω).log) ≤ (∫⁻ (ω : Ω), f ω ∂μ).log

Jensen's inequality for the logarithm: E(log f) ≤ log E(f) under a probability measure, for a function f with values in [0, ∞]. It follows from the tangent line log x ≤ x − 1 applied to f/E(f).