From c262bd86dbee354c5ccbdc6f7c8488c6507d1ff1 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 01:09:17 +0100 Subject: [PATCH 1/2] =?UTF-8?q?feat:=20the=20essential=20supremum=20of=20a?= =?UTF-8?q?=20family=20of=20=E2=84=9D=E2=89=A50=E2=88=9E-valued=20function?= =?UTF-8?q?s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Code --- .../MeasureTheory/Function/EssSupFamily.lean | 277 ++++++++++++++++++ 1 file changed, 277 insertions(+) create mode 100644 LMLExplore/MeasureTheory/Function/EssSupFamily.lean diff --git a/LMLExplore/MeasureTheory/Function/EssSupFamily.lean b/LMLExplore/MeasureTheory/Function/EssSupFamily.lean new file mode 100644 index 00000000..92c0b341 --- /dev/null +++ b/LMLExplore/MeasureTheory/Function/EssSupFamily.lean @@ -0,0 +1,277 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.MeasureTheory.Integral.Lebesgue.Markov +public import Mathlib.MeasureTheory.Measure.WithDensityFinite + +/-! +# The essential supremum of a family of functions + +For a family `f : ι → Ω → ℝ≥0∞` of functions, indexed by an arbitrary, possibly uncountable, +type, the pointwise supremum `fun ω ↦ ⨆ i, f i ω` need not be measurable, and changing each +`f i` on a null set may change it everywhere. The **essential supremum** of the family is the +almost everywhere least function that dominates every `f i` almost everywhere. For an s-finite +measure it exists, it is the supremum of a countable subfamily, and it is unique up to null sets. +It is the object behind the Snell envelope of optimal stopping, the essential supremum over +stopping times of conditional expectations. + +This is not Mathlib's `essSup g μ`, the essential supremum of the values of one function, which is +a constant. + +The existence proof is the argument of [FS16, §A.5], with the bounded decreasing transform +`x ↦ (1 + x)⁻¹` and a finite measure with the null sets of `μ` (Mathlib's `Measure.toFinite`): +a sequence of members minimizing the integral of `(1 + sup)⁻¹` dominates every member, since +adjoining a member can only lower the integrand and so cannot change it except on a null set. + +## Main definitions + +* `MeasureTheory.essSupFamily f μ`: the essential supremum of the family `f` with respect to `μ`. + It is the supremum of a countable subfamily, and `0` when no countable subfamily dominates the + family almost everywhere. + +## Main statements + +* `MeasureTheory.exists_seq_forall_ae_le_iSup`: for an s-finite measure, every nonempty family + of almost everywhere measurable functions is dominated almost everywhere by the supremum of a + sequence of its members. +* `MeasureTheory.ae_le_essSupFamily`, `MeasureTheory.essSupFamily_ae_le`, + `MeasureTheory.essSupFamily_ae_le_iff`, `MeasureTheory.ae_eq_essSupFamily_iff`: the essential + supremum dominates every member, is below every function that dominates every member, and is + characterized up to null sets by these two properties. +* `MeasureTheory.measurable_essSupFamily`: it is measurable for every σ-algebra for which the + members are, in particular for a sub-σ-algebra; `MeasureTheory.aemeasurable_essSupFamily`: it is + almost everywhere measurable when the members are. +* `MeasureTheory.exists_countable_essSupFamily_eq`, `MeasureTheory.exists_seq_essSupFamily_eq`: + it is the supremum of a countable subfamily. +* `MeasureTheory.exists_seq_monotone_ae_eq_essSupFamily`: for a family directed upward almost + everywhere, it is almost everywhere the supremum of an almost everywhere increasing sequence of + members, and `MeasureTheory.setLIntegral_essSupFamily_of_directed`: its integral over any set is + the supremum of the integrals of the members. + +## References + +* [FS16] H. Föllmer and A. Schied, *Stochastic Finance: An Introduction in Discrete Time*, + 4th edition, De Gruyter, 2016, §A.5. +* A. Ramdas, J. Ruf, M. Larsson and W. M. Koolen, *Admissible anytime-valid sequential inference + must rely on nonnegative martingales*, arXiv:2009.03167v3, Appendix A. +-/ + +public section + +open Filter Set +open scoped ENNReal + +namespace MeasureTheory + +variable {Ω ι : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f g : ι → Ω → ℝ≥0∞} + {h : Ω → ℝ≥0∞} + +/-- For an s-finite measure, every nonempty family of almost everywhere measurable functions with +values in `ℝ≥0∞` is dominated almost everywhere by the supremum of a sequence of its members. -/ +theorem exists_seq_forall_ae_le_iSup [SFinite μ] [Nonempty ι] (hf : ∀ i, AEMeasurable (f i) μ) : + ∃ s : ℕ → ι, ∀ i, f i ≤ᵐ[μ] fun ω ↦ ⨆ n, f (s n) ω := by + -- The value of a sequence of indices: the `μ.toFinite`-integral of `(1 + sup)⁻¹`. + let v : (ℕ → ι) → ℝ≥0∞ := fun s ↦ ∫⁻ ω, (1 + ⨆ n, f (s n) ω)⁻¹ ∂μ.toFinite + have hv_anti {s t : ℕ → ι} (hst : ∀ ω, ⨆ n, f (s n) ω ≤ ⨆ n, f (t n) ω) : v t ≤ v s := + lintegral_mono fun ω ↦ ENNReal.inv_le_inv.2 (add_le_add_right (hst ω) 1) + -- A sequence of sequences whose values tend to the infimum of the values. + obtain ⟨u, -, hu, hu_mem⟩ := exists_seq_tendsto_sInf (range_nonempty v) (OrderBot.bddBelow _) + choose s hs using hu_mem + -- Their concatenation `t` attains the infimum. + let t : ℕ → ι := fun m ↦ s (Nat.unpair m).1 (Nat.unpair m).2 + have ht_iSup (ω : Ω) : ⨆ m, f (t m) ω = ⨆ k, ⨆ n, f (s k n) ω := + iSup_unpair fun k n ↦ f (s k n) ω + have ht_min (r : ℕ → ι) : v t ≤ v r := by + refine (ge_of_tendsto' hu fun k ↦ ?_).trans (sInf_le (mem_range_self r)) + rw [← hs k] + exact hv_anti fun ω ↦ (ht_iSup ω).symm ▸ le_iSup (fun k ↦ ⨆ n, f (s k n) ω) k + refine ⟨t, fun i ↦ ?_⟩ + -- Adjoining `i` to `t` does not lower the value, hence does not change the supremum a.e. + let t' : ℕ → ι := fun n ↦ if n = 0 then i else t (n - 1) + have ht'_iSup (ω : Ω) : ⨆ n, f (t' n) ω = f i ω ⊔ ⨆ n, f (t n) ω := by + rw [← sup_iSup_nat_succ] + simp [t'] + have h_meas : AEMeasurable (fun ω ↦ (1 + ⨆ n, f (t n) ω)⁻¹) μ.toFinite := + ((AEMeasurable.iSup fun n ↦ hf (t n)).const_add 1).inv.mono_ac + (toFinite_absolutelyContinuous μ) + have h_fin : ∫⁻ ω, (1 + ⨆ n, f (t' n) ω)⁻¹ ∂μ.toFinite ≠ ∞ := by + refine ne_top_of_le_ne_top (measure_ne_top μ.toFinite univ) ?_ + rw [← lintegral_one] + exact lintegral_mono fun ω ↦ ENNReal.inv_le_one.2 le_self_add + have h_eq := ae_eq_of_ae_le_of_lintegral_le + (ae_of_all _ fun ω ↦ ENNReal.inv_le_inv.2 (add_le_add_right + ((ht'_iSup ω).symm ▸ le_sup_right) 1)) h_fin h_meas (ht_min t') + rw [ae_toFinite] at h_eq + filter_upwards [h_eq] with ω hω + rw [inv_inj, ENNReal.add_right_inj ENNReal.one_ne_top, ht'_iSup] at hω + exact hω ▸ le_sup_left + +open scoped Classical in +/-- The **essential supremum** of a family `f` of functions with values in `ℝ≥0∞` with respect to +a measure `μ`: the almost everywhere least function that dominates every `f i` almost everywhere. +It is defined as the supremum of a sequence of members that dominates every member almost +everywhere, which exists for an s-finite measure and almost everywhere measurable members +(`exists_seq_forall_ae_le_iSup`), and is `0` when no such sequence exists. -/ +noncomputable def essSupFamily (f : ι → Ω → ℝ≥0∞) (μ : Measure Ω) : Ω → ℝ≥0∞ := + if hs : ∃ s : ℕ → ι, ∀ i, f i ≤ᵐ[μ] fun ω ↦ ⨆ n, f (s n) ω then + fun ω ↦ ⨆ n, f (hs.choose n) ω + else 0 + +open scoped Classical in +/-- The defining equation of `essSupFamily`. -/ +theorem essSupFamily_def (f : ι → Ω → ℝ≥0∞) (μ : Measure Ω) : + essSupFamily f μ = if hs : ∃ s : ℕ → ι, ∀ i, f i ≤ᵐ[μ] fun ω ↦ ⨆ n, f (s n) ω then + fun ω ↦ ⨆ n, f (hs.choose n) ω + else 0 := (rfl) + +/-- The essential supremum of an empty family is `0`. -/ +@[simp] +theorem essSupFamily_of_isEmpty [IsEmpty ι] : essSupFamily f μ = 0 := by + simp [essSupFamily_def] + +/-- The essential supremum of a family is the supremum of a countable subfamily. -/ +theorem exists_countable_essSupFamily_eq (f : ι → Ω → ℝ≥0∞) (μ : Measure Ω) : + ∃ C : Set ι, C.Countable ∧ essSupFamily f μ = fun ω ↦ ⨆ i ∈ C, f i ω := by + by_cases hs : ∃ s : ℕ → ι, ∀ i, f i ≤ᵐ[μ] fun ω ↦ ⨆ n, f (s n) ω + · refine ⟨range hs.choose, countable_range _, ?_⟩ + simp only [essSupFamily_def, hs, dite_true, iSup_range] + · refine ⟨∅, countable_empty, ?_⟩ + simp only [essSupFamily_def, hs, dite_false] + simp [Pi.zero_def] + +/-- The essential supremum of a family is pointwise below the pointwise supremum. -/ +theorem essSupFamily_le_iSup (f : ι → Ω → ℝ≥0∞) (μ : Measure Ω) : + essSupFamily f μ ≤ fun ω ↦ ⨆ i, f i ω := by + obtain ⟨C, -, hC⟩ := exists_countable_essSupFamily_eq f μ + rw [hC] + exact fun ω ↦ iSup₂_le fun i _ ↦ le_iSup (fun i ↦ f i ω) i + +/-- The essential supremum of a family dominates every member almost everywhere as soon as some +sequence of members does. -/ +private theorem ae_le_essSupFamily_of_exists + (hs : ∃ s : ℕ → ι, ∀ i, f i ≤ᵐ[μ] fun ω ↦ ⨆ n, f (s n) ω) (i : ι) : + f i ≤ᵐ[μ] essSupFamily f μ := by + simp only [essSupFamily_def, hs, dite_true] + exact hs.choose_spec i + +/-- For an s-finite measure, the essential supremum of a family of almost everywhere measurable +functions dominates every member almost everywhere. -/ +theorem ae_le_essSupFamily [SFinite μ] (hf : ∀ i, AEMeasurable (f i) μ) (i : ι) : + f i ≤ᵐ[μ] essSupFamily f μ := + have : Nonempty ι := ⟨i⟩ + ae_le_essSupFamily_of_exists (exists_seq_forall_ae_le_iSup hf) i + +/-- The essential supremum of a family is almost everywhere below every function that dominates +every member almost everywhere. -/ +theorem essSupFamily_ae_le (hh : ∀ i, f i ≤ᵐ[μ] h) : essSupFamily f μ ≤ᵐ[μ] h := by + obtain ⟨C, hC, hC_eq⟩ := exists_countable_essSupFamily_eq f μ + have : Countable C := hC.to_subtype + filter_upwards [ae_all_iff.2 fun i : C ↦ hh i] with ω hω + rw [hC_eq] + exact iSup₂_le fun i hi ↦ hω ⟨i, hi⟩ + +/-- For an s-finite measure and almost everywhere measurable members, a function dominates the +essential supremum of a family almost everywhere exactly when it dominates every member. -/ +theorem essSupFamily_ae_le_iff [SFinite μ] (hf : ∀ i, AEMeasurable (f i) μ) : + essSupFamily f μ ≤ᵐ[μ] h ↔ ∀ i, f i ≤ᵐ[μ] h := + ⟨fun hh i ↦ (ae_le_essSupFamily hf i).trans hh, essSupFamily_ae_le⟩ + +/-- For an s-finite measure and almost everywhere measurable members, the essential supremum of a +family is characterized up to null sets as the function that dominates every member almost +everywhere and is almost everywhere below every function that does. -/ +theorem ae_eq_essSupFamily_iff [SFinite μ] (hf : ∀ i, AEMeasurable (f i) μ) : + h =ᵐ[μ] essSupFamily f μ ↔ + (∀ i, f i ≤ᵐ[μ] h) ∧ ∀ h' : Ω → ℝ≥0∞, (∀ i, f i ≤ᵐ[μ] h') → h ≤ᵐ[μ] h' := by + refine ⟨fun hh ↦ ⟨fun i ↦ (ae_le_essSupFamily hf i).trans hh.symm.le, fun h' hh' ↦ + hh.le.trans (essSupFamily_ae_le hh')⟩, fun ⟨hh, hmin⟩ ↦ ?_⟩ + exact (hmin _ (ae_le_essSupFamily hf)).antisymm (essSupFamily_ae_le hh) + +/-- The essential supremum is monotone in the family, up to null sets. -/ +theorem essSupFamily_mono_ae [SFinite μ] (hg : ∀ i, AEMeasurable (g i) μ) + (hfg : ∀ i, f i ≤ᵐ[μ] g i) : essSupFamily f μ ≤ᵐ[μ] essSupFamily g μ := + essSupFamily_ae_le fun i ↦ (hfg i).trans (ae_le_essSupFamily hg i) + +/-- The essential supremum of a family of functions that are measurable for a σ-algebra `m`, +for instance a sub-σ-algebra, is `m`-measurable. -/ +theorem measurable_essSupFamily {m : MeasurableSpace Ω} (hf : ∀ i, Measurable[m] (f i)) : + Measurable[m] (essSupFamily f μ) := by + obtain ⟨C, hC, hC_eq⟩ := exists_countable_essSupFamily_eq f μ + rw [hC_eq] + exact Measurable.biSup C hC fun i _ ↦ hf i + +/-- The essential supremum of a family of almost everywhere measurable functions is almost +everywhere measurable. -/ +theorem aemeasurable_essSupFamily (hf : ∀ i, AEMeasurable (f i) μ) : + AEMeasurable (essSupFamily f μ) μ := by + obtain ⟨C, hC, hC_eq⟩ := exists_countable_essSupFamily_eq f μ + rw [hC_eq] + exact AEMeasurable.biSup C hC fun i _ ↦ hf i + +/-- For an s-finite measure, the essential supremum of a nonempty family of almost everywhere +measurable functions is the supremum of a sequence of members. -/ +theorem exists_seq_essSupFamily_eq [SFinite μ] [Nonempty ι] (hf : ∀ i, AEMeasurable (f i) μ) : + ∃ s : ℕ → ι, essSupFamily f μ = fun ω ↦ ⨆ n, f (s n) ω := by + have hs := exists_seq_forall_ae_le_iSup hf + exact ⟨hs.choose, by simp only [essSupFamily_def, hs, dite_true]⟩ + +/-- The essential supremum of a countable family is almost everywhere its pointwise supremum, +for every measure and with no measurability assumption. -/ +theorem essSupFamily_ae_eq_iSup [Countable ι] (f : ι → Ω → ℝ≥0∞) (μ : Measure Ω) : + essSupFamily f μ =ᵐ[μ] fun ω ↦ ⨆ i, f i ω := by + refine EventuallyLE.antisymm (ae_of_all μ (essSupFamily_le_iSup f μ)) ?_ + rcases isEmpty_or_nonempty ι with hι | hι + · exact ae_of_all _ fun ω ↦ by simp + obtain ⟨s, hs⟩ := exists_surjective_nat ι + have hex : ∃ s : ℕ → ι, ∀ i, f i ≤ᵐ[μ] fun ω ↦ ⨆ n, f (s n) ω := + ⟨s, fun i ↦ ae_of_all _ fun ω ↦ by + obtain ⟨n, rfl⟩ := hs i + exact le_iSup (fun n ↦ f (s n) ω) n⟩ + filter_upwards [ae_all_iff.2 (ae_le_essSupFamily_of_exists hex)] with ω hω + exact iSup_le hω + +/-- For an s-finite measure, the essential supremum of a nonempty family of almost everywhere +measurable functions that is directed upward almost everywhere is almost everywhere the supremum +of an almost everywhere increasing sequence of members. -/ +theorem exists_seq_monotone_ae_eq_essSupFamily [SFinite μ] [Nonempty ι] + (hf : ∀ i, AEMeasurable (f i) μ) (hd : Directed (· ≤ᵐ[μ] ·) f) : + ∃ s : ℕ → ι, (∀ᵐ ω ∂μ, Monotone fun n ↦ f (s n) ω) ∧ + essSupFamily f μ =ᵐ[μ] fun ω ↦ ⨆ n, f (s n) ω := by + obtain ⟨u, hu⟩ := exists_seq_essSupFamily_eq hf + choose j hj₁ hj₂ using hd + -- `s (n + 1)` dominates both `s n` and `u (n + 1)`. + let s : ℕ → ι := fun n ↦ Nat.rec (u 0) (fun k sk ↦ j sk (u (k + 1))) n + have hs_succ (n : ℕ) : s (n + 1) = j (s n) (u (n + 1)) := rfl + have hus (n : ℕ) : f (u n) ≤ᵐ[μ] f (s n) := by + cases n with + | zero => exact EventuallyLE.refl _ _ + | succ n => exact hs_succ n ▸ hj₂ _ _ + refine ⟨s, ?_, ?_⟩ + · filter_upwards [ae_all_iff.2 fun n ↦ hs_succ n ▸ hj₁ (s n) (u (n + 1))] with ω hω + exact monotone_nat_of_le_succ hω + · refine EventuallyLE.antisymm ?_ ?_ + · filter_upwards [ae_all_iff.2 hus] with ω hω + rw [hu] + exact iSup_mono hω + · filter_upwards [ae_all_iff.2 fun n ↦ ae_le_essSupFamily hf (s n)] with ω hω + exact iSup_le hω + +/-- For an s-finite measure and a family of almost everywhere measurable functions directed upward +almost everywhere, the integral of the essential supremum over any set is the supremum of the +integrals of the members. -/ +theorem setLIntegral_essSupFamily_of_directed [SFinite μ] (hf : ∀ i, AEMeasurable (f i) μ) + (hd : Directed (· ≤ᵐ[μ] ·) f) (s : Set Ω) : + ∫⁻ ω in s, essSupFamily f μ ω ∂μ = ⨆ i, ∫⁻ ω in s, f i ω ∂μ := by + refine le_antisymm ?_ (iSup_le fun i ↦ lintegral_mono_ae + (ae_restrict_of_ae (ae_le_essSupFamily hf i))) + rcases isEmpty_or_nonempty ι with hι | hι + · simp + obtain ⟨u, hmono, heq⟩ := exists_seq_monotone_ae_eq_essSupFamily hf hd + rw [lintegral_congr_ae (ae_restrict_of_ae heq), + lintegral_iSup' (fun n ↦ (hf (u n)).restrict) (ae_restrict_of_ae hmono)] + exact iSup_le fun n ↦ le_iSup (fun i ↦ ∫⁻ ω in s, f i ω ∂μ) (u n) + +end MeasureTheory From 467d665341ec5e1c4280d9b13a4191cbe0e9cca4 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 09:27:14 +0100 Subject: [PATCH 2/2] docs: state the a.e.-measurability hypothesis in the essSupFamily overview Co-Authored-By: Claude Code --- LMLExplore/MeasureTheory/Function/EssSupFamily.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/LMLExplore/MeasureTheory/Function/EssSupFamily.lean b/LMLExplore/MeasureTheory/Function/EssSupFamily.lean index 92c0b341..606ddfaf 100644 --- a/LMLExplore/MeasureTheory/Function/EssSupFamily.lean +++ b/LMLExplore/MeasureTheory/Function/EssSupFamily.lean @@ -15,7 +15,8 @@ For a family `f : ι → Ω → ℝ≥0∞` of functions, indexed by an arbitrar type, the pointwise supremum `fun ω ↦ ⨆ i, f i ω` need not be measurable, and changing each `f i` on a null set may change it everywhere. The **essential supremum** of the family is the almost everywhere least function that dominates every `f i` almost everywhere. For an s-finite -measure it exists, it is the supremum of a countable subfamily, and it is unique up to null sets. +measure and almost everywhere measurable members it exists, it is the supremum of a countable +subfamily, and it is unique up to null sets. It is the object behind the Snell envelope of optimal stopping, the essential supremum over stopping times of conditional expectations.