Tail Primitive of a Compactly Supported Cutoff

Let $w:\mathbb R\to\mathbb R$ be smooth, nonnegative everywhere, and zero whenever $t\le0$ or $t\ge3$. Let $R>0$ and define

$$q_R(t)=R^{-1}\int_{t/R}^{3}w(s)\,ds.$$

Then $q_R$ is smooth,

$$q_R'(t)=-R^{-2}w(t/R),$$

$0\le q_R(t)$ for every $t$, and

$$q_R(t)\le R^{-1}\int_0^3w(s)\,ds.$$

Finally, $q_R(t)=0$ whenever $3R\le t$.

This scalar profile is a reusable cutoff component for noncompact integration by parts.

Original Lean declaration header

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

theorem inv_mul_intervalIntegral_div_three_cutoff {w : ℝ → ℝ} (hw : ContDiff ℝ ∞ w)
    (hw0 : ∀ t, 0 ≤ w t) (hws : ∀ t, t ≤ 0 ∨ 3 ≤ t → w t = 0) {R : ℝ} (hR : 0 < R) :
    ContDiff ℝ ∞ (fun t => R⁻¹ * ∫ s in t / R..3, w s) ∧
      (∀ t, deriv (fun t => R⁻¹ * ∫ s in t / R..3, w s) t = -((R ^ 2)⁻¹ * w (t / R))) ∧
      (∀ t, 0 ≤ R⁻¹ * ∫ s in t / R..3, w s) ∧
      (∀ t, R⁻¹ * ∫ s in t / R..3, w s ≤ R⁻¹ * ∫ s in (0 : ℝ)..3, w s) ∧
      (∀ t, 3 * R ≤ t → R⁻¹ * ∫ s in t / R..3, w s = 0)

Module navigation

Module: Analysis/Cutoff/Profile.

Previous: exists_majorant_abs_deriv_deriv_smoothTransition_two_sub · Next: deriv_comp_sub_div_and_deriv_deriv.

Source excerpt, lines 237–243 · Frozen source 408915f.

Literature

This formalizes Lemma A.4 of Letwin (arXiv:2607.24164v1), p. 17, for its scalar tail primitive.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Cutoff_Profile

open scoped ContDiff

theorem FunctionalInequalities.Analysis.inv_mul_intervalIntegral_div_three_cutoff_readable {w : ℝ → ℝ} (hw : ContDiff ℝ ∞ w)
    (hw0 : ∀ t, 0 ≤ w t) (hws : ∀ t, t ≤ 0 ∨ 3 ≤ t → w t = 0) {R : ℝ} (hR : 0 < R) :
    ContDiff ℝ ∞ (fun t => R⁻¹ * ∫ s in t / R..3, w s) ∧
      (∀ t, deriv (fun t => R⁻¹ * ∫ s in t / R..3, w s) t = -((R ^ 2)⁻¹ * w (t / R))) ∧
      (∀ t, 0 ≤ R⁻¹ * ∫ s in t / R..3, w s) ∧
      (∀ t, R⁻¹ * ∫ s in t / R..3, w s ≤ R⁻¹ * ∫ s in (0 : ℝ)..3, w s) ∧
      (∀ t, 3 * R ≤ t → R⁻¹ * ∫ s in t / R..3, w s = 0) := by sorry