First and Second Integral Convergence Under Scaled Cutoffs

This statement gives convergence of the first and second integrals of cutoff products.

Let $E$ be a real inner product space with its Borel measurable structure, let $\mu$ be a finite measure on $E$, and let $f:E\to\mathbb R$ satisfy MemLp f 2 μ, including almost-everywhere strong measurability and finite $L^2$ seminorm. Write $\chi_R$ for Energy.Euclidean.LipschitzApproximation.scaled R.

Both limits hold as $n\in\mathbb N$ tends to infinity:

These two scalar convergence statements support variance approximation by cutoff functions.

Formalization Note Neither completeness nor finite dimensionality of $E$ is assumed here. The conclusion is a conjunction of integral limits, not a statement of $L^2$-norm convergence.

Original Lean declaration header

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

theorem tendsto_integral_scaled_mul {μ : Measure E} [IsFiniteMeasure μ] {f : E → ℝ}
    (hf : MemLp f 2 μ) :
    Tendsto (fun n : ℕ => ∫ x, Energy.Euclidean.LipschitzApproximation.scaled ((n : ℝ) + 1) x * f x ∂μ)
        atTop (𝓝 (∫ x, f x ∂μ)) ∧
      Tendsto (fun n : ℕ =>
          ∫ x, (Energy.Euclidean.LipschitzApproximation.scaled ((n : ℝ) + 1) x * f x) ^ 2 ∂μ)
        atTop (𝓝 (∫ x, f x ^ 2 ∂μ))

Module navigation

Module: Poincare/SmoothTest/WeakLimit.

Definition modules: Analysis/Cutoff/SmoothBall.

Previous: Admissible.of_contDiff_hasCompactSupport · Next: norm_gradient_scaled_mul_sq_le.

Source excerpt, lines 201–207 · Frozen source 408915f.