[dysfunctor]

Adds O'Donnell's Ornstein–Uhlenbeck operator L (§11.3) on top of the Hermite expansion:

• the Hermite differential equation;
• Gaussian integration by parts, ⟨L f, g⟩ = ⟨∇f, ∇g⟩;
• L on L²(γⁿ) as an operator with a named domain;
• L as the derivative of ρ ↦ U_ρ f, together with the domain characterization of Exercise 11.18 and the derivative formulas of Proposition 11.27.

Part of #2131 (Chapter 11). This is new mathematics. The only infrastructure is two small general lemmas, placed in their shared modules.

It builds on the Hermite expansion from #4868 and is a single commit on current main.

Conventions.

• L f is ornsteinUhlenbeck f : Lp ℝ 2 γⁿ, the series ∑ α, |α| f̂(α) h_α, where |α| = ∑ i, α i.
• Its domain is MemOrnsteinUhlenbeckDomain f: f ∈ L²(γⁿ) and ∑ α, |α|² f̂(α)² < ∞.
• On smooth functions, L appears as the expression x · ∇f − Δf, with partial derivatives along coordinate lines: deriv (fun t => f (Function.update z i t)) (z i).
• Derivatives of ρ ↦ U_ρ f are taken in L², as in the book. They apply to any family u : ℝ → Lp ℝ 2 γⁿ with u ρ =ᵐ U_ρ f for |ρ| ≤ 1.
• The book's definition is a left derivative in ρ at 1. In exponential time ρ = e^{−t} it becomes L f = −(d/dt) U_{e^{−t}} f |_{t=0⁺}, which is also stated.

New API (namespace ProbabilityTheory unless noted)

• Foundations/RingTheory/Polynomial/Hermite.lean: Polynomial.X_mul_derivative_hermite_sub, the Hermite equation X H_n′ − H_n″ = n H_n (Exercise 11.10(c)).
• Foundations/MeasureTheory/Integral/PiUpdate.lean: MeasureTheory.ae_integrable_update. An integrable F on a product of probability measures is integrable along almost every coordinate line.
• New Foundations/Probability/Gaussian/OrnsteinUhlenbeck.lean:
  • differential form:
    • mul_deriv_normalizedHermite_sub;
    • sum_mul_deriv_multiHermite_update_sub (x · ∇h_α − Δh_α = |α| h_α);
  • integration by parts:
    • integral_mul_deriv_sub_deriv_deriv_mul_gaussianReal;
    • integral_mul_deriv_update_sub_mul_pi_gaussianReal;
    • integral_sum_mul_deriv_update_sub_mul_pi_gaussianReal;
  • the operator and its domain:
    • ornsteinUhlenbeck, ornsteinUhlenbeck_def;
    • MemOrnsteinUhlenbeckDomain, memOrnsteinUhlenbeckDomain_iff;
    • MemOrnsteinUhlenbeckDomain.memLp, MemOrnsteinUhlenbeckDomain.summable;
    • memℓp_two_sum_mul_iff;
    • hermiteBasis_repr_ornsteinUhlenbeck, hermiteCoeff_ornsteinUhlenbeck;
  • Definition 11.24, Proposition 11.40 and Exercise 11.18:
    • hasDerivWithinAt_gaussianNoiseOp, hasDerivWithinAt_gaussianNoiseOp_exp_neg_zero;
    • eq_ornsteinUhlenbeck_of_hasDerivWithinAt;
    • memOrnsteinUhlenbeckDomain_of_hasDerivWithinAt;
    • exists_hasDerivWithinAt_gaussianNoiseOp_iff;
    • memOrnsteinUhlenbeckDomain_gaussianNoiseOp (11.18(c));
    • MemOrnsteinUhlenbeckDomain.gaussianNoiseOp;
  • Proposition 11.27:
    • ornsteinUhlenbeck_gaussianNoiseOp (L U_ρ f = U_ρ L f in L²);
    • hasDerivWithinAt_Icc_gaussianNoiseOp, hasDerivAt_gaussianNoiseOp;
    • memℓp_mul_pow_mul_hermiteCoeff;
    • hasDerivAt_gaussianNoiseOp_eq_inv_smul_ornsteinUhlenbeck, hasDerivAt_gaussianNoiseOp_eq_inv_smul_gaussianNoiseOp;
    • hasDerivAt_gaussianNoiseOp_exp_neg.

This PR also relies on hermiteCoeff_coeFn and hermiteBasis_repr_tsum_smul in HermiteExpansion.lean. Both belong to the base PR.

Reuse.

• The one-dimensional integration by parts is Stein's lemma (integral_sub_mul_gaussianReal) applied to f′g.
• The n-dimensional reduction uses MeasureTheory.measurePreserving_update and integral_integral_update from PiUpdate.lean.
• The L² statements use hermiteCoeff, hermiteBasis, hermiteBasis_repr and hermiteCoeff_gaussianNoiseOp from the base PR, together with Mathlib's abs_pow_sub_pow_le, hasDerivAt_pow, uniqueDiffWithinAt_Iic and tendsto_pow_const_mul_const_pow_of_abs_lt_one.
• The Duplicate-statement, Parallel-definition and Repeated-proof-block scans report nothing.

Source mapping ([O'Donnell 2014, §11.3])

• Def 11.24 (L f = d/dρ U_ρ f |_{ρ=1}):
  • ornsteinUhlenbeck is the Hermite series, and the theorems identify it with the derivative.
  • hasDerivWithinAt_gaussianNoiseOp gives the left L² derivative at ρ = 1.
  • eq_ornsteinUhlenbeck_of_hasDerivWithinAt shows that any left derivative equals L f.
  • hasDerivWithinAt_gaussianNoiseOp_exp_neg_zero is the form with ρ = e^{−t} at t = 0.
• Prop 11.26 (L f = x · ∇f − Δf): proved on the Hermite basis only (sum_mul_deriv_multiHermite_update_sub). It is not proved for general smooth f.
• Prop 11.27 (d/dρ U_ρ f = ρ⁻¹ L U_ρ f = ρ⁻¹ U_ρ L f), stated in L²:
  • For every f ∈ L² and |ρ| < 1, including ρ = 0, ρ ↦ U_ρ f is differentiable with derivative ∑ |α| ρ^{|α|−1} f̂(α) h_α (hasDerivAt_gaussianNoiseOp).
  • For ρ ≠ 0, that derivative is ρ⁻¹ L U_ρ f for every f ∈ L², and ρ⁻¹ U_ρ L f for f in the domain.
  • L U_ρ f = U_ρ L f holds as an equality in L² for |ρ| ≤ 1.
  • For f in the domain, the series derivative also holds within [−1, 1] at |ρ| ≤ 1, endpoints included (hasDerivWithinAt_Icc_gaussianNoiseOp).
  • The exponential-time form d/dt U_{e^{−t}} f = −L U_{e^{−t}} f holds for t > 0.
  • At ρ = 0 only the series form is stated, since ρ⁻¹ is undefined there.
  • The book derives the proposition from the semigroup law; here it is read off the Hermite expansion. Coordinates of difference quotients are dominated by |α| r^{|α|−1} |f̂(α)| for some |ρ| < r < 1, which is summable by 11.18(c).
• Prop 11.28 / Ex 11.8 (⟨L f, g⟩ = ⟨∇f, ∇g⟩): stated with explicit differentiability and integrability hypotheses instead of the book's C³-and-domain-of-L assumption.
• Prop 11.40 / Ex 11.18:
  • (L f)^(α) = |α| f̂(α) is hermiteBasis_repr_ornsteinUhlenbeck.
  • (a)/(b), the derivative exists iff ∑ |α|² f̂(α)² < ∞, is exists_hasDerivWithinAt_gaussianNoiseOp_iff.
  • (c), U_ρ f ∈ Dom L for |ρ| < 1, is memOrnsteinUhlenbeckDomain_gaussianNoiseOp.
• Ex 11.10(c) (the Hermite ODE): Polynomial.X_mul_derivative_hermite_sub.

Not formalized:

• Prop 11.26 for general smooth f;
• the symmetric form ⟨f, L g⟩ = ⟨L f, g⟩ of Prop 11.28 on L²;
• pointwise (rather than L²) derivatives of U_ρ f;
• L as a Mathlib unbounded operator (LinearPMap). Here it is a total function with a separate domain predicate.

Tests (CslibFrontierTests/GaussianOrnsteinUhlenbeck.lean)

• The Hermite equation for H_2 = X² − 1, and x h_1′ − h_1″ = x.
• The value 1 of integration by parts for f = g = id, for the coordinate of Unit → ℝ, and for z₀ on Fin 2 → ℝ.
• For f = h_β:
  • the coordinates of L h_β;
  • the left derivative at 1 and its uniqueness;
  • the t = 0 form;
  • the derivative at |ρ| < 1;
  • ρ⁻¹ L U_ρ h_β and ρ⁻¹ U_ρ L h_β at ρ = 1/2;
  • the coefficients of L U_{1/2} h_β;
  • the t > 0 form.
• f = ∑ n, (n + 1)⁻¹ h_n, which is in L² but outside the domain:
  • the failing direction of Ex 11.18: no left derivative at 1;
  • Ex 11.18(c): U_{1/2} f is in the domain;
  • Prop 11.27 at ρ = 1/2 without the domain.

Review. An independent review found no faithfulness problems with the conventions. This head applies its requested changes:

• Ex 11.18(c) is proved, and the unneeded domain hypotheses are dropped from the |ρ| < 1 and t > 0 derivative theorems.
• The ρ = e^{−t} parametrization is disclosed, and the t = 0 form is added.
• L is a definition with a named domain predicate, and the commutation and Prop 11.40 lemmas are in book form.
• The re-derived geometric-sum bound is replaced by abs_pow_sub_pow_le.
• The redundant import is dropped.
• Ex 11.10(c) is cited.
• The tests are concrete and include the failing direction.
• The manual wording is corrected.

Manual impact

• Operator's Manual: a new section in manual/workflows/probabilistic-workflows.md, "Differentiate Gaussian noise with the Ornstein–Uhlenbeck operator". It comes after "Expand Gaussian functions in the Hermite basis" and covers:

  • imports, namespaces and conventions;
  • the definition, the domain and how to build u;
  • every public name with its hypotheses;
  • the checked clients and the scope.

  "Integrate Hermite polynomials against a Gaussian" and "Compose Gaussian noise operators" now link to the new section.

• Agent Operator's Manual: no change, because this PR does not change a workflow, role or process.

ROADMAP: no change. The Boolean-analysis item (#2131) remains open, and no listed item is completed by this PR.

Validation (local, at the PR head)

• lake build --wfail CslibFrontier CslibFrontierTests.GaussianOrnsteinUhlenbeck CslibFrontierTests.GaussianHermiteExpansion CslibFrontierTests.GaussianHermite passes.
• These checks pass:
  • python3 -B scripts/check_hygiene.py --check-simp;
  • python3 -B scripts/check_operator_manual.py;
  • lake exe mk_all --check.
• python3 -B scripts/parallel_defs.py --theorems, python3 -B scripts/parallel_defs.py and python3 -B scripts/proof_copies.py report no candidates.
• The full scripts/check.sh passes.

AI assistance: drafted and ported with Claude Code. Agent-reviewed; human review pending.

🤖 Generated with Claude Code

[SamuelSchlesinger]

Agent review claim: coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913) is reviewing head b666a1c78f873b3b1bc010a0c27ee2f67e86bcce. This is agent review, not human review.

[SamuelSchlesinger]

Independent agent review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) at b666a1c78f873b3b1bc010a0c27ee2f67e86bcce: APPROVE (holding queue until ci-checks completes).

• Mathematical faithfulness & signs (OrnsteinUhlenbeck.lean, Hermite.lean, PiUpdate.lean). Verified every sign and normalization against O'Donnell (2014, §11.3): positive-semidefinite differential expression $L f = x \cdot \nabla f - \Delta f$ (X_mul_derivative_hermite_sub, mul_deriv_normalizedHermite_sub, sum_mul_deriv_multiHermite_update_sub), 1D and product-Gaussian integration by parts (integral_mul_deriv_sub_deriv_deriv_mul_gaussianReal, integral_sum_mul_deriv_update_sub_mul_pi_gaussianReal via ae_integrable_update), left $\rho$-derivative $+L f$ at $\rho = 1$ on Set.Iic 1, right $t$-derivative $-L f$ of $U_{e^{-t}} f$ at $t = 0$ on Set.Ici 0, and interior $\rho$- and $t$-derivatives (|\rho| < 1, including $\rho = 0$, and $t > 0$).
• Domain predicate & junk-value boundaries. MemOrnsteinUhlenbeckDomain cleanly separates $L^2(\gamma^n)$ inputs from $\operatorname{Dom}(L)$: ornsteinUhlenbeck_gaussianNoiseOp (|\rho| \le 1) and hasDerivAt_gaussianNoiseOp_eq_inv_smul_gaussianNoiseOp properly require hf : MemOrnsteinUhlenbeckDomain f (avoiding any tsum junk collapse outside $\operatorname{Dom}(L)$), while memOrnsteinUhlenbeckDomain_gaussianNoiseOp, hasDerivAt_gaussianNoiseOp_eq_inv_smul_ornsteinUhlenbeck, and hasDerivAt_gaussianNoiseOp_exp_neg require only MemLp f 2 \gamma on $|\rho| < 1$ / $t > 0$.
• Non-vacuity & counterexample (CslibFrontierTests/GaussianOrnsteinUhlenbeck.lean). Exercises concrete Hermite polynomials, 1D/product integration by parts evaluating to 1, basis vectors h_\beta, and the explicit counterexample slowVec = \sum_n (n+1)^{-1} h_n \in L^2(\gamma) \setminus \operatorname{Dom}(L) (no left derivative at 1, smoothed into $\operatorname{Dom}(L)$ and differentiable at \rho = 1/2).
• Both manuals & rendered PDF QA. Audited manual/workflows/probabilistic-workflows.md against all public declarations and scope limitations, visually inspected rendered pages 69–70 and 72–74 of cslib-frontier-operators-manual.pdf from workflow run 43369572650 (section 6.49 and cross-links in 6.46/6.47 render cleanly), and verified manual/AGENT_OPERATORS.md needs no edit.

This is agent review, not human review.