Quadratic Forms Preserve $L^4$ Integrability at Exponent $2$

This is a general moment-transfer lemma for quadratic forms.

Let $(\alpha,\mu)$ be a measurable space with a measure, let $E$ be a real inner-product normed group, let $f:\alpha\to E$ satisfy MemLp f 4 μ, and let $A:E\to E$ be a continuous linear map. Then the scalar quadratic form $x\mapsto\langle A(f(x)),f(x)\rangle$ belongs to MemLp with exponent $2$:

The lemma is a reusable integrability fact for quadratic observables, with no probability, finite-dimensionality, or measurability assumption on $f$ beyond the stated MemLp hypothesis.

Original Lean declaration header

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

set_option maxHeartbeats 300000 in
theorem memLp_quadratic_of_memLp_four {alpha E : Type*} [MeasurableSpace alpha]
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] {mu : Measure alpha}
    {f : alpha → E} (hf : MemLp f 4 mu) (A : E →L[ℝ] E) :
    MemLp (fun x => ⟪A (f x), f x⟫) 2 mu

Module navigation

Module: Probability/Moments.

Previous: sum_variance_entries_eq_integral_trace_sub_trace_mean.

Source excerpt, lines 509–513 · Frozen source 408915f.