Assembly of the Weak Generator Identity

This is an assembly lemma for a weak inverse-Hessian generator identity.

Let $u,V,a,f$ be functions on $\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))$. Assume $u,V$ are $C^1$, $\nabla u$ is Lipschitz, the exponent $-u+V\circ\nabla u$ is Lipschitz, and almost everywhere

Assume also that each weighted coordinate test has a Lipschitz compactly supported representative, that its coordinate derivative satisfies the specified a.e. formula, and that the associated energyDensity u a f is integrable.

Then

The statement is an internal analytic assembly interface: its hypotheses include the derivative and integrability inputs explicitly, and it does not itself assert the broader Monge–Ampère theorem.

Original Lean declaration header

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

private lemma assemble_generator {n : ℕ}
    {u V a f : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) {G : NNReal}
    (hG : LipschitzWith G (gradient u)) (hV : ContDiff ℝ 1 V)
    {LF : NNReal} (hF : LipschitzWith LF (fun x => -u x + V (gradient u x)))
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (-u x + V (gradient u x)))
    (ht : ∀ i, ∃ L : NNReal,
      LipschitzWith L (weightedTest u a f i) ∧
        HasCompactSupport (weightedTest u a f i))
    (hd : ∀ i, ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))), ∀ j,
      coord (weightedTest u a f i) j x =
        Real.exp (-u x) *
          (coord a j x * coord f i x -
            a x * coord u j x * coord f i x +
            a x * hessianMatrix f x j i))
    (hE : Integrable (energyDensity u a f)
      (volume : Measure (EuclideanSpace ℝ (Fin n)))) :
    (∫ x, generatorDensity u V a f x
      ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) =
        -∫ x, energyDensity u a f x
          ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/InverseHessian/Weak.

Definition modules: Analysis/BakryEmery/HessianOperator.

Supporting theorems: ae_fderiv_mongeAmpere_exponent, integrable_inv_hessianMatrix_mul_of_bounded_compact, sum_integral_inv_hessianMatrix_mul_fderiv_eq, sum_inv_gradient_test_sub_chain_eq.

Previous: smooth_test_derivative · Next: integral_mul_generator_eq_neg_energy.

Source excerpt, lines 602–623 · Frozen source 408915f.