Almost-Everywhere Derivative Formula for Weak Matrix Inverses

This is a technical almost-everywhere inverse differentiation rule for matrix-valued weak derivatives.

Let $A,R:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(d))\to\mathbb R^{m\times m}$, with weak directional derivatives $DA,DR$ along a fixed direction. Assume:

1. Every entry of $A$ and $R$ is locally essentially bounded on compact sets (MemLp with exponent $\top$).
2. Every entry of $DA$ and $DR$ belongs to local $L^2$ on compact sets.
3. Almost everywhere, $R(x)A(x)=I$.

Then, almost everywhere,

The dimensions $d$ and $m$ are independent and may be zero. The declaration ae_weak_matrix_inverse_derivative_readable assumes the weak derivatives and integrability data as inputs; it does not assume classical differentiability.

Original Lean declaration header

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

theorem ae_weak_matrix_inverse_derivative {d m : ℕ}
    {A R DA DR : EuclideanSpace ℝ (Fin d) → Matrix (Fin m) (Fin m) ℝ}
    {v : EuclideanSpace ℝ (Fin d)}
    (hA : ∀ i j, HasWeakDerivAlong (fun x => A x i j) (fun x => DA x i j) v)
    (hR : ∀ i j, HasWeakDerivAlong (fun x => R x i j) (fun x => DR x i j) v)
    (hA_top : ∀ i j, ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
      MemLp (fun x => A x i j) (⊤ : ENNReal)
        ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S))
    (hR_top : ∀ i j, ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
      MemLp (fun x => R x i j) (⊤ : ENNReal)
        ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S))
    (hDA2 : ∀ i j, ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
      MemLp (fun x => DA x i j) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S))
    (hDR2 : ∀ i j, ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
      MemLp (fun x => DR x i j) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S))
    (hRA : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin d))), R x * A x = 1) :
    ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin d))),
      DR x = -(R x * DA x * R x)

Module navigation

Module: Analysis/Matrix/WeakDerivative.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: HasWeakDerivAlong.congr_ae, HasWeakDerivAlong.mul_of_locally_bounded, hasWeakDerivAlong_finsetSum_mul, hasWeakDerivAlong_of_contDiff.

Previous: hasWeakDerivAlong_trace_quadratic_of_locally_memLp_two · Next: bounded_trace_quadratic_weak_derivative_data.

Source excerpt, lines 130–149 · Frozen source 408915f.