Almost-Everywhere Derivative of the Monge–Ampère Exponent

This formalizes the coordinate chain-rule identity associated with the Monge–Ampère exponent, cited as a partial formalization of Lemma 2.4 of Letwin (arXiv:2607.24164v1).

Let $n\in\mathbb N$ and let $u,V:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))\to\mathbb R$. Assume:

1. $u$ is $C^1$.
2. Its gradient is Lipschitz with some constant $G\in[0,\infty)$.
3. $V$ is $C^1$.

Then, for almost every $x$ and every coordinate index $j<n$,

where $H_u$ is the coordinate matrix hessianMatrix, and $e_j$ is EuclideanSpace.basisFun (Fin n) ℝ j. The declaration is a coordinate identity only; it does not assert a Monge–Ampère equation.

Original Lean declaration header

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

theorem ae_fderiv_mongeAmpere_exponent {n : ℕ}
    {u V : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) {G : NNReal} (hG : LipschitzWith G (gradient u))
    (hV : ContDiff ℝ 1 V) :
    ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))), ∀ j : Fin n,
      fderiv ℝ (fun y => -u y + V (gradient u y)) x
          (EuclideanSpace.basisFun (Fin n) ℝ j) =
        -fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ j) +
          ∑ k, hessianMatrix u x j k *
            fderiv ℝ V (gradient u x) (EuclideanSpace.basisFun (Fin n) ℝ k)

Module navigation

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

Definition modules: Analysis/BakryEmery/HessianOperator.

Next: sum_inv_gradient_test_sub_chain_eq.

Source excerpt, lines 220–229 · Frozen source 408915f.