Energy Convergence of Scaled Cutoff Products

This statement gives convergence of smooth-test energies under the designated expanding cutoffs.

Let $E$ be a finite-dimensional complete real inner product space with its Borel measurable structure and $\mu$ a finite measure. Let $f:E\to\mathbb R$ be admissible (Poincare.SmoothTest.Admissible): $f$ is $C^\infty$, belongs to $L^2(\mu)$, and $\|\nabla f\|^2$ is integrable. For $R>0$, let $\chi_R$ denote Energy.Euclidean.LipschitzApproximation.scaled R. Define the energy (Poincare.SmoothTest.energy) by $\mathcal E_\mu(g)=\int\|\nabla g\|^2\,d\mu$.

As $n\in\mathbb N$ tends to infinity,

This is an energy approximation statement for extending inequalities from compactly supported smooth tests to admissible tests. The energy has no factor of $1/2$.

Original Lean declaration header

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

theorem tendsto_energy_scaled_mul {μ : Measure E} [IsFiniteMeasure μ] {f : E → ℝ}
    (hf : Admissible μ f) :
    Tendsto (fun n : ℕ =>
        energy μ (fun x => Energy.Euclidean.LipschitzApproximation.scaled ((n : ℝ) + 1) x * f x))
      atTop (𝓝 (energy μ f))

Module navigation

Module: Poincare/SmoothTest/WeakLimit.

Definition modules: Analysis/Cutoff/SmoothBall, Poincare/SmoothTest/Basic.

Supporting theorems: norm_gradient_scaled_mul_sq_le.

Previous: norm_gradient_scaled_mul_sq_le · Next: Holds.of_compactSupport.

Source excerpt, lines 422–426 · Frozen source 408915f.