From bae30df53b594b23417e162edce446def950d432 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 13 Aug 2026 16:59:55 +0200 Subject: [PATCH] DPI --- Statlib.lean | 2 + Statlib/EValues/DPI.lean | 222 +++++++++++++++++++++++++++++++++++ Statlib/ForMathlib/ISup.lean | 134 +++++++++++++++++++++ 3 files changed, 358 insertions(+) create mode 100644 Statlib/EValues/DPI.lean create mode 100644 Statlib/ForMathlib/ISup.lean diff --git a/Statlib.lean b/Statlib.lean index 5ec9949..2f08ecf 100644 --- a/Statlib.lean +++ b/Statlib.lean @@ -1,3 +1,4 @@ +import Statlib.EValues.DPI import Statlib.EValues.EVariable import Statlib.EValues.Utility.Basic import Statlib.EValues.Utility.Log @@ -5,6 +6,7 @@ import Statlib.ForMathlib.Algebra.Order.Group.PosPart import Statlib.ForMathlib.Convex import Statlib.ForMathlib.ENNReal import Statlib.ForMathlib.EReal +import Statlib.ForMathlib.ISup import Statlib.ForMathlib.MeasureTheory.Integral.EReal.AuxLemmas import Statlib.ForMathlib.MeasureTheory.Integral.EReal.Bochner import Statlib.ForMathlib.MeasureTheory.Integral.EReal.EIntegrable diff --git a/Statlib/EValues/DPI.lean b/Statlib/EValues/DPI.lean new file mode 100644 index 0000000..ca190e8 --- /dev/null +++ b/Statlib/EValues/DPI.lean @@ -0,0 +1,222 @@ +/- +Copyright (c) 2025 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne, Gaëtan Serré +-/ + +module + +public import Statlib.EValues.EVariable +public import Statlib.EValues.Utility.Log +public import Statlib.ForMathlib.ISup + +/-! +# Data Processing Inequality + +This file establishes the data processing inequality (DPI) for e-variables: applying a Markov +kernel or measurable function cannot increase the maximum expected utility. + +## Main definitions + +* `maxUtility P S U`: The maximum expected utility over all e-variables for `S` under measure `P`. +* `maxRandUtility P S U`: The maximum expected utility over randomized e-variables. + +## Main statements + +* `maxRandUtility_eq_maxUtility`: Randomization does not increase maximum utility. +* `maxUtility_comp_le`, `maxUtility_map_le`: Data processing inequalities for kernels and functions. +* `MeasurableEmbedding.maxUtility_map_eq`: Equality holds for measurable embeddings. +* `convexOn_maxUtility`: Maximum utility is convex in the measure. + +-/ + + +@[expose] public section + +open scoped ENNReal NNReal ProbabilityTheory + +open MeasureTheory ProbabilityTheory + +variable {𝓧 𝓨 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {S : Set (Measure 𝓧)} + +namespace ProbabilityTheory + +/-- The maximum utility `∫ᵉ x, (U ∘ X) x ∂P` of a measure `P` over all e-variables `X` for +a set of measures `S`. -/ +noncomputable +def maxUtility (P : Measure 𝓧) (S : Set (Measure 𝓧)) (U : Utility) : EReal := + ⨆ (X : 𝓧 → ℝ≥0∞) (_hX : IsEVar X S), ∫ᵉ x, (U ∘ X) x ∂P + +/-- The maximum randomized utility `∫ᵉ x, U x ∂(η ∘ₘ P)` of a measure `P` over all randomized +e-variables `η` for a set of measures `S`. -/ +noncomputable +def maxRandUtility (P : Measure 𝓧) (S : Set (Measure 𝓧)) (U : Utility) : EReal := + ⨆ (η : Kernel 𝓧 ℝ≥0∞) (_hη₁ : IsMarkovKernel η) (_hη₂ : IsRandEVar η S), ∫ᵉ x, U x ∂(η ∘ₘ P) + +variable {P : Measure 𝓧} {S T : Set (Measure 𝓧)} {U : Utility} {φ : 𝓧 → 𝓨} + +lemma maxUtility_eq_sSup : maxUtility P S U = + sSup {y | ∃ X, IsEVar X S ∧ y = ∫ᵉ x, (U ∘ X) x ∂P} := iSup₂_eq_sSup + +lemma maxRandUtility_eq_sSup : maxRandUtility P S U = + sSup {y | ∃ η, IsMarkovKernel η ∧ IsRandEVar η S ∧ y = ∫ᵉ x, U x ∂(η ∘ₘ P)} := iSup₃_eq_sSup + +@[simp] +lemma maxUtility_empty : maxUtility P ∅ U = U ∞ * P .univ := by + simp only [maxUtility, Function.comp_apply] + refine le_antisymm ?_ ?_ + · refine iSup₂_le_iff.mpr fun Y hY ↦ ?_ + calc ∫ᵉ x, U (Y x) ∂P + _ ≤ ∫ᵉ x, U ∞ ∂P := eintegral_mono fun _ ↦ U.monotone le_top + _ = U ∞ * P .univ := by simp + · exact le_iSup_of_le (fun _ ↦ ∞) (le_of_eq (by simp)) + +lemma maxUtility_anti (hS : S ⊆ T) : maxUtility P T U ≤ maxUtility P S U := by + rw [maxUtility_eq_sSup, maxUtility_eq_sSup] + refine sSup_le_sSup ?_ + rintro y ⟨X, hX, hy⟩ + exact ⟨X, hX.anti_set hS, hy⟩ + +lemma maxRandUtility_anti (hS : S ⊆ T) : maxRandUtility P T U ≤ maxRandUtility P S U := by + rw [maxRandUtility_eq_sSup, maxRandUtility_eq_sSup] + refine sSup_le_sSup ?_ + rintro y ⟨η, hη₁, hη₂, hy⟩ + exact ⟨η, hη₁, hη₂.anti_set hS, hy⟩ + +/-- The maximum randomized utility is the maximum utility. -/ +lemma maxRandUtility_eq_maxUtility (P : Measure 𝓧) (S : Set (Measure 𝓧)) : + maxRandUtility P S U = maxUtility P S U := by + refine le_antisymm ?_ ?_ + · rw [maxRandUtility_eq_sSup] + rw [sSup_le_iff] + rintro y ⟨η, hη₁, hη₂, hy⟩ + obtain ⟨X, hX, h_le⟩ : ∃ X, IsEVar X S ∧ y ≤ ∫ᵉ x, (U ∘ X) x ∂P := by + let X := fun x ↦ ∫⁻ y, y ∂(η x) + refine ⟨X, ⟨by fun_prop, fun μ hμ ↦ ?_, fun μ hμ ↦ ?_⟩, ?_⟩ + · rw [isRandEVar_iff_isEVar] at hη₂ + exact hη₂.eintegral_ne_bot μ hμ + · rw [isRandEVar_iff_isEVar] at hη₂ + exact hη₂.eintegral_nonpos μ hμ + · rw [hy] + refine (eintegral_comp_measure_le U.measurable).trans ?_ + refine eintegral_mono fun _ ↦ ?_ + exact U.eintegral_le_map (by fun_prop) + trans ∫ᵉ x, (U ∘ X) x ∂P + · exact h_le + · rw [maxUtility_eq_sSup] + refine le_sSup ?_ + exact ⟨X, hX, rfl⟩ + · rw [maxRandUtility_eq_sSup, maxUtility_eq_sSup] + refine sSup_le_sSup ?_ + rintro y ⟨X, hX, hy⟩ + refine ⟨Kernel.deterministic X hX.measurable, inferInstance, ⟨fun μ hμ ↦ ?_, fun μ hμ ↦ ?_⟩, ?_⟩ + · simp only [Kernel.lintegral_deterministic] + exact hX.eintegral_ne_bot μ hμ + · simp only [Kernel.lintegral_deterministic] + exact hX.eintegral_nonpos μ hμ + · rw [hy, Measure.deterministic_comp_eq_map hX.measurable, + eintegral_map U.measurable hX.measurable] + rfl + +/-- **Data Processing Inequality** for randomized utility a Markov kernel. -/ +lemma maxRandUtility_comp_le (P : Measure 𝓧) {S : Set (Measure 𝓧)} (κ : Kernel 𝓧 𝓨) + [IsMarkovKernel κ] : + maxRandUtility (κ ∘ₘ P) {κ ∘ₘ μ | μ ∈ S} U ≤ maxRandUtility P S U := by + simp_rw [maxRandUtility_eq_sSup] + refine sSup_le_sSup fun y ↦ ?_ + rintro ⟨η, hη₁, hη₂, hξ_int⟩ + rw [P.comp_assoc] at hξ_int + exact ⟨η ∘ₖ κ, inferInstance, hη₂.comp, hξ_int⟩ + +/-- **Data processing inequality** for the maximum utility and a Markov kernel. -/ +lemma maxUtility_comp_le (P : Measure 𝓧) {S : Set (Measure 𝓧)} (κ : Kernel 𝓧 𝓨) + [IsMarkovKernel κ] : maxUtility (κ ∘ₘ P) {κ ∘ₘ μ | μ ∈ S} U ≤ maxUtility P S U := by + rw [← maxRandUtility_eq_maxUtility _ _, ← maxRandUtility_eq_maxUtility _ _] + exact maxRandUtility_comp_le P κ + +/-- **Data processing inequality** for the maximum utility and a measurable function. -/ +lemma maxUtility_map_le (P : Measure 𝓧) {S : Set (Measure 𝓧)} (hφ : Measurable φ) : + maxUtility (P.map φ) {μ.map φ | μ ∈ S} U ≤ maxUtility P S U := by + simp_rw [← Measure.deterministic_comp_eq_map hφ] + exact maxUtility_comp_le P <| Kernel.deterministic φ hφ + +/-- **Data processing Equality**: mapping by a measurable embeddings preserve maximum utility. -/ +lemma _root_.MeasurableEmbedding.maxUtility_map_eq [Nonempty 𝓧] (φ : 𝓧 → 𝓨) + (hφ : MeasurableEmbedding φ) (P : Measure 𝓧) (S : Set (Measure 𝓧)) : + maxUtility (P.map φ) {μ.map φ | μ ∈ S} U = maxUtility P S U := by + have hφ_inv : hφ.invFun ∘ φ = id := by -- extract lemma + ext x + simp only [Function.comp_apply, id_eq] + rw [hφ.leftInverse_invFun] + apply le_antisymm (maxUtility_map_le P hφ.measurable) + have hP_eq : P = (P.map φ).map hφ.invFun := by + rw [Measure.map_map hφ.measurable_invFun hφ.measurable, hφ_inv, Measure.map_id] + have hS_eq : S = {μ.map hφ.invFun | μ ∈ {ν.map φ | ν ∈ S}} := by + ext μ + simp only [Set.mem_ofPred_eq, exists_exists_and_eq_and] + refine ⟨fun hμ ↦ ?_, fun hμ ↦ ?_⟩ + · refine ⟨μ, hμ, ?_⟩ + rw [Measure.map_map hφ.measurable_invFun hφ.measurable, hφ_inv, Measure.map_id] + · obtain ⟨ν, hν, rfl⟩ := hμ + rwa [Measure.map_map hφ.measurable_invFun hφ.measurable, hφ_inv, Measure.map_id] + conv_lhs => rw [hP_eq, hS_eq] + exact maxUtility_map_le (P.map φ) hφ.measurable_invFun + +/-- The maximum log utility is nonnegative. -/ +lemma maxUtility_nonneg (P : Measure 𝓧) : + 0 ≤ maxUtility P S logUtility := by + calc 0 + _ ≤ ∫ᵉ x, (logUtility.toFun ∘ (fun _ ↦ 1)) x ∂P := by simp [logUtility] + _ ≤ maxUtility P S logUtility := by + refine le_iSup₂ (f := fun X _ ↦ ∫ᵉ x, (logUtility.toFun ∘ X) x ∂P) (fun _ ↦ 1) ?_ + exact isEVar_fun_one S + +/-- The maximum utility is a convex function of the measure. -/ +lemma convexOn_maxUtility (S : Set (Measure 𝓧)) : + ConvexOn ℝ≥0∞ Set.univ (fun P ↦ maxUtility P S U) := by + refine ⟨convex_univ, fun P _ Q _ a b ha hb hab ↦ ?_⟩ + simp only [maxUtility] + have ha : a ≠ ∞ := ne_top_of_le_ne_top (by simp : 1 ≠ ∞) (by simp [← hab]) + have hb : b ≠ ∞ := ne_top_of_le_ne_top (by simp : 1 ≠ ∞) (by simp [← hab]) + simp_rw [eintegral_add_measure, eintegral_smul_measure ha, eintegral_smul_measure hb] + calc ⨆ (X) (_ : IsEVar X S), a * ∫ᵉ x, (U.toFun ∘ X) x ∂P + b * ∫ᵉ x, (U.toFun ∘ X) x ∂Q + _ = ⨆ X, (a * ⨆ (_ : IsEVar X S), ∫ᵉ x, (U.toFun ∘ X) x ∂P) + + b * ⨆ (_ : IsEVar X S), ∫ᵉ x, (U.toFun ∘ X) x ∂Q := by + congr with X + by_cases hX : IsEVar X S + · simp [hX] + · simp only [hX, Function.comp_apply, not_false_eq_true, iSup_neg] + by_cases ha : a = 0 + · have hb : 0 < (b : EReal) := by + simp only [EReal.coe_ennreal_pos] + by_contra! + have : b = 0 := by grind + simp [ha, this] at hab + rw [EReal.mul_bot_of_pos hb] + simp + · have ha' : 0 < (a : EReal) := by simp; grind + rw [EReal.mul_bot_of_pos ha'] + simp + _ ≤ (⨆ X, a * ⨆ (_ : IsEVar X S), ∫ᵉ x, (U.toFun ∘ X) x ∂P) + + ⨆ X, b * ⨆ (_ : IsEVar X S), ∫ᵉ x, (U.toFun ∘ X) x ∂Q := EReal.iSup_add_le_add_iSup + _ = a • maxUtility P S U + b • maxUtility Q S U := by + simp only [maxUtility, EReal.smul_ennreal_eq_mul] + rw [EReal.iSup_ennreal_mul hb, EReal.iSup_ennreal_mul ha] + +lemma maxUtility_involutive (P : Measure 𝓧) (S : Set (Measure 𝓧)) {φ : 𝓧 → 𝓧} + (hφ : Measurable φ) (hφ_inv : φ ∘ φ = id) : + maxUtility P {μ.map φ | μ ∈ S} U = maxUtility (P.map φ) S U := by + apply le_antisymm + · calc maxUtility P {μ.map φ | μ ∈ S} U + _ = maxUtility ((P.map φ).map φ) {μ.map φ | μ ∈ S} U := by + rw [Measure.map_map hφ hφ, hφ_inv, Measure.map_id] + _ ≤ maxUtility (P.map φ) S U := maxUtility_map_le _ hφ + · calc maxUtility (P.map φ) S U + _ = maxUtility (P.map φ) {(μ.map φ).map φ | μ ∈ S} U := by + congr with μ + simp_rw [Measure.map_map hφ hφ, hφ_inv, Measure.map_id] + grind + _ = maxUtility (P.map φ) {μ.map φ | μ ∈ {ν.map φ | ν ∈ S}} U := by congr with μ; simp + _ ≤ maxUtility P {μ.map φ | μ ∈ S} U := maxUtility_map_le _ hφ + +end ProbabilityTheory diff --git a/Statlib/ForMathlib/ISup.lean b/Statlib/ForMathlib/ISup.lean new file mode 100644 index 0000000..0741c6e --- /dev/null +++ b/Statlib/ForMathlib/ISup.lean @@ -0,0 +1,134 @@ +/- +Copyright (c) 2025 Gaëtan Serré. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gaëtan Serré +-/ + +module + +public import Mathlib.Data.EReal.Basic +public import Mathlib.Order.CompletePartialOrder + +/-! # Lemmas about iSup and iInf +-/ + +@[expose] public section + +lemma iSup₂_eq_sSup {α ι : Type*} [CompleteLattice ι] {P : α → Prop} {g : α → ι} : + ⨆ (x : α) (_ : P x), g x = sSup {y | ∃ x, P x ∧ y = g x} := by + rw [sSup_eq_iSup] + simp_rw [Set.mem_ofPred_eq, iSup_exists, iSup_and] + suffices ⨆ a, ⨆ x, ⨆ (_ : P x), ⨆ (_ : a = g x), a = + ⨆ x, ⨆ (_ : P x), ⨆ a, ⨆ (_ : a = g x), a by + simp_rw [this, iSup_iSup_eq_left] + rw [iSup_comm] + refine iSup_congr fun i => ?_ + rw [iSup_comm] + +lemma iSup₃_eq_sSup {α ι : Type*} [CompleteLattice ι] {P₁ P₂ : α → Prop} {g : α → ι} : + ⨆ (x : α) (_ : P₁ x) (_ : P₂ x), g x = sSup {y | ∃ x, P₁ x ∧ P₂ x ∧ y = g x} := by + rw [sSup_eq_iSup] + simp_rw [Set.mem_ofPred_eq, iSup_exists, iSup_and] + suffices ⨆ a, ⨆ x, ⨆ (_ : P₁ x), ⨆ (_ : P₂ x), ⨆ (_ : a = g x), a = + ⨆ x, ⨆ (_ : P₁ x), ⨆ (_ : P₂ x), ⨆ a, ⨆ (_ : a = g x), a by + simp_rw [this, iSup_iSup_eq_left] + rw [iSup_comm] + refine iSup_congr fun i => ?_ + rw [iSup_comm] + refine iSup_congr fun i => ?_ + rw [iSup_comm] + +lemma iInf₂_eq_sInf {α ι : Type*} [CompleteLattice ι] {P : α → Prop} {g : α → ι} : + ⨅ (x : α) (_ : P x), g x = sInf {y | ∃ x, P x ∧ y = g x} := by + rw [sInf_eq_iInf] + simp_rw [Set.mem_ofPred_eq, iInf_exists, iInf_and] + suffices ⨅ a, ⨅ x, ⨅ (_ : P x), ⨅ (_ : a = g x), a = + ⨅ x, ⨅ (_ : P x), ⨅ a, ⨅ (_ : a = g x), a by + simp_rw [this, iInf_iInf_eq_left] + rw [iInf_comm] + refine iInf_congr fun i => ?_ + rw [iInf_comm] + +lemma iInf₃_eq_sInf {α ι : Type*} [CompleteLattice ι] {P₁ P₂ : α → Prop} {g : α → ι} : + ⨅ (x : α) (_ : P₁ x) (_ : P₂ x), g x = sInf {y | ∃ x, P₁ x ∧ P₂ x ∧ y = g x} := by + rw [sInf_eq_iInf] + simp_rw [Set.mem_ofPred_eq, iInf_exists, iInf_and] + suffices ⨅ a, ⨅ x, ⨅ (_ : P₁ x), ⨅ (_ : P₂ x), ⨅ (_ : a = g x), a = + ⨅ x, ⨅ (_ : P₁ x), ⨅ (_ : P₂ x), ⨅ a, ⨅ (_ : a = g x), a by + simp_rw [this, iInf_iInf_eq_left] + rw [iInf_comm] + refine iInf_congr fun i => ?_ + rw [iInf_comm] + refine iInf_congr fun i => ?_ + rw [iInf_comm] + +lemma iInf₄_eq_sInf {α β ι : Type*} [CompleteLattice ι] {P₁ : α → Prop} {P₂ : β → Prop} + {g : α → β → ι} : + ⨅ (x : α) (y : β) (_ : P₁ x) (_ : P₂ y), g x y = sInf {z | ∃ x y, P₁ x ∧ P₂ y ∧ z = g x y} := by + rw [sInf_eq_iInf] + simp_rw [Set.mem_ofPred_eq, iInf_exists, iInf_and] + suffices ⨅ a, ⨅ x, ⨅ y, ⨅ (_ : P₁ x), ⨅ (_ : P₂ y), ⨅ (_ : a = g x y), a = + ⨅ x, ⨅ y, ⨅ (_ : P₁ x), ⨅ (_ : P₂ y), ⨅ a, ⨅ (_ : a = g x y), a by + simp_rw [this, iInf_iInf_eq_left] + rw [iInf_comm] + refine iInf_congr fun i => ?_ + rw [iInf_comm] + refine iInf_congr fun i => ?_ + rw [iInf_comm] + refine iInf_congr fun i => ?_ + rw [iInf_comm] + +lemma iSup₄_eq_sSup {α β ι : Type*} [CompleteLattice ι] {P₁ : α → Prop} {P₂ : β → Prop} + {g : α → β → ι} : + ⨆ (x : α) (y : β) (_ : P₁ x) (_ : P₂ y), g x y = sSup {z | ∃ x y, P₁ x ∧ P₂ y ∧ z = g x y} := by + rw [sSup_eq_iSup] + simp_rw [Set.mem_ofPred_eq, iSup_exists, iSup_and] + suffices ⨆ a, ⨆ x, ⨆ y, ⨆ (_ : P₁ x), ⨆ (_ : P₂ y), ⨆ (_ : a = g x y), a = + ⨆ x, ⨆ y, ⨆ (_ : P₁ x), ⨆ (_ : P₂ y), ⨆ a, ⨆ (_ : a = g x y), a by + simp_rw [this, iSup_iSup_eq_left] + rw [iSup_comm] + refine iSup_congr fun i => ?_ + rw [iSup_comm] + refine iSup_congr fun i => ?_ + rw [iSup_comm] + refine iSup_congr fun i => ?_ + rw [iSup_comm] + +open Pointwise + +lemma sInf_add' {α : Type*} [AddCommMagma α] [Sub α] [CompleteLattice α] [OrderedSub α] + {s t : Set α} : sInf (s + t) = sInf s + sInf t := by + let u := fun (p q : α) ↦ p + q + let l := fun (a b : α) ↦ b - a + apply sInf_image2_eq_sInf_sInf (u := u) (u₁ := l) (u₂ := l) ?_ ?_ + all_goals simp only [GaloisConnection, tsub_le_iff_right, Function.swap, implies_true, l, u] + simp_rw [add_comm] + simp + +lemma iInf₂_add {α β ι : Type*} [AddCommMagma ι] [Sub ι] [CompleteLattice ι] [OrderedSub ι] + {P₁ : α → Prop} {P₂ : β → Prop} {f : α → ι} {g : β → ι} : + (⨅ (x : α) (_ : P₁ x), f x) + (⨅ (y : β) (_ : P₂ y), g y) = + ⨅ (x : α) (y : β) (_ : P₁ x) (_ : P₂ y), f x + g y := by + rw [iInf₂_eq_sInf, iInf₂_eq_sInf, iInf₄_eq_sInf, ← sInf_add'] + congr + ext y + rw [Set.mem_add] + constructor + · rintro ⟨_, ⟨a, ha, rfl⟩, _, ⟨b, hb, rfl⟩, rfl⟩ + exact ⟨a, b, ha, hb, rfl⟩ + · rintro ⟨a, b, ha, hb, rfl⟩ + exact ⟨f a, ⟨a, ha, rfl⟩, g b, ⟨b, hb, rfl⟩, rfl⟩ + +lemma exists_iSup₂_EReal_add {α β : Type*} {P₁ : α → Prop} {P₂ : β → Prop} + {f : α → EReal} {g : β → EReal} {x : α} (hx : P₁ x) {y : β} (hy : P₂ y) + (hx_sup : f x = ⨆ (x : α) (_ : P₁ x), f x) + (hy_sup : g y = ⨆ (y : β) (_ : P₂ y), g y) : + (⨆ (x : α) (_ : P₁ x), f x) + (⨆ (y : β) (_ : P₂ y), g y) = + ⨆ (x : α) (y : β) (_ : P₁ x) (_ : P₂ y), f x + g y := by + refine le_antisymm ?_ ?_ + · rw [← hx_sup, ← hy_sup] + exact le_iSup₂_of_le x y <| le_iSup₂_of_le hx hy <| le_refl _ + · refine iSup₂_le fun i j ↦ iSup₂_le fun hi hj ↦ ?_ + calc + _ ≤ (⨆ (x) (_ : P₁ x), f x) + g j := add_le_add_left (le_biSup f hi) _ + _ ≤ (⨆ (x) (_ : P₁ x), f x) + ⨆ (y) (_ : P₂ y), g y := add_le_add_right (le_biSup g hj) _