Squared-Distance Characterization of a Scalar Multiple

This statement is an auxiliary Hilbert-space argument. Let $x,y:Ω→ℝ$ belong to MemLp with exponent $2$ under a measure $P$. Let $c∈ℝ$ and let $X,Y,Z∈[0,∞]$ be the squared ENNReal integrals of $x$, $y$, and $x-y$, respectively. Assume

1. $X=\int\|x\|^2dP$, $Y=\int\|y\|^2dP$, and $Z=\int\|x-y\|^2dP$;
2. $X.toReal=c^2Y.toReal$;
3. $Z.toReal=(c-1)^2Y.toReal$.

Then

The result uses toReal on the ENNReal quantities and requires only the stated MemLp assumptions, not that $P$ be a probability measure. It is a reusable uniqueness criterion for identifying scalar multiples from squared distances.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.

theorem ae_eq_const_mul_of_sq_distances {x y : Ω → ℝ} (hx : MemLp x 2 P) (hy : MemLp y 2 P)
    {c : ℝ} {X Y Z : ℝ≥0∞}
    (hSx : ∫⁻ ω, (‖x ω‖₊ : ℝ≥0∞) ^ 2 ∂P = X)
    (hSy : ∫⁻ ω, (‖y ω‖₊ : ℝ≥0∞) ^ 2 ∂P = Y)
    (hSxy : ∫⁻ ω, (‖x ω - y ω‖₊ : ℝ≥0∞) ^ 2 ∂P = Z)
    (hXY : X.toReal = c ^ 2 * Y.toReal) (hZY : Z.toReal = (c - 1) ^ 2 * Y.toReal) :
    x =ᵐ[P] fun ω => c * y ω

Module navigation

Module: LevyStochCalc/Brownian/ItoLinear.

Previous: stochasticIntegralBrownian_add · Next: stochasticIntegralBrownian_const_mul.

Source excerpt, lines 300–306 · Frozen source 408915f.