Finite fiber-average conditional expectation: combinatorial API proposal
We propose a self-contained combinatorial API for finite conditional expectation by fiber averaging, filling a gap between Mathlib's abstract measure-theoretic condExp and explicit finite-sum computation.
Mathlib's condExp provides the standard a.e. laws (condExp_const, condExp_of_aestronglyMeasurable', condExp_condExp_of_le, pull-out lemmas) but does not identify condExp for counting measure on a finite quotient with the explicit pointwise fiber-average formula. The API below supplies this concrete bridge.
Definitions
Given finite types Ω, X, and a surjective map π : Ω → X:
fiberAverage f a = (∑ b ∈ fiber(π(a)), f b) / |fiber(π(a))|finiteMean f = (∑ a, f a) / |Ω|finiteVariance f = ∑ a, f(a)² − |Ω| · (finiteMean f)²FiberInvariant f iff f is constant on each fiber
Proved properties (over any ordered field 𝕜)
Operator-algebraic package:
- Positivity:
(∀ a, 0 ≤ f a) → ∀ a, 0 ≤ fiberAverage f a
- Unitality:
fiberAverage 1 = 1
- Idempotence:
fiberAverage (fiberAverage f) = fiberAverage f
- Identity on invariants:
FiberInvariant f → fiberAverage f = f
- Bimodule law:
fiberAverage (B₁ · A · B₂) = B₁ · fiberAverage(A) · B₂ for fiber-invariant B₁, B₂
Analytic package:
6. Mean preservation: finiteMean (fiberAverage f) = finiteMean f
7. L² contraction: ∑ a, (fiberAverage f a)² ≤ ∑ a, f(a)²
8. Variance dissipation: finiteVariance (fiberAverage f) ≤ finiteVariance f
9. One-atom annihilation: [Subsingleton X] → finiteVariance (fiberAverage f) = 0
All proofs use only finite sums, sq_sum_le_card_mul_sum_sq, and field_simp/ring. The file has no sorry, admit, or axiom, and typechecks against Lean 4.29.0-rc8 + Mathlib v4.29.0-rc8 (the versions pinned by this repository).
Non-redundancy with Mathlib
Mathlib's MeasureTheory.Function.ConditionalExpectation provides the five operator-algebraic laws at the abstract a.e. level (with integrability/measurability hypotheses). It does not contain a theorem identifying condExp for counting measure and a comap sigma-algebra with the explicit pointwise fiber-average formula above. The analytic package (L² contraction, variance dissipation) is also absent in this finite combinatorial form.
A prototype Lean file (332 lines) is available and builds cleanly as Analysis.Misc.FiniteConditionalExpectation in a local checkout of this repo. If you think this fits the scope of the project, we would be glad to submit a PR adapted to the repository's style and review conventions.
Repo: https://github.com/the-omega-institute/automath
Finite fiber-average conditional expectation: combinatorial API proposal
We propose a self-contained combinatorial API for finite conditional expectation by fiber averaging, filling a gap between Mathlib's abstract measure-theoretic
condExpand explicit finite-sum computation.Mathlib's
condExpprovides the standard a.e. laws (condExp_const,condExp_of_aestronglyMeasurable',condExp_condExp_of_le, pull-out lemmas) but does not identifycondExpfor counting measure on a finite quotient with the explicit pointwise fiber-average formula. The API below supplies this concrete bridge.Definitions
Given finite types
Ω,X, and a surjective mapπ : Ω → X:fiberAverage f a = (∑ b ∈ fiber(π(a)), f b) / |fiber(π(a))|finiteMean f = (∑ a, f a) / |Ω|finiteVariance f = ∑ a, f(a)² − |Ω| · (finiteMean f)²FiberInvariant fifffis constant on each fiberProved properties (over any ordered field
𝕜)Operator-algebraic package:
(∀ a, 0 ≤ f a) → ∀ a, 0 ≤ fiberAverage f afiberAverage 1 = 1fiberAverage (fiberAverage f) = fiberAverage fFiberInvariant f → fiberAverage f = ffiberAverage (B₁ · A · B₂) = B₁ · fiberAverage(A) · B₂for fiber-invariantB₁,B₂Analytic package:
6. Mean preservation:
finiteMean (fiberAverage f) = finiteMean f7. L² contraction:
∑ a, (fiberAverage f a)² ≤ ∑ a, f(a)²8. Variance dissipation:
finiteVariance (fiberAverage f) ≤ finiteVariance f9. One-atom annihilation:
[Subsingleton X] → finiteVariance (fiberAverage f) = 0All proofs use only finite sums,
sq_sum_le_card_mul_sum_sq, andfield_simp/ring. The file has nosorry,admit, oraxiom, and typechecks against Lean 4.29.0-rc8 + Mathlib v4.29.0-rc8 (the versions pinned by this repository).Non-redundancy with Mathlib
Mathlib's
MeasureTheory.Function.ConditionalExpectationprovides the five operator-algebraic laws at the abstract a.e. level (with integrability/measurability hypotheses). It does not contain a theorem identifyingcondExpfor counting measure and a comap sigma-algebra with the explicit pointwise fiber-average formula above. The analytic package (L² contraction, variance dissipation) is also absent in this finite combinatorial form.A prototype Lean file (332 lines) is available and builds cleanly as
Analysis.Misc.FiniteConditionalExpectationin a local checkout of this repo. If you think this fits the scope of the project, we would be glad to submit a PR adapted to the repository's style and review conventions.Repo: https://github.com/the-omega-institute/automath