Smoothness of the Energy Form Near Invertible Operators

This statement proves that the coordinate-tensor energy form is $C^2$ near an invertible operator.

Let $n,r\in\mathbb N$, let $A$ be a continuous linear operator on $\mathbb R^n$ represented as EuclideanSpace ℝ (Fin n), and assume $A$ is a unit, hence invertible in the relevant operator ring. Let $T:(\operatorname{Fin}(r)\to\operatorname{Fin}(n))\to\mathbb R$. Then the map

is twice continuously differentiable at $(A,T)$.

This local regularity result supplies the differentiability needed for second-order calculations involving the energy form.

Formalization Note The statement uses finite-dimensional EuclideanSpace ℝ (Fin n) and Lean's IsUnit hypothesis rather than a separately stated determinant condition.

Original Lean declaration header

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

theorem contDiffAt_energyForm (A : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) (hA : IsUnit A)
    (T : (Fin r → Fin n) → ℝ) :
    ContDiffAt ℝ 2 (fun q : (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) × ((Fin r → Fin n) → ℝ) =>
      energyForm q.1 q.2) (A, T)

Module navigation

Module: Analysis/Tensor/EnergyForm.

Next: sum_mul_prod_delta_erase.

Source excerpt, lines 55–58 · Frozen source 408915f.