Scaled Cutoff Estimate

This auxiliary lemma gives a quantitative cutoff estimate for a closed weighted-gradient domain.

Let $V$ be finite-dimensional and complete, let $m$ be an additive Haar measure, let $\nu$ be log-concave with nonempty interior support, and let $U\in C^1(V)$ satisfy $\nu=m.\operatorname{tilted}(-U)$. Let $u\in L^2(\nu)$ satisfy:

1. For every smooth compactly supported $f$, the pairing of $u$ with $(A+1)f$ is zero, where $A=\overline{T}^{\dagger}\overline{T}$ is represented by adjointComp.
2. For every smooth compactly supported multiplier $\chi$, the class $\chi u$ belongs to $D(\overline{T})$.

If $r>0$, $M\ge0$, and the cutoff satisfies $\|\nabla\chi_r(y)\|\le M/r$ for all $y$, then

The cutoff family and the domain are represented by cutoff, toLp, and closedWeightedOperator. This is a technical estimate used to pass from local domain membership to global vanishing.

Original Lean declaration header

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

private theorem norm_toLp_mul_cutoff_le
    (hνU : (ν : Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 1 U) (u : (Lp ℝ 2 (ν : Measure V)))
    (horth : ∀ (f : V → ℝ) (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f),
      ⟪((adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi))
        ⟨_, hν.toLp_mem_adjointComp_domain m hi hνU hU hf hfc⟩ : (Lp ℝ 2 (ν : Measure V))), u⟫ +
        ⟪((memLp_of_contDiff_hasCompactSupport ν hf hfc).toLp f : (Lp ℝ 2 (ν : Measure V))), u⟫ = 0)
    (hloc : ∀ (χ : V → ℝ) (hχ : ContDiff ℝ ∞ χ) (hχc : HasCompactSupport χ),
      (memLp_mul_of_contDiff_hasCompactSupport (ν := ν) hχ hχc u).toLp _ ∈
        (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain)
    {r M : ℝ} (hr : 0 < r) (hM0 : 0 ≤ M)
    (hM : ∀ y : V, ‖gradient (cutoff (V := V) r) y‖ ≤ M / r) :
    ‖(memLp_mul_of_contDiff_hasCompactSupport (ν := ν) (contDiff_cutoff r)
        (hasCompactSupport_cutoff hr) u).toLp _‖ ≤ (M / r) * ‖u‖

Module navigation

Module: KLS/LogConcave/HeatSemigroup/OperatorCore.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, KLS/LogConcave/HeatSemigroup/Generator, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Energy/WeightedGradient/Core, KLS/LogConcave/WeightedGradient/Multiplier.

Supporting theorems: weightedLaplacian_eq_zero_of_notMem_tsupport, exists_mem_domain_closedWeightedOperator_toLp_mul, exists_seq_smooth_tendsto_graph.

Next: eq_zero_of_localRegularity.

Source excerpt, lines 190–202 · Frozen source 408915f.