Exponential Weighting of an Unweighted Flux Identity

This is a weighted-testing lemma for compactly supported $C^1$ tests.

Let $u,c:\mathbb R^n\to\mathbb R$ be such that $u$ is $C^1$. Let $J_a$ be locally integrable for every coordinate $a$, and let $c$ be locally integrable. Assume that every compactly supported $C^1$ function $\phi$ satisfies

Then $e^{-u}(c-\sum_aJ_a\partial_a u)$ is locally integrable, and every compactly supported $C^1$ function $\psi$ satisfies

The lemma is a product-rule interface for passing from an unweighted divergence identity to its $e^{-u}$-weighted form.

Original Lean declaration header

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

private theorem integral_exp_neg_flux_of_unweighted {n : ℕ}
    {u c : EuclideanSpace ℝ (Fin n) → ℝ}
    {J : EuclideanSpace ℝ (Fin n) → Fin n → ℝ}
    (hu : ContDiff ℝ 1 u)
    (hJ : ∀ a : Fin n, LocallyIntegrable (fun x => J x a)
      (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hc : LocallyIntegrable c (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hId : ∀ φ : EuclideanSpace ℝ (Fin n) → ℝ,
      ContDiff ℝ 1 φ → HasCompactSupport φ →
      (∫ x, ∑ a : Fin n, J x a *
        fderiv ℝ φ x (EuclideanSpace.basisFun (Fin n) ℝ a)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) =
      -(∫ x, c x * φ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))))) :
    LocallyIntegrable
      (fun x => Real.exp (-u x) * (c x - ∑ a : Fin n, J x a *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ a)))
      (volume : Measure (EuclideanSpace ℝ (Fin n))) ∧
    ∀ ψ : EuclideanSpace ℝ (Fin n) → ℝ,
      ContDiff ℝ 1 ψ → HasCompactSupport ψ →
      (∫ x, Real.exp (-u x) * (∑ a : Fin n, J x a *
        fderiv ℝ ψ x (EuclideanSpace.basisFun (Fin n) ℝ a))
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) =
      -(∫ x, Real.exp (-u x) * (c x - ∑ a : Fin n, J x a *
        fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ a)) * ψ x
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/WeakHessianEvolution.

Previous: ae_hessian_flux_forcing_minus_drift · Next: integral_exp_neg_hessian_flux_eq_curvature_gram.

Source excerpt, lines 1285–1309 · Frozen source 408915f.