Subtracting an Affine-Orthogonal Part From an Orthogonal Function

This lemma gives an exact function identity for affine subtraction when the first function is orthogonal to affine functions.

Let $n\in\mathbb N$, $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)), and $\mu$ a probability measure on $E$. Assume:

1. $\operatorname{id}\in L^2(\mu)$.
2. $f,g:E\to\mathbb R$ belong to $L^2(\mu)$.
3. $\int f\,d\mu=0$ and $\int\langle u,x\rangle f(x)\,d\mu=0$ for every $u\in E$.

For any function $h$, write $\widetilde h=$ affineOrthPart $\mu\ h$, defined by subtracting $\int h\,d\mu$ and $\sum_j(\int\langle e_j,y\rangle h(y)\,d\mu(y))\langle e_j,\cdot\rangle$, where $(e_j)$ is the standard orthonormal basis. Then, as functions on $E$,

This identity is useful for comparing affine-subtracted approximations. It is pointwise, not merely almost everywhere, and requires neither centering nor identity covariance of $\mu$.

Original Lean declaration header

Within namespace FunctionalInequalities.L2. Shown in its original module context. Proof omitted.

theorem sub_affineOrthPart_eq (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) {f g : EuclideanSpace ℝ (Fin n) → ℝ} (hf : MemLp f 2 μ)
    (hf0 : ∫ x, f x ∂μ = 0) (hfx : ∀ u, ∫ x, ⟪u, x⟫ * f x ∂μ = 0) (hg : MemLp g 2 μ) :
    f - affineOrthPart μ g = affineOrthPart μ (f - g)

Module navigation

Module: L2/AffineDecomposition.

Previous: integral_inner_mul_affineOrthPart · Next: contDiff_affineOrthPart.

Source excerpt, lines 480–483 · Frozen source 408915f.