MetricEnergy.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The regularized metric energy in finite transfer

For the two eigenvalues of the positive semidefinite tensor formed by the coordinate differentials, this is the energy density for the regularized metric A + τ g₀. These estimates are the scalar analytic step in the finite-transfer construction. In particular, rank-one fillings have vanishing limiting energy.

def OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy line 23
Source documentation
Sum of the two coordinate energy contributions in an eigenframe.
```
def metricEnergy (a b τ : ℝ) : ℝ :=
…
```
theorem OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy_eq_density line 28
Source documentation
This is the density formula written in the manuscript.
```
theorem metricEnergy_eq_density {a b τ : ℝ}
    (ha : 0 ≤ a) (hb : 0 ≤ b) (hτ : 0 < τ) :
    metricEnergy a b τ =
      (2 * a * b + τ * (a + b)) / Real.sqrt ((a + τ) * (b + τ)) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy
theorem OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy_le_trace line 45
Source documentation
The regularized density has the original trace as a uniform bound. This bound is independent of the positive regularization parameter.
```
theorem metricEnergy_le_trace {a b τ : ℝ}
    (ha : 0 ≤ a) (hb : 0 ≤ b) (hτ : 0 < τ) :
    metricEnergy a b τ ≤ a + b := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy
theorem OAI.CircleDomainRigidity.FiniteTransfer.tendsto_energy_term line 59
theorem OAI.CircleDomainRigidity.FiniteTransfer.tendsto_metricEnergy line 84
Source documentation
The limiting energy is twice the square root of the determinant.
```
theorem tendsto_metricEnergy {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    Tendsto (metricEnergy a b) (𝓝[>] 0) (𝓝 (2 * Real.sqrt (a * b))) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy
theorem OAI.CircleDomainRigidity.FiniteTransfer.tendsto_metricEnergy_rank_one line 93
Source documentation
Rank-one tensors contribute zero in the regularized limit.
```
theorem tendsto_metricEnergy_rank_one {a b : ℝ}
    (ha : 0 ≤ a) (hb : 0 ≤ b) (hrank : a * b = 0) :
    Tendsto (metricEnergy a b) (𝓝[>] 0) (𝓝 0) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy