Squared Gradient Bound for a Scaled Cutoff Product

This is a pointwise estimate for the gradient of a function multiplied by the designated scaled cutoff.

Let $E$ be a finite-dimensional complete real inner product space. Denote the fixed bump Energy.Euclidean.LipschitzApproximation.bump by $\beta$, and its scaled cutoff Energy.Euclidean.LipschitzApproximation.scaled R by $\chi_R$. Assume:

1. $R,M\in\mathbb R$ and $R>0$.
2. $\|D\beta(y)\|\le M$ for every $y\in E$, where the norm is the operator norm of the Fréchet derivative.
3. $f:E\to\mathbb R$ is differentiable at $x\in E$.

Then

This technical estimate controls the energy contribution introduced by cutoff multiplication. It requires no measure or global differentiability assumption on $f$.

Original Lean declaration header

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

theorem norm_gradient_scaled_mul_sq_le {R M : ℝ} (hR : 0 < R)
    (hM : ∀ x : E, ‖fderiv ℝ (⇑(Energy.Euclidean.LipschitzApproximation.bump (E := E))) x‖ ≤ M)
    {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) :
    ‖gradient (fun y => Energy.Euclidean.LipschitzApproximation.scaled R y * f y) x‖ ^ 2 ≤
      2 * ‖gradient f x‖ ^ 2 + 2 * (M / R) ^ 2 * f x ^ 2

Module navigation

Module: Poincare/SmoothTest/WeakLimit.

Definition modules: Analysis/Cutoff/SmoothBall.

Previous: tendsto_integral_scaled_mul · Next: tendsto_energy_scaled_mul.

Source excerpt, lines 343–347 · Frozen source 408915f.