The comparison energy inequality: a spatial truncation for the Kato regularization

CIV.Comparison.EnergyInequality proves the support/integrability facts about comparisonEnergy and the Grönwall step of lem:aniso:comparison, but takes the integrated energy inequality eq:aniso:comparison:positive:energy as a hypothesis (hineq of comparisonEnergy_le_exp_mul_integral_sq). CIV.Comparison.EnergyInequality2 proves that this integrated inequality follows once the mollified equation eq:aniso:comparison:mollified (mollified_equation) is upgraded from a distributional identity in time into a fundamental-theorem-of-calculus statement, and records that the natural closed form for the Kato regularization, Φ_κ(g) = (g + √(g² + κ²)) / 2 − κ / 2, does not tend to 0 as g → -∞: it tends to -κ / 2. Composing Φ_κ with the excess g = q_ε − Ψ_σ directly (unbounded below away from the compact support of v_ε = g₊) therefore gives an energy ∫ Φ_κ(g)² that diverges over all of Vec m, for every fixed κ > 0, since the integrand tends to the nonzero constant κ² / 4 over infinite measure. A κ-independent spatial truncation is needed before the Kato step, not a regularization of the unbounded difference g on the whole space.

Main results

• The truncation. mollifierCutoff m R is a smooth cutoff on Vec m, built as a product of one-dimensional profiles kappaBump1D R (one per coordinate, using Vec m's sup norm): it is 1 on closedBall 0 R, supported in closedBall 0 (2 * R), and valued in [0, 1] (contDiff_mollifierCutoff, mollifierCutoff_eq_one, hasCompactSupport_mollifierCutoff, mollifierCutoff_nonneg, mollifierCutoff_le_one). Once R is fixed at or above the support radius Minf / σ of BarrierSupport.posPart_mollifySlice_sub_barrier_eq_zero, multiplying comparisonPosPart by the cutoff does not change it at all, for every x (comparisonPosPart_mul_mollifierCutoff_eq_self): this is an exact pointwise identity, not a limit, and its squared form shows the truncated energy equals comparisonEnergy exactly (integral_sq_mul_mollifierCutoff_eq_comparisonEnergy). Consequently no limit R → ∞ is needed anywhere below: R is fixed once, at any value ≥ Minf / σ. The Kato regularization of the excess, multiplied by the cutoff, is smooth and compactly supported for every κ > 0 (contDiff_kappaProfile_mul_mollifierCutoff, hasCompactSupport_kappaProfile_mul_mollifierCutoff) — the divergence described above is exactly what the cutoff repairs.

• The Kato profile as a real-variable function. katoSmooth's second argument has type ℝ → ℝ, so the spatial composition needs kappaProfile kap := katoSmooth kap id : ℝ → ℝ applied to the excess g x, not katoSmooth itself applied to a function of Vec m. kappaProfile kap is smooth, its derivative has the closed form (1 + t / √(t² + κ²)) / 2 ∈ [0, 1], and it is globally 1-Lipschitz (hasDerivAt_kappaProfile, lipschitzWith_kappaProfile).

• A fundamental theorem of calculus for the squared Kato profile of a primitive. If F satisfies F τ = F τ₀ + ∫ h on an open set, (kappaProfile kap ∘ F)² obeys the same kind of identity, with right side the chain-rule derivative 2 Φ_κ(F) Φ_κ'(F) h (sq_kappaProfile_eq_add_intervalIntegral). The proof shows F is absolutely continuous (a primitive of an interval-integrable function), transports absolute continuity through the globally-Lipschitz kappaProfile kap (LipschitzWith.comp_absolutelyContinuousOnInterval), computes the a.e. derivative of the square by the chain rule, and applies the fundamental theorem of calculus for absolutely continuous functions (AbsolutelyContinuousOnInterval.integral_deriv_eq_sub).

• The pointwise-in-x upgrade of the mollified equation. Applying CIV.eq_add_intervalIntegral_of_pairing_eq to mollified_equation's tested identity (with no adapter: the two shapes match exactly) shows that, for a fixed spatial point x, mollifySlice m ε q (x, ·) is literally the primitive of the right side of eq:aniso:comparison:mollified (mollifySlice_eq_add_intervalIntegral). Since the barrier is affine in τ with the constant rate σ * K, the excess g = q_ε − Ψ_σ obeys the same kind of primitive identity, with the constant σ * K subtracted from the right side (excess_eq_add_intervalIntegral) — this part needs no calculus at all, only the closed form of barrier.

• Their combination: the per-x, per-κ truncated energy-density identity (truncatedKatoSq_eq_add_intervalIntegral), obtained by feeding the excess's primitive identity into the fundamental theorem of calculus for the squared Kato profile and multiplying through by the (τ-independent) constant mollifierCutoff m R x.

Hypotheses hCont and hLoc

Invoking eq_add_intervalIntegral_of_pairing_eq at a fixed spatial point x requires ContinuousOn (fun τ => mollifySlice m ε q (x, τ)) I and local integrability on I of the right side of eq:aniso:comparison:mollified at x. These enter mollifySlice_eq_add_intervalIntegral, excess_eq_add_intervalIntegral and truncatedKatoSq_eq_add_intervalIntegral as the explicit hypotheses hCont and hLoc. CIV.mollifySlice_ae_ae_sub_eq_intervalIntegral proves the corresponding identity, almost everywhere in time, without them.

Use

The per-x identity is integrated over Vec m in CIV.Comparison.EnergySpatialIntegration, where the Green identity for the truncated Laplacian is available in both directions (integral_partialLaplacian_mul_eq_neg_integral_gradPair_mul, integrating by parts off the differentiated factor, and integral_mul_lapD_eq, off the test factor). They combine into integral_partialLaplacian_mul_comm_of_hasCompactSupport, the form needed when the differentiated factor is smooth but not compactly supported, as mollifySlice is. The spatial integration of the Laplacian term is integral_kappaTestFn_mul_partialLaplacian_eq, and the κ ↓ 0 interchange with the outer time integral is tendsto_intervalIntegral_integral_sq_kappaProfile_mul_mollifierCutoff; both use mollifierCutoff and kappaProfile from this file.

Vec m's ambient norm is the sup norm (the default Pi structure on Fin m → ℝ), so the cutoff is built as a literal product of one-dimensional profiles rather than through ContDiffBump (0 : Vec m).

Part 1: the spatial cutoff

theorem CIV.contDiff_finset_prod {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {n : WithTop ℕ∞} (s : Finset ι) {f : ι → E → ℝ} (hf : ∀ i ∈ s, ContDiff ℝ n (f i)) : ContDiff ℝ n fun (x : E) => ∏ i ∈ s, f i x

A smooth product of finitely many smooth real functions, composed with coordinate projections, is smooth.

noncomputable def CIV.kappaBump1D (R : ℝ) : ℝ → ℝ

The one-dimensional smooth cutoff of scale R: equal to 1 on closedBall 0 R, supported in ball 0 (2 * R), ranging in [0, 1]. The junk value off 0 < R is 0.

Equations

• CIV.kappaBump1D R t = if h : 0 < R then ↑{ rIn := R, rOut := 2 * R, rIn_pos := h, rIn_lt_rOut := ⋯ } t else 0

theorem CIV.kappaBump1D_eq (R : ℝ) (hR : 0 < R) (t : ℝ) : kappaBump1D R t = ↑{ rIn := R, rOut := 2 * R, rIn_pos := hR, rIn_lt_rOut := ⋯ } t

theorem CIV.contDiff_kappaBump1D (R : ℝ) (hR : 0 < R) : ContDiff ℝ (↑⊤) (kappaBump1D R)

theorem CIV.kappaBump1D_nonneg (R : ℝ) (hR : 0 < R) (t : ℝ) : 0 ≤ kappaBump1D R t

theorem CIV.kappaBump1D_le_one (R : ℝ) (hR : 0 < R) (t : ℝ) : kappaBump1D R t ≤ 1

theorem CIV.kappaBump1D_eq_one (R : ℝ) (hR : 0 < R) {t : ℝ} (ht : |t| ≤ R) : kappaBump1D R t = 1

theorem CIV.kappaBump1D_eq_zero (R : ℝ) (hR : 0 < R) {t : ℝ} (ht : 2 * R ≤ |t|) : kappaBump1D R t = 0

noncomputable def CIV.mollifierCutoff (m : ℕ) (R : ℝ) (x : CKN.Vec m) : ℝ

The spatial cutoff of scale R on Vec m: the product of the one-dimensional cutoffs kappaBump1D R applied to each coordinate. Equal to 1 on closedBall 0 R, supported in closedBall 0 (2 * R), ranging in [0, 1]. Built as a literal product over coordinates because Vec m's ambient norm is the Pi sup norm, for which closedBall 0 R is exactly the box {x | ∀ i, |x i| ≤ R}.

Equations

• CIV.mollifierCutoff m R x = ∏ i : Fin m, CIV.kappaBump1D R (x i)

theorem CIV.finset_prod_le_one_of_forall_mem_Icc {ι : Type u_1} (s : Finset ι) {f : ι → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i ∧ f i ≤ 1) : ∏ i ∈ s, f i ≤ 1

A finite product of real numbers each lying in [0, 1] itself lies in [0, 1].

theorem CIV.contDiff_mollifierCutoff (m : ℕ) (R : ℝ) (hR : 0 < R) : ContDiff ℝ (↑⊤) (mollifierCutoff m R)

theorem CIV.mollifierCutoff_nonneg (m : ℕ) (R : ℝ) (hR : 0 < R) (x : CKN.Vec m) : 0 ≤ mollifierCutoff m R x

theorem CIV.mollifierCutoff_le_one (m : ℕ) (R : ℝ) (hR : 0 < R) (x : CKN.Vec m) : mollifierCutoff m R x ≤ 1

theorem CIV.mollifierCutoff_eq_one (m : ℕ) (R : ℝ) (hR : 0 < R) {x : CKN.Vec m} (hx : x ∈ Metric.closedBall 0 R) : mollifierCutoff m R x = 1

theorem CIV.mollifierCutoff_eq_zero (m : ℕ) (R : ℝ) (hR : 0 < R) {x : CKN.Vec m} (hx : x ∉ Metric.closedBall 0 (2 * R)) : mollifierCutoff m R x = 0

theorem CIV.hasCompactSupport_mollifierCutoff (m : ℕ) (R : ℝ) (hR : 0 < R) : HasCompactSupport (mollifierCutoff m R)

Part 2: the truncation is exact once R ≥ Minf / σ — no R → ∞ limit

theorem CIV.comparisonPosPart_mul_mollifierCutoff_eq_self {m : ℕ} {ε M σ K τ₀ τ Minf R : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) (hR : 0 < R) (hRM : Minf / σ ≤ R) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) (x : CKN.Vec m) : comparisonPosPart m ε M σ K τ₀ q (x, τ) * mollifierCutoff m R x = comparisonPosPart m ε M σ K τ₀ q (x, τ)

Stage (1) of the truncation. Once R dominates the support radius Minf / σ of BarrierSupport.posPart_mollifySlice_sub_barrier_eq_zero, the cutoff mollifierCutoff m R is identically 1 on the excess comparisonPosPart, for every x — not merely in a limit as R → ∞. Multiplying by the cutoff therefore does not change comparisonPosPart at all.

theorem CIV.sq_comparisonPosPart_mul_mollifierCutoff_eq_self {m : ℕ} {ε M σ K τ₀ τ Minf R : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) (hR : 0 < R) (hRM : Minf / σ ≤ R) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) (x : CKN.Vec m) : (comparisonPosPart m ε M σ K τ₀ q (x, τ) * mollifierCutoff m R x) ^ 2 = comparisonPosPart m ε M σ K τ₀ q (x, τ) ^ 2

The squared form of comparisonPosPart_mul_mollifierCutoff_eq_self: the truncated energy density equals the untruncated one, exactly, for the fixed R ≥ Minf / σ.

theorem CIV.integral_sq_mul_mollifierCutoff_eq_comparisonEnergy {m : ℕ} {ε M σ K τ₀ τ Minf R : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) (hR : 0 < R) (hRM : Minf / σ ≤ R) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) : ∫ (x : CKN.Vec m), (comparisonPosPart m ε M σ K τ₀ q (x, τ) * mollifierCutoff m R x) ^ 2 = comparisonEnergy m ε M σ K τ₀ q τ

The truncated energy equals comparisonEnergy exactly, for every R ≥ Minf / σ: no limit R → ∞ is needed once R is fixed at or above the support radius of comparisonPosPart.

Part 3: the real-variable Kato profile

noncomputable def CIV.kappaProfile (kap : ℝ) : ℝ → ℝ

The real-variable Kato profile Φ_κ(t) = (t + √(t² + κ²)) / 2 − κ / 2: katoSmooth kap applied to the identity, so that spatial compositions x ↦ Φ_κ(g x) (for g : Vec m → ℝ) can be written kappaProfile kap (g x) — katoSmooth itself only accepts a function of ℝ.

Equations

• CIV.kappaProfile kap = CIV.katoSmooth kap id

theorem CIV.kappaProfile_eq (kap t : ℝ) : kappaProfile kap t = (t + √(t ^ 2 + kap ^ 2)) / 2 - kap / 2

theorem CIV.contDiff_kappaProfile (kap : ℝ) (hkap : 0 < kap) : ContDiff ℝ (↑⊤) (kappaProfile kap)

theorem CIV.hasDerivAt_kappaProfile (kap : ℝ) (hkap : 0 < kap) (t : ℝ) : HasDerivAt (kappaProfile kap) ((1 + t / √(t ^ 2 + kap ^ 2)) / 2) t

The derivative of the Kato profile in closed form.

theorem CIV.deriv_kappaProfile (kap : ℝ) (hkap : 0 < kap) (t : ℝ) : deriv (kappaProfile kap) t = (1 + t / √(t ^ 2 + kap ^ 2)) / 2

theorem CIV.deriv_kappaProfile_mem_Icc (kap : ℝ) (hkap : 0 < kap) (t : ℝ) : 0 ≤ deriv (kappaProfile kap) t ∧ deriv (kappaProfile kap) t ≤ 1

The derivative of the Kato profile lies in [0, 1].

theorem CIV.lipschitzWith_kappaProfile (kap : ℝ) (hkap : 0 < kap) : LipschitzWith 1 (kappaProfile kap)

The Kato profile is globally 1-Lipschitz.

Part 4: the fundamental theorem of calculus for the squared Kato profile

theorem CIV.sq_kappaProfile_eq_add_intervalIntegral {kap : ℝ} (hkap : 0 < kap) {I : Set ℝ} (hI : IsOpen I) {F h : ℝ → ℝ} {τ₀ : ℝ} (hF : ∀ τ ∈ I, F τ = F τ₀ + ∫ (s : ℝ) in τ₀..τ, h s) {a b : ℝ} (hab : a ≤ b) (habI : Set.Icc a b ⊆ I) (hτ₀ab : τ₀ ∈ Set.Icc a b) (hh : IntervalIntegrable h MeasureTheory.volume a b) : kappaProfile kap (F b) ^ 2 = kappaProfile kap (F a) ^ 2 + ∫ (s : ℝ) in a..b, 2 * kappaProfile kap (F s) * deriv (kappaProfile kap) (F s) * h s

If F obeys the primitive identity F τ = F τ₀ + ∫ s in τ₀..τ, h s throughout an open set I, and [a, b] ⊆ I with τ₀ ∈ [a, b], then the squared Kato regularization (kappaProfile kap ∘ F)² obeys the same kind of identity on [a, b], with right side the chain-rule derivative 2 · kappaProfile kap (F s) · deriv (kappaProfile kap) (F s) · h s.

Part 5: the pointwise-in-x upgrade of the mollified equation

theorem CIV.mollifySlice_eq_add_intervalIntegral {m d : ℕ} {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) (heq : IsDistributionalDriftDiffusion m d I B divB q) {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) (hCont : ContinuousOn (fun (τ : ℝ) => mollifySlice m ε q (x, τ)) I) (hLoc : MeasureTheory.LocallyIntegrableOn (fun (τ : ℝ) => partialLaplacian m d (mollifySlice m ε q) (x, τ) - gradPair m (mollifySlice m ε q) (x, τ) (B (x, τ)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, τ)) (fun (y : CKN.Vec m) => divB (y, τ)) (fun (y : CKN.Vec m) => q (y, τ)) x) I MeasureTheory.volume) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) {τ : ℝ} (hτ : τ ∈ I) : mollifySlice m ε q (x, τ) = mollifySlice m ε q (x, τ₀) + ∫ (s : ℝ) in τ₀..τ, partialLaplacian m d (mollifySlice m ε q) (x, s) - gradPair m (mollifySlice m ε q) (x, s) (B (x, s)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, s)) (fun (y : CKN.Vec m) => divB (y, s)) (fun (y : CKN.Vec m) => q (y, s)) x

The mollified slice is a primitive in time, under the hypotheses hCont and hLoc. For a fixed spatial point x, the mollified slice mollifySlice m ε q (x, ·) is literally the primitive, based at any τ₀ ∈ I, of the right side of eq:aniso:comparison:mollified — this upgrades mollified_equation's tested (distributional) identity into an equality of real numbers, via the general distributional fundamental theorem of calculus eq_add_intervalIntegral_of_pairing_eq. The two shapes match with no adapter.

theorem CIV.excess_eq_add_intervalIntegral {m d : ℕ} {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) (heq : IsDistributionalDriftDiffusion m d I B divB q) {ε : ℝ} (hε : 0 < ε) (M σ K : ℝ) (x : CKN.Vec m) (hCont : ContinuousOn (fun (τ : ℝ) => mollifySlice m ε q (x, τ)) I) (hLoc : MeasureTheory.LocallyIntegrableOn (fun (τ : ℝ) => partialLaplacian m d (mollifySlice m ε q) (x, τ) - gradPair m (mollifySlice m ε q) (x, τ) (B (x, τ)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, τ)) (fun (y : CKN.Vec m) => divB (y, τ)) (fun (y : CKN.Vec m) => q (y, τ)) x) I MeasureTheory.volume) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) {τ : ℝ} (hτ : τ ∈ I) : mollifySlice m ε q (x, τ) - barrier m M σ K τ₀ (x, τ) = mollifySlice m ε q (x, τ₀) - barrier m M σ K τ₀ (x, τ₀) + ∫ (s : ℝ) in τ₀..τ, partialLaplacian m d (mollifySlice m ε q) (x, s) - gradPair m (mollifySlice m ε q) (x, s) (B (x, s)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, s)) (fun (y : CKN.Vec m) => divB (y, s)) (fun (y : CKN.Vec m) => q (y, s)) x - σ * K

The excess g = q_ε − Ψ_σ over the barrier, as a function of τ at the fixed spatial point x, obeys the same kind of primitive identity as mollifySlice: the barrier is affine in τ with the constant rate σ * K (Barrier.barrier, unfolded directly — no calculus is needed for this part).

Part 6: the per-x, per-κ truncated energy-density identity

theorem CIV.truncatedKatoSq_eq_add_intervalIntegral {m d : ℕ} {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) (heq : IsDistributionalDriftDiffusion m d I B divB q) {ε : ℝ} (hε : 0 < ε) (M σ K : ℝ) (x : CKN.Vec m) (R kap : ℝ) (hkap : 0 < kap) (hCont : ContinuousOn (fun (τ : ℝ) => mollifySlice m ε q (x, τ)) I) (hLoc : MeasureTheory.LocallyIntegrableOn (fun (τ : ℝ) => partialLaplacian m d (mollifySlice m ε q) (x, τ) - gradPair m (mollifySlice m ε q) (x, τ) (B (x, τ)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, τ)) (fun (y : CKN.Vec m) => divB (y, τ)) (fun (y : CKN.Vec m) => q (y, τ)) x) I MeasureTheory.volume) {τ₀ τ : ℝ} (hτ₀ : τ₀ ∈ I) (hτ : τ ∈ I) (hτord : τ₀ ≤ τ) : (kappaProfile kap (mollifySlice m ε q (x, τ) - barrier m M σ K τ₀ (x, τ)) * mollifierCutoff m R x) ^ 2 = (kappaProfile kap (mollifySlice m ε q (x, τ₀) - barrier m M σ K τ₀ (x, τ₀)) * mollifierCutoff m R x) ^ 2 + ∫ (s : ℝ) in τ₀..τ, 2 * kappaProfile kap (mollifySlice m ε q (x, s) - barrier m M σ K τ₀ (x, s)) * deriv (kappaProfile kap) (mollifySlice m ε q (x, s) - barrier m M σ K τ₀ (x, s)) * (partialLaplacian m d (mollifySlice m ε q) (x, s) - gradPair m (mollifySlice m ε q) (x, s) (B (x, s)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, s)) (fun (y : CKN.Vec m) => divB (y, s)) (fun (y : CKN.Vec m) => q (y, s)) x - σ * K) * mollifierCutoff m R x ^ 2

Combines excess_eq_add_intervalIntegral (the excess is its own primitive) with sq_kappaProfile_eq_add_intervalIntegral (the chain rule/fundamental theorem of calculus for its squared Kato regularization) and multiplies through by the constant mollifierCutoff m R x: the per-x, per-κ identity that the energy computation integrates spatially (integral_kappaTestFn_mul_partialLaplacian_eq).

Part 7: the truncated Kato test function is smooth and compactly supported

theorem CIV.hasCompactSupport_kappaProfile_mul_mollifierCutoff {m : ℕ} {ε M σ K τ₀ τ R kap : ℝ} (hR : 0 < R) {q : CKN.Vec m × ℝ → ℝ} : HasCompactSupport fun (x : CKN.Vec m) => kappaProfile kap (mollifySlice m ε q (x, τ) - barrier m M σ K τ₀ (x, τ)) * mollifierCutoff m R x

The culmination of stage (1). For every κ > 0, the Kato regularization of the excess, multiplied by the spatial cutoff, is compactly supported — the divergent, uncut Φ_κ(g) alone is not, since Φ_κ(g) → -κ / 2 (not 0) away from the compact support of v_ε.

theorem CIV.contDiff_kappaProfile_mul_mollifierCutoff {m : ℕ} {ε M σ K τ₀ τ R kap : ℝ} (hε : 0 < ε) (hR : 0 < R) (hkap : 0 < kap) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => kappaProfile kap (mollifySlice m ε q (x, τ) - barrier m M σ K τ₀ (x, τ)) * mollifierCutoff m R x