Fourth-moment bounds for clipping #
MeasureTheory.MemLp.max_min shows that clipping a real Lᵖ function to [-M, M], for
0 ≤ M, preserves Lᵖ membership for any measure. For M > 0,
MeasureTheory.Integrable.integral_sq_sub_max_min_le bounds the integrated squared clipping
error by the fourth moment divided by 16 M², using the pointwise inequality from
TauCeti.Algebra.Order.Field.Clipping. This controls the L² error of clipping Gaussian
linear observables in the truncation proof of Grothendieck's inequality.
The expression max (-M) (min M x) is the real-valued form of Set.projIcc.
References #
- F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §8.1.
theorem
MeasureTheory.MemLp.max_min
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
{p : ENNReal}
(hf : MemLp f p μ)
{M : ℝ}
(hM : 0 ≤ M)
:
Clipping a real Lᵖ function to a symmetric interval preserves Lᵖ membership,
without a finiteness assumption on the measure.
theorem
MeasureTheory.Integrable.integral_sq_sub_max_min_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf₄ : Integrable (fun (x : α) => f x ^ 4) μ)
{M : ℝ}
(hM : 0 < M)
:
The squared L² clipping error is bounded by the fourth moment divided by 16 M².