Reverse Information Projection and duality

Main definitions

• KL: a version of the Kullback-Leibler divergence between two measures, which differ from the one in Mathlib (klDiv) in that it has only the integral term. It does not compensate for the case where the measures are not probability measures.
• MemEffectiveSet S μ: a measure μ is in the effective set of a set of measures S if the expectation under μ of every e-variable for S is at most 1.
• ripr P S: Reverse Information Projection of the measure P on the set S. It is defined as P.withDensity fun ω ↦ (numeraire P S ω)⁻¹. It minimizes the Kullback-Leibler divergence KL P μ among measures in the effective set of S.

Main statements

• maxUtility_eq_KL_ripr: if the numeraire is almost everywhere finite, then maxUtility P S logUtility = KL P (ripr P S).
• maxUtility_eq_iInf_KL_memEffectiveSet: if the numeraire is almost everywhere finite, then maxUtility P S logUtility = ⨅ (μ) (_hμ : MemEffectiveSet S μ), KL P μ. This is the duality between maximal logarithmic utility and minimal Kullback-Leibler divergence.

theorem MeasureTheory.lintegral_rnDeriv_mul_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P μ : Measure 𝓧} {X : 𝓧 → ENNReal} (hX : Measurable X) : ∫⁻ (ω : 𝓧), μ.rnDeriv P ω * X ω ∂P ≤ ∫⁻ (ω : 𝓧), X ω ∂μ

theorem eintegrable_rnDeriv_mul_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : 𝓧 → EReal} (hμν : μ.AbsolutelyContinuous ν) (hf : Measurable f) : MeasureTheory.EIntegrable (fun (a : 𝓧) => ↑(μ.rnDeriv ν a).toReal * f a) ν ↔ MeasureTheory.EIntegrable f μ

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

Reverse Information Projection.

Equations

• ProbabilityTheory.ripr P S = P.withDensity fun (ω : 𝓧) => (ProbabilityTheory.numeraire P S ω)⁻¹

theorem ProbabilityTheory.ripr_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) : (ripr P S) Set.univ = ∫⁻ (x : 𝓧), (numeraire P S x)⁻¹ ∂P

theorem ProbabilityTheory.ripr_univ_le_measure_fsupport {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : (ripr P S) Set.univ ≤ P (Function.fsupport (numeraire P S))

theorem ProbabilityTheory.ripr_univ_le_measure_univ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) : (ripr P S) Set.univ ≤ P Set.univ

theorem ProbabilityTheory.ripr_univ_le_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsProbabilityMeasure P] : (ripr P S) Set.univ ≤ 1

The reverse information projection is a sub-probability measure (its total mass is at most 1).

instance ProbabilityTheory.isFiniteMeasure_ripr {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] : MeasureTheory.IsFiniteMeasure (ripr P S)

theorem ProbabilityTheory.absolutelyContinuous_ripr_of_ae_ne_top {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (h_top : ∀ᵐ (x : 𝓧) ∂P, numeraire P S x ≠ ⊤) : P.AbsolutelyContinuous (ripr P S)

theorem ProbabilityTheory.rnDeriv_div_ripr {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (h_top : ∀ᵐ (x : 𝓧) ∂P, numeraire P S x ≠ ⊤) : P.rnDeriv (ripr P S) =ᵐ[P] numeraire P S

theorem ProbabilityTheory.llr_div_ripr {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (h_top : ∀ᵐ (x : 𝓧) ∂P, numeraire P S x ≠ ⊤) : MeasureTheory.llr P (ripr P S) =ᵐ[P] fun (x : 𝓧) => Real.log (numeraire P S x).toReal

theorem ProbabilityTheory.llr_div_ripr' {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (h_top : ∀ᵐ (x : 𝓧) ∂P, numeraire P S x ≠ ⊤) : MeasureTheory.llr P (ripr P S) =ᵐ[P] fun (x : 𝓧) => (numeraire P S x).log.toReal

noncomputable def ProbabilityTheory.KL {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν : MeasureTheory.Measure 𝓧) : EReal

A version of the Kullback-Leibler divergence between two measures. It takes value in EReal because it might be negative for non-probability measures.

Equations

• ProbabilityTheory.KL μ ν = if μ.AbsolutelyContinuous ν ∧ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ then ↑(∫ (x : 𝓧), MeasureTheory.llr μ ν x ∂μ) else ⊤

theorem ProbabilityTheory.eintegral_log_numeraire_eq_integral {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (h_top : ∀ᵐ (x : 𝓧) ∂P, numeraire P S x ≠ ⊤) (h_int : ∫ᵉ (x : 𝓧), (numeraire P S x).log ∂P ≠ ⊤) : ∫ᵉ (x : 𝓧), (numeraire P S x).log ∂P = ↑(∫ (x : 𝓧), Real.log (numeraire P S x).toReal ∂P)

theorem ProbabilityTheory.integrable_llr_div_ripr_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (h_top : ∀ᵐ (x : 𝓧) ∂P, numeraire P S x ≠ ⊤) : MeasureTheory.Integrable (MeasureTheory.llr P (ripr P S)) P ↔ ∫ᵉ (x : 𝓧), (numeraire P S x).log ∂P ≠ ⊤

theorem ProbabilityTheory.maxUtility_eq_KL_ripr {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsFiniteMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (h_top : ∀ᵐ (x : 𝓧) ∂P, numeraire P S x ≠ ⊤) : maxUtility P S logUtility = KL P (ripr P S)

def ProbabilityTheory.MemEffectiveSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (S : Set (MeasureTheory.Measure 𝓧)) (μ : MeasureTheory.Measure 𝓧) : Prop

A measure μ is in the effective set of a set of measures S if the expectation under μ of every e-variable for S is at most 1.

Equations

• ProbabilityTheory.MemEffectiveSet S μ = ∀ (X : 𝓧 → ENNReal), ProbabilityTheory.IsEVar X S → ∫⁻ (ω : 𝓧), X ω ∂μ ≤ 1

theorem ProbabilityTheory.MemEffectiveSet.measure_univ_le_one {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {μ : MeasureTheory.Measure 𝓧} (hμ : MemEffectiveSet S μ) : μ Set.univ ≤ 1

theorem ProbabilityTheory.MemEffectiveSet.isFiniteMeasure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {μ : MeasureTheory.Measure 𝓧} (hμ : MemEffectiveSet S μ) : MeasureTheory.IsFiniteMeasure μ

theorem ProbabilityTheory.memEffectiveSet_ripr {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsProbabilityMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : MemEffectiveSet S (ripr P S)

theorem ProbabilityTheory.lintegral_mul_le_of_memEffectiveSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} {μ : MeasureTheory.Measure 𝓧} (hμ : MemEffectiveSet S μ) {X : 𝓧 → ENNReal} (hX : IsEVar X S) : ∫⁻ (ω : 𝓧), X ω * μ.rnDeriv P ω ∂P ≤ 1

theorem ProbabilityTheory.eintegral_log_mul_nonpos_of_memEffectiveSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure P] {μ : MeasureTheory.Measure 𝓧} (hμ : MemEffectiveSet S μ) {X : 𝓧 → ENNReal} (hX : IsEVar X S) : ∫ᵉ (ω : 𝓧), (X ω * μ.rnDeriv P ω).log ∂P ≤ 0

theorem ProbabilityTheory.llr_ae_eq_log_inv_rnDeriv {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure P] {μ : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] (h_ac : P.AbsolutelyContinuous μ) : MeasureTheory.llr P μ =ᵐ[P] fun (x : 𝓧) => Real.log ((μ.rnDeriv P)⁻¹ x).toReal

theorem ProbabilityTheory.eintegrable_klFun_rnDeriv {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (P μ : MeasureTheory.Measure 𝓧) : MeasureTheory.EIntegrable (fun (ω : 𝓧) => ↑(InformationTheory.klFun (μ.rnDeriv P ω).toReal)) P

theorem ProbabilityTheory.eintegrable_rnDeriv_mul_log_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) : MeasureTheory.EIntegrable (fun (a : 𝓧) => ↑(μ.rnDeriv ν a).toReal * ↑(Real.log (μ.rnDeriv ν a).toReal)) ν ↔ MeasureTheory.EIntegrable (fun (a : 𝓧) => ↑(MeasureTheory.llr μ ν a)) μ

theorem ProbabilityTheory.eintegrable_llr {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure P] {μ : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] (h_ac : P.AbsolutelyContinuous μ) : MeasureTheory.EIntegrable (fun (ω : 𝓧) => ↑(MeasureTheory.llr P μ ω)) P

theorem ProbabilityTheory.eintegrable_ennreal_log_rnDeriv {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure P] {μ : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] (h_ac : P.AbsolutelyContinuous μ) : MeasureTheory.EIntegrable (fun (ω : 𝓧) => ((μ.rnDeriv P)⁻¹ ω).log) P

theorem ProbabilityTheory.eintegral_log_isEVar_le_eintegral_rnDeriv {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure P] {μ : MeasureTheory.Measure 𝓧} (hμ : MemEffectiveSet S μ) [MeasureTheory.IsFiniteMeasure μ] (h_ac : P.AbsolutelyContinuous μ) {X : 𝓧 → ENNReal} (hX : IsEVar X S) : ∫ᵉ (ω : 𝓧), (X ω).log ∂P ≤ ∫ᵉ (ω : 𝓧), ((μ.rnDeriv P)⁻¹ ω).log ∂P

theorem ProbabilityTheory.KL_eq_eintegral_log_inv_rnDeriv {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P μ : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure μ] (h_ac : P.AbsolutelyContinuous μ) (h_int : MeasureTheory.Integrable (MeasureTheory.llr P μ) P) : KL P μ = ∫ᵉ (x : 𝓧), ((μ.rnDeriv P)⁻¹ x).log ∂P

theorem ProbabilityTheory.maxUtility_le_KL_of_memEffectiveSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) {μ : MeasureTheory.Measure 𝓧} (hμ : MemEffectiveSet S μ) : maxUtility P S logUtility ≤ KL P μ

theorem ProbabilityTheory.maxUtility_le_iInf_KL_memEffectiveSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) : maxUtility P S logUtility ≤ ⨅ (μ : MeasureTheory.Measure 𝓧), ⨅ (_ : MemEffectiveSet S μ), KL P μ

theorem ProbabilityTheory.maxUtility_eq_iInf_KL_memEffectiveSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {P : MeasureTheory.Measure 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [MeasureTheory.IsProbabilityMeasure P] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (h_top : ∀ᵐ (x : 𝓧) ∂P, numeraire P S x ≠ ⊤) : maxUtility P S logUtility = ⨅ (μ : MeasureTheory.Measure 𝓧), ⨅ (_ : MemEffectiveSet S μ), KL P μ

Duality between maximal logarithmic utility and minimal Kullback-Leibler divergence.