TensorEnergy.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

From a positive two-dimensional tensor to optimized energy

The trace and determinant determine the energy of A + τ I. The scalar roots used below are the two nonnegative eigenvalues, constructed directly from the characteristic polynomial. This connects the metric limit to the Gram determinant of the actual finite list of coordinate differentials.

def OAI.CircleDomainRigidity.FiniteTransfer.upperRoot line 21
def OAI.CircleDomainRigidity.FiniteTransfer.lowerRoot line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.roots_nonneg line 24
theorem OAI.CircleDomainRigidity.FiniteTransfer.roots_sum line 34
theorem OAI.CircleDomainRigidity.FiniteTransfer.roots_product line 38
def OAI.CircleDomainRigidity.FiniteTransfer.tensorEnergy line 45
Source documentation
The coordinate-invariant expression for the regularized energy density.
```
def tensorEnergy (T D τ : ℝ) : ℝ :=
…
```
theorem OAI.CircleDomainRigidity.FiniteTransfer.tensorEnergy_eq_metricEnergy line 48
theorem OAI.CircleDomainRigidity.FiniteTransfer.tensorEnergy_le_trace line 64
theorem OAI.CircleDomainRigidity.FiniteTransfer.tendsto_tensorEnergy line 71

theorem OAI.CircleDomainRigidity.FiniteTransfer.tendsto_integral_tensorEnergy line 81

Source documentation

Dominated convergence in terms of the tensor invariants.

theorem tendsto_integral_tensorEnergy {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {T D : X → ℝ} (hT : Measurable T) (hD : Measurable D)
    (hT0 : ∀ x, 0 ≤ T x) (hD0 : ∀ x, 0 ≤ D x)
    (hdisc : ∀ x, 0 ≤ T x ^ 2 - 4 * D x) (htrace : Integrable T μ) :
    Tendsto (fun τ : ℝ => ∫ x, tensorEnergy (T x) (D x) τ ∂μ) (𝓝[>] 0)
      (𝓝 (∫ x, 2 * Real.sqrt (D x) ∂μ)) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.tensorEnergy

def OAI.CircleDomainRigidity.FiniteTransfer.covectorTrace line 106
Source documentation
Trace of the Gram tensor formed from a finite list of planar covectors.
```
def covectorTrace (x y : ℕ → ℝ) (n : ℕ) : ℝ :=
…
```
def OAI.CircleDomainRigidity.FiniteTransfer.covectorDet line 110
Source documentation
Determinant of the same Gram tensor.
```
def covectorDet (x y : ℕ → ℝ) (n : ℕ) : ℝ :=
…
```
theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorTrace_nonneg line 114
theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorDet_nonneg line 118
theorem OAI.CircleDomainRigidity.FiniteTransfer.covector_discriminant_nonneg line 123