MetricTensor.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The regularized metric as a matrix

This identifies the scalar energy expression with trace ((A + τ I)⁻¹ A) sqrt (det (A + τ I)), and proves that regularizing a positive semidefinite tensor gives a positive definite metric. Thus the energy optimization applies to the actual metric tensor.

def OAI.CircleDomainRigidity.FiniteTransfer.symmetricTensor line 20
def OAI.CircleDomainRigidity.FiniteTransfer.regularizedTensor line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.regularizedTensor_posDef line 25
theorem OAI.CircleDomainRigidity.FiniteTransfer.det_regularizedTensor line 30
theorem OAI.CircleDomainRigidity.FiniteTransfer.det_regularizedTensor_pos line 35
theorem OAI.CircleDomainRigidity.FiniteTransfer.trace_inverse_energy_eq_tensorEnergy line 44
Source documentation
The actual inverse-matrix energy density equals the scalar invariant expression used in the dominated-convergence argument.
```
theorem trace_inverse_energy_eq_tensorEnergy {a b c τ : ℝ}
    (ha : 0 ≤ a) (hc : 0 ≤ c) (hD : 0 ≤ a * c - b ^ 2) (hτ : 0 < τ) :
    Matrix.trace ((regularizedTensor a b c τ)⁻¹ * symmetricTensor a b c) *
      Real.sqrt (regularizedTensor a b c τ).det =
      tensorEnergy (a + c) (a * c - b ^ 2) τ := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.regularizedTensor, OAI.CircleDomainRigidity.FiniteTransfer.symmetricTensor, OAI.CircleDomainRigidity.FiniteTransfer.tensorEnergy