Centered Noise Does Not Decrease Quadratic Variance

This is a convolution monotonicity statement for quadratic-form variance.

Let $E$ be a complete real inner-product normed space with Borel and second-countable structure. Let $\mu$ and $\nu$ be probability measures on $E$, each with finite fourth moment, and assume the mean of $\nu$ is zero. For any continuous linear map $A:E\to E$,

Here Measure.conv is the law of the sum of independent variables with laws $\mu$ and $\nu$. The result is a reusable variance comparison and does not assert any constant bound.

Original Lean declaration header

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

set_option maxHeartbeats 500000 in
theorem quadratic_variance_le_centered_noise_convolution
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
    (mu nu : ProbabilityMeasure E)
    (hmu4 : MemLp (id : E → E) 4 (mu : Measure E))
    (hnu4 : MemLp (id : E → E) 4 (nu : Measure E))
    (hmean : (∫ z, z ∂(nu : Measure E)) = 0) (A : E →L[ℝ] E) :
    variance (fun x : E => ⟪A x, x⟫) (mu : Measure E) ≤
      variance (fun x : E => ⟪A x, x⟫) ((mu : Measure E).conv (nu : Measure E))

Module navigation

Module: Probability/QuadraticVariance.

Supporting theorems: memLp_quadratic_of_memLp_four, decomposition.

Previous: tendsto_variance_quadratic_matrix_forms.

Source excerpt, lines 96–105 · Frozen source 408915f.