[RemyDegenne]

This PR adds the essential supremum of an arbitrary family of ℝ≥0∞-valued functions, MeasureTheory.essSupFamily f μ for f : ι → Ω → ℝ≥0∞ and any index type, together with its characterizing API, in the new file LMLExplore/MeasureTheory/Function/EssSupFamily.lean. This is the second bullet of EValues Layer 3.1 ("Essential supremum of a family"), the general tool the roadmap places in LMLExplore/MeasureTheory/Function/.

Roadmap: EValues

Target: EValues README, Layer 3.1 Definition and characterization, bullet Essential supremum of a family [RRLK, Appendix A; FS16, §A.5]: for a σ-finite measure and any nonempty family of measurable functions Ω → ℝ≥0∞, construct a measurable function that dominates every member a.e. and is a.e. below every measurable function that does; prove that it is the supremum of a countable subfamily, and the supremum of an increasing sequence of the family when the family is directed upward. Its consumer is the next bullet of the same milestone, the Snell envelope: L n is defined as the essential supremum, over the bounded stopping times τ ≥ n, of conditional expectations given ℱ n. That needs essSupFamily for an uncountable index type, measurable_essSupFamily for ℱ n-measurability, and exists_seq_monotone_ae_eq_essSupFamily / setLIntegral_essSupFamily_of_directed for the supermartingale property and ∫⁻ L 0 ∂P = ⨆ τ, ∫⁻ E τ ∂P. The envelope in turn feeds [RRLK, Lemma 6]. After this PR, Layer 3.1 still needs the definition IsEProcess, the Snell envelope and [RRLK, Lemma 6].

What the file contains:

• exists_seq_forall_ae_le_iSup: for an s-finite μ, a nonempty family of a.e.-measurable functions is a.e. dominated by the supremum of a sequence of its members. This is the existence theorem. The proof follows [FS16, §A.5]: minimize ∫⁻ (1 + sup)⁻¹ ∂μ.toFinite over sequences of members, concatenate a minimizing sequence of sequences with iSup_unpair, and adjoin one member at a time, using ae_eq_of_ae_le_of_lintegral_le.
• essSupFamily and essSupFamily_def; essSupFamily_of_isEmpty (simp).
• The universal property, up to null sets: ae_le_essSupFamily, essSupFamily_ae_le (no hypotheses, and the upper bound need not be measurable), essSupFamily_ae_le_iff, ae_eq_essSupFamily_iff (uniqueness), and essSupFamily_mono_ae.
• measurable_essSupFamily (for any σ-algebra m for which the members are measurable, so a sub-σ-algebra works) and aemeasurable_essSupFamily.
• exists_countable_essSupFamily_eq (unconditional), exists_seq_essSupFamily_eq, essSupFamily_le_iSup (pointwise), and essSupFamily_ae_eq_iSup (countable families, for any measure, with no measurability).
• The directed case: exists_seq_monotone_ae_eq_essSupFamily (a.e. increasing sequence of members) and setLIntegral_essSupFamily_of_directed (monotone convergence over any set).

Ways the roadmap statement is generalized: the measure is s-finite rather than σ-finite, and s-finiteness is needed, as an infinite multiple of counting measure on an uncountable set shows. Members need only be a.e.-measurable. The family is indexed by any type rather than given as a set, so a set 𝒳 is the case f = Subtype.val. Directedness is up to null sets, Directed (· ≤ᵐ[μ] ·) f, which is the form the Snell envelope's pasting of stopping times provides.

No Mathlib, Tau Ceti, LML or Statlib declaration provides this. I searched for "essential supremum" and essSup-of-a-family / countable-subfamily statements in all four. Mathlib's essSup g μ is the constant essential supremum of one function, and Tau Ceti's exists_countable_iSup_eq_of_continuous concerns pointwise suprema of continuous functions. No public declarations are removed or renamed.

Local checks (tauceti-local-checks verify --policy ordinary): scope: scoped: against 13fc17b, local-axioms: checked 1 changed module(s), 19 declaration(s); 0 violation(s), whole-library lake build --iofail green, style and environment lint pass. These were run with the real toolchain lean on PATH/LEAN because the host's memory-gated wrapper was stalled; CI is authoritative.

🤖 Prepared with Claude Code

[RemyDegenne]

🟡 documentation — request_changes claude/claude-opus-5-5

Declaration docstrings match their statements; the module overview overclaims by stating existence for s-finite measures without the a.e.-measurability hypothesis.

• LMLExplore/MeasureTheory/Function/EssSupFamily.lean:17 — The module overview says 'For an s-finite measure it exists' for an arbitrary family f, but the existence results (exists_seq_forall_ae_le_iSup, ae_le_essSupFamily) also require ∀ i, AEMeasurable (f i) μ. Without that hypothesis the definition can fall back to 0, which need not dominate the members. Fix: Change it to 'For an s-finite measure and almost everywhere measurable members it exists, …', matching line 38 and the definition docstring at line 117.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 36s · 44.2k in (36.6k cache read, 7.6k cache write) / 3.5k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	Definition and all statements faithfully formalize the essential supremum of a family (FS16 §A.5), including the universal property, measurability for sub-σ-algebras, countable-subfamily representation and the directed case; edge cases (empty family, countable family, non-measurable bounds) are handled correctly. No vacuity, placeholders or over-strong assumptions found.
✅	reuse	approved	claude/claude-opus-5-5	No Mathlib or LMLExplore declaration provides an essential supremum of a family of functions, and the proofs reuse the relevant Mathlib API (ae_eq_of_ae_le_of_lintegral_le, iSup_unpair, Measure.toFinite, lintegral_iSup', Measurable.biSup). Directed.sequence and lintegral_iSup_directed would only fit with encodable or countable index types, so they cannot replace the hand-rolled sequence or the directed integral lemma.
✅	scope	approved	claude/claude-opus-5-5	The PR builds the target named in EValues Layer 3.1, 'Essential supremum of a family' (README.md:534-538): existence, the universal property, the countable subfamily and the directed case, which the next bullet, the Snell envelope, uses directly. It is one topic in one new file under the roadmap-designated LMLExplore/MeasureTheory/Function/, and does not duplicate anything already in the code.
✅	attribution	approved	claude/claude-opus-5-5	The file credits both central informal sources the roadmap names, [FS16, §A.5] for the existence proof and [RRLK, Appendix A], and names Mathlib's Measure.toFinite, the key construction the proof uses. No Mathlib or prior formalization of a family essential supremum exists that would need credit.
✅	api-design	approved	claude/claude-opus-5-5	The surface is minimal, the definition body is hidden behind essSupFamily_def := (rfl), and the characterizing API (universal property, uniqueness, measurability, countable subfamily, directed case) is complete for the Snell envelope consumer. The one private helper is specific to this definition, and no compatibility or duplicate surface was found.
✅	generality	approved	claude/claude-opus-5-5	Every hypothesis is used and none is stronger than needed. The statements generalize the roadmap target naturally (s-finite, a.e.-measurable, any index type, a.e.-directed) without speculative abstraction or special-case duplication.
✅	placement	approved	claude/claude-opus-5-5	The new file sits in the roadmap-designated LMLExplore/MeasureTheory/Function/, matching Mathlib's placement of EssSup, and has no flat sibling sharing its prefix. Both imports supply declarations the proof uses (ae_eq_of_ae_le_of_lintegral_le; Measure.toFinite and related lemmas).
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions in standard Mathlib terminology, consistent with essSup_mono_ae, ae_le_essSup and lintegral_iSup_directed; _iff/_eq suffixes match the statements and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring and every public declaration are documented accurately, with each docstring's hypotheses and scope matching its statement and no process or roadmap narrative in the file.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, rely on standard Mathlib lemmas and one-step simp/rw, and have no undocumented change/show or cross-wrapper defeq. The one longer proof (existence) is under 50 lines and commented stage by stage.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 467d665. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $0.83.}