The sign of the diffusion term: Green's identity and the vanishing Kato curvature

This file analyses the diffusion term in the truncated Kato energy identity truncatedKatoSq_eq_add_intervalIntegral behind the integrated energy inequality eq:aniso:comparison:positive:energy. The point is its sign: kappaProfile kap is convex but takes negative values, so kappaProfile kap (g x) * deriv (deriv (kappaProfile kap)) (g x) is not signed for fixed kap, and the gradient of the cutoff contributes a further term.

Throughout, g : Vec m → ℝ is a smooth excess (in the application, fun x => mollifySlice m ε q (x, s) - barrier m M σ K τ₀ (x, s) at a fixed time s) and chi : Vec m → ℝ is a smooth, compactly supported cutoff (in the application, mollifierCutoff m R). Let φ_kap := fun x => 2 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x) * chi x ^ 2, the truncated Kato test function whose pairing against the Laplacian is the diffusion term.

Main results

• integral_mul_lapD_eq — Green's identity for the partial Laplacian: for any smooth, compactly supported φ and smooth u, ∫ φ · lapD u = -∑_{i<d} ∫ ∂_i φ · ∂_i u. This is d applications of Mathlib's integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable, one per diffusive coordinate. That lemma needs differentiability at every point of the other function's support, which the Kato-smoothed φ_kap has and the non-smooth comparisonPosPart lacks. lapD is partialLaplacian specialized to a function of Vec m alone, definitionally equal to it at a fixed time slice (partialLaplacian_eq_lapD).

• integral_kappaTestFn_mul_lapD_eq — the chain-rule decomposition, combining Green's identity with the product and chain rule hasFDerivAt_kappaTestFn for φ_kap: with kappaProfile2 kap the second derivative of kappaProfile kap (deriv_deriv_kappaProfile), dirichletD the partial Dirichlet energy ∑_{i<d} (∂_i g)² and mixedD the mixed term ∑_{i<d} ∂_i chi · ∂_i g,

  ∫ φ_kap · lapD g = -∫ chi² (2 (deriv (kappaProfile kap) (g ·))² + 2 kappaProfile kap (g ·) kappaProfile2 kap (g ·)) dirichletD - ∫ 4 kappaProfile kap (g ·) deriv (kappaProfile kap) (g ·) chi · mixedD.

  The 2 (deriv …)² piece is the dissipation, nonnegative for every kap > 0 with no limit needed (kappaTestFn_dissipation_nonneg), so it may be dropped when an upper bound is wanted. The 2 kappaProfile kap kappaProfile2 kap piece is the curvature term.

• tendsto_integral_curvature_term_nhds_zero — the curvature term vanishes as kap ↓ 0, as an integral over all of Vec m. It rests on two facts about the real-variable Kato profile: kappaProfile kap 0 = 0 exactly, for every kap (kappaProfile_zero), so no argument about the gradient on the level set {g = 0} is needed; and consequently |kappaProfile kap t * kappaProfile2 kap t| ≤ 1/2 for every t and every kap > 0 (abs_kappaProfile_mul_kappaProfile2_le). This kap-independent bound gives dominated convergence against ∫ chi² dirichletD (finite, since chi has compact support and dirichletD is continuous), with pointwise limit 0 at every x (tendsto_kappaProfile_mul_kappaProfile2_nhds_zero).

• tendsto_integral_mixed_term_nhds_zero — the kap ↓ 0 limit of the mixed-cutoff term is 4 ∫ max (g ·) 0 · chi · mixedD, which is 0 when max (g ·) 0 and mixedD have disjoint supports (tendsto_integral_mixed_term_nhds_zero_of_disjoint).

• partialLaplacian_sub_gradPair_mollifySlice_sub_le — the barrier reduction: by barrier_supersolution and the linearity lemmas gradPair_sub and partialLaplacian_sub, the Laplacian-minus-drift combination of the mollified slice, less the barrier's time derivative, is bounded above by the same combination for the excess.

• integral_kappaProfile_mul_deriv_mul_mollifierCutoff_sq_le — the Cauchy–Schwarz bound on the pairing of the truncated Kato test function with a square-integrable forcing term.

• tendsto_integral_sq_kappaProfile_mul_mollifierCutoff_nhds_comparisonEnergy — the truncated Kato energy converges to comparisonEnergy as kap ↓ 0.

CIV.Comparison.EnergySpatialIntegration integrates integral_kappaTestFn_mul_lapD_eq and the energy limit in space and time, using lapD, dirichletD, mixedD and kappaProfile2. The comparison proof uses Green's identity integral_mul_lapD_eq (through integral_partialLaplacian_mul_comm_of_hasCompactSupport) and the linearity lemmas gradPair_sub and partialLaplacian_sub (in CIV.Comparison.Direct.SliceEnergy). Vec m carries the sup norm throughout; nothing here needs the Euclidean length.

noncomputable def CIV.kappaProfile2 (kap t : ℝ) : ℝ

The second derivative of the Kato profile in closed form.

Equations

• CIV.kappaProfile2 kap t = kap ^ 2 / (2 * √(t ^ 2 + kap ^ 2) ^ 3)

theorem CIV.hasDerivAt_deriv_kappaProfile (kap : ℝ) (hkap : 0 < kap) (t : ℝ) : HasDerivAt (deriv (kappaProfile kap)) (kappaProfile2 kap t) t

The second derivative of the Kato profile, kappaProfile2, is genuinely its derivative: (kappaProfile kap) is differentiable twice for kap > 0, with the closed form computed by the quotient rule.

theorem CIV.deriv_deriv_kappaProfile (kap : ℝ) (hkap : 0 < kap) (t : ℝ) : deriv (deriv (kappaProfile kap)) t = kappaProfile2 kap t

deriv (deriv (kappaProfile kap)) = kappaProfile2 kap, the value form of hasDerivAt_deriv_kappaProfile.

theorem CIV.kappaProfile_zero (kap : ℝ) (hkap : 0 < kap) : kappaProfile kap 0 = 0

The Kato profile vanishes exactly at 0, for every kap: this single fact is what lets the curvature term below be dominated uniformly in kap, with no delicate a.e.-vanishing-gradient argument on the level set {g = 0}.

theorem CIV.abs_kappaProfile_mul_kappaProfile2_le (kap : ℝ) (hkap : 0 < kap) (t : ℝ) : |kappaProfile kap t * kappaProfile2 kap t| ≤ 1 / 2

The curvature coefficient kappaProfile kap t * kappaProfile2 kap t is bounded by an absolute constant, uniformly in t and kap > 0. This is the quantitative core of the diffusion sign derivation: the convex, possibly-negative Kato profile can only ever contribute a bounded amount through its own curvature.

theorem CIV.kappaProfile_mul_kappaProfile2_eq (kap t : ℝ) (hkap : 0 < kap) : kappaProfile kap t * kappaProfile2 kap t = kap ^ 2 * (t + √(t ^ 2 + kap ^ 2) - kap) / (4 * √(t ^ 2 + kap ^ 2) ^ 3)

The curvature coefficient in closed form, as a single fraction.

theorem CIV.tendsto_kappaProfile_mul_kappaProfile2_nhds_zero (t : ℝ) : Filter.Tendsto (fun (kap : ℝ) => kappaProfile kap t * kappaProfile2 kap t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The curvature coefficient tends to 0 pointwise as kap ↓ 0, for every real t. Away from t = 0 this is continuity of the closed form; at t = 0 it is exact (kappaProfile_zero), not merely a limit. Combined with abs_kappaProfile_mul_kappaProfile2_le's uniform bound, this is what makes the curvature term of the diffusion identity vanish under dominated convergence (tendsto_integral_curvature_term_nhds_zero below), which is the precise sense in which the sign of the diffusion term is resolved here.

theorem CIV.neg_le_kappaProfile_mul_deriv_kappaProfile (kap : ℝ) (hkap : 0 < kap) (t : ℝ) : -(kap / 16) ≤ kappaProfile kap t * deriv (kappaProfile kap) t

The product kappaProfile kap t * deriv (kappaProfile kap) t is bounded below by -kap / 16, uniformly in t: it is O(kap), since kappaProfile kap t * deriv (kappaProfile kap) t is homogeneous of degree 1 in (kap, t) jointly. Used to control the supersolution slack the barrier contributes once the drift and diffusion of the mollified equation are reduced to the excess alone.

theorem CIV.tendsto_kappaProfile_mul_deriv_kappaProfile (t : ℝ) : Filter.Tendsto (fun (kap : ℝ) => kappaProfile kap t * deriv (kappaProfile kap) t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (max t 0))

kappaProfile kap t * deriv (kappaProfile kap) t → max t 0 as kap ↓ 0, for every t: the Kato regularization of t ↦ (t_+)²/2's derivative converges to the derivative of t ↦ (t_+)²/2 itself away from the (here harmless) single point t = 0.

noncomputable def CIV.lapD (m d : ℕ) (u : CKN.Vec m → ℝ) (x : CKN.Vec m) : ℝ

The partial Laplacian of a pure Vec m → ℝ function, in the first d coordinates.

Equations

• CIV.lapD m d u x = ∑ i : Fin m, if ↑i < d then (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ u y) (CKN.basisVec i)) x) (CKN.basisVec i) else 0

theorem CIV.partialLaplacian_eq_lapD {m d : ℕ} (φ : CKN.Vec m × ℝ → ℝ) (z : CKN.Vec m × ℝ) : partialLaplacian m d φ z = lapD m d (fun (y : CKN.Vec m) => φ (y, z.2)) z.1

partialLaplacian unfolds to lapD of the fixed-time spatial slice: purely definitional, so that the Green's identity below (stated for lapD, a function of Vec m alone) applies directly to partialLaplacian.

theorem CIV.fderiv_fderiv_sub_apply {m : ℕ} {f1 f2 : CKN.Vec m → ℝ} (hf1 : ContDiff ℝ (↑⊤) f1) (hf2 : ContDiff ℝ (↑⊤) f2) (x : CKN.Vec m) (i : Fin m) : (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ (fun (w : CKN.Vec m) => f1 w - f2 w) y) (CKN.basisVec i)) x) (CKN.basisVec i) = (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ f1 y) (CKN.basisVec i)) x) (CKN.basisVec i) - (fderiv ℝ (fun (y : CKN.Vec m) => (fderiv ℝ f2 y) (CKN.basisVec i)) x) (CKN.basisVec i)

The second coordinate derivative of a difference is the difference of the second coordinate derivatives, for globally smooth f1, f2.

theorem CIV.lapD_sub {m d : ℕ} {f1 f2 : CKN.Vec m → ℝ} (hf1 : ContDiff ℝ (↑⊤) f1) (hf2 : ContDiff ℝ (↑⊤) f2) (x : CKN.Vec m) : lapD m d (fun (y : CKN.Vec m) => f1 y - f2 y) x = lapD m d f1 x - lapD m d f2 x

lapD is linear in its function argument, for globally smooth summands: the tool needed to split partialLaplacian of the mollified slice into the partial Laplacian of the excess plus that of the barrier.

theorem CIV.integral_mul_lapD_eq {m d : ℕ} {φ u : CKN.Vec m → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hu : ContDiff ℝ (↑⊤) u) : ∫ (x : CKN.Vec m), φ x * lapD m d u x = -∑ i : Fin m, if ↑i < d then ∫ (x : CKN.Vec m), (fderiv ℝ φ x) (CKN.basisVec i) * (fderiv ℝ u x) (CKN.basisVec i) else 0

Green's identity for lapD. For a smooth, compactly supported test function φ and a smooth u, ∫ φ · lapD u = -∑_{i<d} ∫ ∂_i φ · ∂_i u: d applications of Mathlib's integration by parts for Fréchet derivatives, one per diffusive coordinate, each licensed because φ and u are differentiable at every point (not merely a.e.) — the obstruction DiPerna–Lions-type test functions such as comparisonPosPart run into is exactly what the Kato smoothing of the excess repairs.

theorem CIV.hasFDerivAt_kappaTestFn {m : ℕ} {g chi : CKN.Vec m → ℝ} {kap : ℝ} (hkap : 0 < kap) (hg : ContDiff ℝ (↑⊤) g) (hchi : ContDiff ℝ (↑⊤) chi) (x : CKN.Vec m) : HasFDerivAt (fun (y : CKN.Vec m) => 2 * kappaProfile kap (g y) * deriv (kappaProfile kap) (g y) * chi y ^ 2) ((chi x ^ 2 * (2 * deriv (kappaProfile kap) (g x))) • deriv (kappaProfile kap) (g x) • fderiv ℝ g x + (chi x ^ 2 * (2 * kappaProfile kap (g x))) • kappaProfile2 kap (g x) • fderiv ℝ g x + (2 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x)) • (2 * chi x) • fderiv ℝ chi x) x

The Fréchet derivative of the truncated Kato test function 2 Φ_κ(g) Φ_κ'(g) χ², by the product and chain rules.

theorem CIV.fderiv_kappaTestFn_apply {m : ℕ} {g chi : CKN.Vec m → ℝ} {kap : ℝ} (hkap : 0 < kap) (hg : ContDiff ℝ (↑⊤) g) (hchi : ContDiff ℝ (↑⊤) chi) (x v : CKN.Vec m) : (fderiv ℝ (fun (y : CKN.Vec m) => 2 * kappaProfile kap (g y) * deriv (kappaProfile kap) (g y) * chi y ^ 2) x) v = chi x ^ 2 * (2 * deriv (kappaProfile kap) (g x) ^ 2 + 2 * kappaProfile kap (g x) * kappaProfile2 kap (g x)) * (fderiv ℝ g x) v + 4 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x) * chi x * (fderiv ℝ chi x) v

The value of the derivative of the truncated-Kato test function 2 Φ_κ(g) Φ_κ'(g) χ² in a direction v, by the product/chain rule.

noncomputable def CIV.dirichletD (m d : ℕ) (g : CKN.Vec m → ℝ) (x : CKN.Vec m) : ℝ

The partial Dirichlet energy density ∑_{i<d} (∂_i g)².

Equations

• CIV.dirichletD m d g x = ∑ i : Fin m, if ↑i < d then (fderiv ℝ g x) (CKN.basisVec i) ^ 2 else 0

noncomputable def CIV.mixedD (m d : ℕ) (g chi : CKN.Vec m → ℝ) (x : CKN.Vec m) : ℝ

The mixed cutoff/gradient term ∑_{i<d} ∂_i χ · ∂_i g.

Equations

• CIV.mixedD m d g chi x = ∑ i : Fin m, if ↑i < d then (fderiv ℝ chi x) (CKN.basisVec i) * (fderiv ℝ g x) (CKN.basisVec i) else 0

theorem CIV.sum_fderiv_kappaTestFn_mul_fderiv_eq {m d : ℕ} {g chi : CKN.Vec m → ℝ} {kap : ℝ} (hkap : 0 < kap) (hg : ContDiff ℝ (↑⊤) g) (hchi : ContDiff ℝ (↑⊤) chi) (x : CKN.Vec m) : (∑ i : Fin m, if ↑i < d then (fderiv ℝ (fun (y : CKN.Vec m) => 2 * kappaProfile kap (g y) * deriv (kappaProfile kap) (g y) * chi y ^ 2) x) (CKN.basisVec i) * (fderiv ℝ g x) (CKN.basisVec i) else 0) = chi x ^ 2 * (2 * deriv (kappaProfile kap) (g x) ^ 2 + 2 * kappaProfile kap (g x) * kappaProfile2 kap (g x)) * dirichletD m d g x + 4 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x) * chi x * mixedD m d g chi x

The pointwise sum ∑_{i<d} ∂_i φ · ∂_i g for the truncated-Kato test function φ, in closed form: this is exactly the sum Green's identity produces.

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

deriv (kappaProfile kap) is itself smooth, for kap > 0: deriv f = fderiv ℝ f · 1, so this is ContDiff.fderiv_right applied to kappaProfile kap and evaluated at 1.

theorem CIV.integral_kappaTestFn_mul_lapD_eq {m d : ℕ} {g chi : CKN.Vec m → ℝ} {kap : ℝ} (hkap : 0 < kap) (hg : ContDiff ℝ (↑⊤) g) (hchi : ContDiff ℝ (↑⊤) chi) (hchic : HasCompactSupport chi) : ∫ (x : CKN.Vec m), 2 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x) * chi x ^ 2 * lapD m d g x = -∫ (x : CKN.Vec m), chi x ^ 2 * (2 * deriv (kappaProfile kap) (g x) ^ 2 + 2 * kappaProfile kap (g x) * kappaProfile2 kap (g x)) * dirichletD m d g x + 4 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x) * chi x * mixedD m d g chi x

Green's identity for the truncated-Kato diffusion term, combined with the product/chain rule: the exact spatial identity behind the sign of the diffusion term. No inequality or limit is taken: this is algebra plus one integration by parts.

theorem CIV.continuous_dirichletD {m d : ℕ} {g : CKN.Vec m → ℝ} (hg : ContDiff ℝ (↑⊤) g) : Continuous (dirichletD m d g)

The partial Dirichlet energy density is continuous, when g is smooth.

theorem CIV.continuous_kappaProfile2 (kap : ℝ) (hkap : 0 < kap) : Continuous (kappaProfile2 kap)

The second derivative of the Kato profile is continuous in t, for fixed kap > 0.

theorem CIV.continuous_integrand_curvature {m d : ℕ} {g chi : CKN.Vec m → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hchi : ContDiff ℝ (↑⊤) chi) {kap : ℝ} (hkap : 0 < kap) : Continuous fun (x : CKN.Vec m) => chi x ^ 2 * (2 * kappaProfile kap (g x) * kappaProfile2 kap (g x)) * dirichletD m d g x

The curvature-term integrand is continuous, for fixed kap > 0.

theorem CIV.tendsto_integral_curvature_term_nhds_zero {m d : ℕ} {g chi : CKN.Vec m → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hchi : ContDiff ℝ (↑⊤) chi) (hchic : HasCompactSupport chi) : Filter.Tendsto (fun (kap : ℝ) => ∫ (x : CKN.Vec m), chi x ^ 2 * (2 * kappaProfile kap (g x) * kappaProfile2 kap (g x)) * dirichletD m d g x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The diffusion term's curvature contribution vanishes as kap ↓ 0, as an integral over all of Vec m. Dominated convergence: abs_kappaProfile_mul_kappaProfile2_le supplies the kap-independent dominating function χ² · dirichletD (integrable, since χ has compact support and dirichletD is continuous), and tendsto_kappaProfile_mul_kappaProfile2_nhds_zero supplies the pointwise limit 0. This is the resolution, at the level of the full spatial integral rather than pointwise, of the sign question this module exists to answer.

The barrier reduction: transferring the mollified equation's estimate to the excess

The next three declarations combine barrier_supersolution with the linearity of gradPair and partialLaplacian over subtraction, given only the spatial smoothness contDiff_mollifySlice/contDiff_barrier supply at a fixed time slice — no joint space-time smoothness of either summand is assumed, and hCont/hLoc play no role here. The reduction shows that the Laplacian-minus-drift combination of the mollified slice, once the barrier's own time derivative σ · K is subtracted, is bounded above by the same combination for the excess g = q_ε − Ψ_σ alone: whatever the mollified equation supplies for q_ε therefore transfers to g without loss, since barrier_supersolution supplies exactly enough slack (0 ≤ σK + ∇Ψ_σ · B − Δ_XΨ_σ) to absorb the barrier's own Laplacian and drift terms.

theorem CIV.gradPair_sub {m : ℕ} {f f2 : CKN.Vec m × ℝ → ℝ} (z : CKN.Vec m × ℝ) (hf : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => f (x, z.2)) (hf2 : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => f2 (x, z.2)) (v : CKN.Vec m) : gradPair m (fun (w : CKN.Vec m × ℝ) => f w - f2 w) z v = gradPair m f z v - gradPair m f2 z v

gradPair is linear over subtraction, given the spatial-slice smoothness of each summand at the point's own time coordinate.

theorem CIV.partialLaplacian_sub {m d : ℕ} {f f2 : CKN.Vec m × ℝ → ℝ} (z : CKN.Vec m × ℝ) (hf : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => f (x, z.2)) (hf2 : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => f2 (x, z.2)) : partialLaplacian m d (fun (w : CKN.Vec m × ℝ) => f w - f2 w) z = partialLaplacian m d f z - partialLaplacian m d f2 z

partialLaplacian is linear over subtraction, given the same spatial-slice smoothness as gradPair_sub: this is lapD_sub transported across partialLaplacian_eq_lapD.

theorem CIV.partialLaplacian_sub_gradPair_mollifySlice_sub_le {m d : ℕ} {ε M σ τ₀ Λ Minf s : ℝ} (hε : 0 < ε) (hσ : 0 ≤ σ) {q : CKN.Vec m × ℝ → ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, s)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, s)| ≤ Minf) {B : CKN.Vec m × ℝ → CKN.Vec m} (x : CKN.Vec m) (hB : ‖B (x, s)‖ ≤ Λ) : partialLaplacian m d (mollifySlice m ε q) (x, s) - gradPair m (mollifySlice m ε q) (x, s) (B (x, s)) - σ * barrierRate m d Λ ≤ lapD m d (fun (y : CKN.Vec m) => mollifySlice m ε q (y, s) - barrier m M σ (barrierRate m d Λ) τ₀ (y, s)) x - (fderiv ℝ (fun (y : CKN.Vec m) => mollifySlice m ε q (y, s) - barrier m M σ (barrierRate m d Λ) τ₀ (y, s)) x) (B (x, s))

The barrier reduction. With the rate K = barrierRate m d Λ of barrier_supersolution, the Laplacian-minus-drift combination of the mollified slice, less the barrier's own time derivative σK, is bounded above by the same combination for the excess g = fun y => mollifySlice m ε q (y, s) - barrier m M σ K τ₀ (y, s).

The Cauchy–Schwarz bound on the truncated-Kato/commutator pairing

two_mul_mul_le_two_mul_abs_mul_abs and integral_abs_mul_abs_le_sqrt_mul_sqrt are combined here to bound the pairing of the truncated Kato test function's leading factor against an arbitrary square-integrable right-hand term c (the commutator or drift-type forcing of eq:aniso:comparison:mollified), truncated by mollifierCutoff m R. Once kappaProfile kap (g ·) * mollifierCutoff m R is identified with comparisonPosPart * mollifierCutoff m R as kap ↓ 0 (integral_sq_mul_mollifierCutoff_eq_comparisonEnergy makes its squared integral exactly comparisonEnergy), the right side becomes the 2 √E · r shape of the hypothesis hineq of comparisonEnergy_le_exp_mul_integral_sq; the kap ↓ 0 limit of the truncated Kato energy is tendsto_integral_sq_kappaProfile_mul_mollifierCutoff_nhds_comparisonEnergy below.

theorem CIV.integral_kappaProfile_mul_deriv_mul_mollifierCutoff_sq_le {m : ℕ} {g c : CKN.Vec m → ℝ} {kap R : ℝ} (hkap : 0 < kap) (hR : 0 < R) (hMemF : MeasureTheory.MemLp (fun (x : CKN.Vec m) => kappaProfile kap (g x) * mollifierCutoff m R x) 2 MeasureTheory.volume) (hMemc : MeasureTheory.MemLp c 2 MeasureTheory.volume) (hInt : MeasureTheory.Integrable (fun (x : CKN.Vec m) => 2 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x) * c x * mollifierCutoff m R x ^ 2) MeasureTheory.volume) (hInt2 : MeasureTheory.Integrable (fun (x : CKN.Vec m) => 2 * |kappaProfile kap (g x) * mollifierCutoff m R x| * |c x|) MeasureTheory.volume) : ∫ (x : CKN.Vec m), 2 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x) * c x * mollifierCutoff m R x ^ 2 ≤ 2 * √(∫ (x : CKN.Vec m), (kappaProfile kap (g x) * mollifierCutoff m R x) ^ 2) * √(∫ (x : CKN.Vec m), c x ^ 2)

The Cauchy–Schwarz commutator bound. deriv (kappaProfile kap) ∈ [0, 1] (deriv_kappaProfile_mem_Icc) and mollifierCutoff m R ∈ [0, 1] (mollifierCutoff_nonneg/mollifierCutoff_le_one) let the pointwise bound two_mul_mul_le_two_mul_abs_mul_abs discard both factors at the cost of absolute values, and integral_mono transports it to the integral, which integral_abs_mul_abs_le_sqrt_mul_sqrt then bounds by twice the product of the L² norms of kappaProfile kap (g ·) * mollifierCutoff m R and c.

The dissipation term's sign and the mixed-cutoff term's kap ↓ 0 limit

The remaining two pieces of integral_kappaTestFn_mul_lapD_eq's right-hand side: the dissipation summand chi² · 2 (Φ_κ'(g))² · dirichletD, nonnegative for every kap > 0 with no limit needed, and the mixed-cutoff summand 4 Φ_κ(g) Φ_κ'(g) chi · mixedD, whose kap ↓ 0 limit is computed here by dominated convergence, as in tendsto_integral_curvature_term_nhds_zero.

The mixed term does not vanish for fixed kap. Once a cutoff radius R is fixed at or above the support radius of comparisonPosPart, mixedD is supported where the cutoff's own gradient is nonzero, which — by comparisonPosPart_eq_zero_of_norm_ge — is exactly where the excess g itself is ≤ 0. That does not make kappaProfile kap (g ·) vanish there for a fixed kap: kappaProfile_neg_of_neg shows it is strictly negative on all of {g < 0}, not merely in the limit kap ↓ 0 (only kappaProfile_zero gives an exact zero, at g = 0 alone). So the mixed term does not vanish identically for fixed kap; its kap ↓ 0 limit does, under the disjoint-support hypothesis of tendsto_integral_mixed_term_nhds_zero_of_disjoint.

theorem CIV.dirichletD_nonneg {m d : ℕ} (g : CKN.Vec m → ℝ) (x : CKN.Vec m) : 0 ≤ dirichletD m d g x

dirichletD is a sum of squares, hence nonnegative.

theorem CIV.kappaTestFn_dissipation_nonneg {m d : ℕ} (g chi : CKN.Vec m → ℝ) (kap : ℝ) (x : CKN.Vec m) : 0 ≤ chi x ^ 2 * (2 * deriv (kappaProfile kap) (g x) ^ 2) * dirichletD m d g x

The dissipation term's sign. The dissipation contribution chi² · 2 (Φ_κ'(g))² · dirichletD to integral_kappaTestFn_mul_lapD_eq's curvature/dissipation summand is nonnegative for every kap, since it needs only that a square is nonnegative and dirichletD is a sum of squares — so it contributes no obstruction to an upper bound on the diffusion term and may always be dropped.

theorem CIV.kappaTestFn_curvature_le_dissipation_add_curvature {m d : ℕ} (g chi : CKN.Vec m → ℝ) (kap : ℝ) (x : CKN.Vec m) : chi x ^ 2 * (2 * kappaProfile kap (g x) * kappaProfile2 kap (g x)) * dirichletD m d g x ≤ chi x ^ 2 * (2 * deriv (kappaProfile kap) (g x) ^ 2 + 2 * kappaProfile kap (g x) * kappaProfile2 kap (g x)) * dirichletD m d g x

Adding the dissipation term back to the curvature term can only increase it: the pointwise form of "the dissipation term may be dropped when an upper bound is wanted".

theorem CIV.kappaProfile_neg_of_neg (kap : ℝ) (hkap : 0 < kap) {t : ℝ} (ht : t < 0) : kappaProfile kap t < 0

The Kato profile is strictly negative below 0. This is why the disjoint support of g₊ does not make the mixed-cutoff term vanish identically for a fixed kap: kappaProfile kap vanishes only exactly at t = 0 (kappaProfile_zero), not on the whole ray t ≤ 0, so being supported where g ≤ 0 does not make kappaProfile kap (g ·) vanish there.

theorem CIV.continuous_mixedD {m d : ℕ} {g chi : CKN.Vec m → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hchi : ContDiff ℝ (↑⊤) chi) : Continuous (mixedD m d g chi)

The mixed cutoff/gradient density is continuous, when g and chi are smooth.

theorem CIV.abs_kappaProfile_le (kap : ℝ) (hkap : 0 < kap) (t : ℝ) : |kappaProfile kap t| ≤ |t| + kap / 2

The kap-uniform bound on the Kato profile, the domination ingredient for the mixed-term limit: |Φ_κ(t)| ≤ |t| + kap / 2, from the two-sided sandwich max t 0 - kap/2 ≤ Φ_κ(t) ≤ max t 0 against katoSmooth.

theorem CIV.tendsto_integral_mixed_term_nhds_zero {m d : ℕ} {g chi : CKN.Vec m → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hchi : ContDiff ℝ (↑⊤) chi) (hchic : HasCompactSupport chi) : Filter.Tendsto (fun (kap : ℝ) => ∫ (x : CKN.Vec m), 4 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x) * chi x * mixedD m d g chi x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : CKN.Vec m), 4 * max (g x) 0 * chi x * mixedD m d g chi x))

The mixed-cutoff term's kap ↓ 0 limit, by dominated convergence. Structurally identical to tendsto_integral_curvature_term_nhds_zero: tendsto_kappaProfile_mul_deriv_kappaProfile supplies the pointwise limit Φ_κ(g) Φ_κ'(g) → max(g, 0), and abs_kappaProfile_le (restricted to kap ≤ 1, where it gives a kap-independent bound) supplies the dominating function 4 (|g| + 1/2) |chi| |mixedD|, integrable because chi has compact support and every other factor is continuous. The resulting limit integral is 4 ∫ max(g, 0) · chi · mixedD, not 0 in general — see the module docstring above and tendsto_integral_mixed_term_nhds_zero_of_disjoint below for the extra, application-specific hypothesis under which it is 0.

theorem CIV.tendsto_integral_mixed_term_nhds_zero_of_disjoint {m d : ℕ} {g chi : CKN.Vec m → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hchi : ContDiff ℝ (↑⊤) chi) (hchic : HasCompactSupport chi) (hdisj : ∀ (x : CKN.Vec m), max (g x) 0 * mixedD m d g chi x = 0) : Filter.Tendsto (fun (kap : ℝ) => ∫ (x : CKN.Vec m), 4 * kappaProfile kap (g x) * deriv (kappaProfile kap) (g x) * chi x * mixedD m d g chi x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The mixed-cutoff term's kap ↓ 0 limit is 0 under a disjoint-support hypothesis. Not an identity holding for every fixed kap, but a kap ↓ 0 limit resting on tendsto_integral_mixed_term_nhds_zero, once max (g ·) 0 and mixedD m d g chi have disjoint supports pointwise. For the excess and the cutoff mollifierCutoff m R, this hypothesis comes from mollifierCutoff_eq_one and comparisonPosPart_eq_zero_of_norm_ge.

The kap ↓ 0 identification of the truncated Kato energy with comparisonEnergy

integral_sq_mul_mollifierCutoff_eq_comparisonEnergy identifies the truncated energy ∫ (comparisonPosPart · mollifierCutoff m R)² with comparisonEnergy; it says nothing about ∫ (kappaProfile kap (g ·) · mollifierCutoff m R)², since comparisonPosPart = max (g ·) 0 and kappaProfile kap (g ·) are different functions at every fixed kap — e.g. kappaProfile 1 (-1) ≠ max (-1) 0. They agree only as kap ↓ 0. The three theorems below supply that limit, by dominated convergence as in tendsto_integral_mixed_term_nhds_zero above: tendsto_katoSmooth gives the pointwise limit kappaProfile kap t → max t 0, and abs_kappaProfile_le (restricted to kap ≤ 1) gives the kap-independent dominating function (|g ·| + 1/2)² · mollifierCutoff m R ², integrable because mollifierCutoff m R has compact support (hasCompactSupport_mollifierCutoff) and every other factor is continuous.

theorem CIV.tendsto_integral_sq_kappaProfile_mul_mollifierCutoff_nhds_zero {m : ℕ} {g : CKN.Vec m → ℝ} {R : ℝ} (hg : Continuous g) (hR : 0 < R) : Filter.Tendsto (fun (kap : ℝ) => ∫ (x : CKN.Vec m), (kappaProfile kap (g x) * mollifierCutoff m R x) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : CKN.Vec m), (max (g x) 0 * mollifierCutoff m R x) ^ 2))

The squared truncated Kato profile converges to the squared truncated positive part, for any continuous g : Vec m → ℝ and cutoff radius R > 0, as kap ↓ 0.

theorem CIV.tendsto_integral_sq_kappaProfile_mul_mollifierCutoff_nhds_comparisonPosPart {m : ℕ} {ε M σ K τ₀ τ Minf R : ℝ} (hε : 0 < ε) (hR : 0 < 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) : Filter.Tendsto (fun (kap : ℝ) => ∫ (x : CKN.Vec m), (kappaProfile kap (mollifySlice m ε q (x, τ) - barrier m M σ K τ₀ (x, τ)) * mollifierCutoff m R x) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : CKN.Vec m), (comparisonPosPart m ε M σ K τ₀ q (x, τ) * mollifierCutoff m R x) ^ 2))

The kap ↓ 0 identification, at the excess g = mollifySlice - barrier. Instantiates tendsto_integral_sq_kappaProfile_mul_mollifierCutoff_nhds_zero at g x := mollifySlice m ε q (x, τ) - barrier m M σ K τ₀ (x, τ), continuous by contDiff_mollifySlice/contDiff_barrier, and rewrites the limit using comparisonPosPart m ε M σ K τ₀ q (x, τ) = max (g x) 0, which holds by definition of comparisonPosPart — not an approximation.

theorem CIV.tendsto_integral_sq_kappaProfile_mul_mollifierCutoff_nhds_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) : Filter.Tendsto (fun (kap : ℝ) => ∫ (x : CKN.Vec m), (kappaProfile kap (mollifySlice m ε q (x, τ) - barrier m M σ K τ₀ (x, τ)) * mollifierCutoff m R x) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (comparisonEnergy m ε M σ K τ₀ q τ))

The kap ↓ 0 limit of the truncated Kato energy is comparisonEnergy, the form matching the hypothesis hineq of comparisonEnergy_le_exp_mul_integral_sq. The proof composes tendsto_integral_sq_kappaProfile_mul_mollifierCutoff_nhds_comparisonPosPart with integral_sq_mul_mollifierCutoff_eq_comparisonEnergy, which is exact once R ≥ Minf / σ.