FiniteEnergy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Selecting the finite-transfer regularization

For a finite list of planar differentials, a small integral of absolute pairwise wedges produces a regularized metric with small total energy. This proves the energy optimization step of finite transfer, after the geometric filling and staircase construction have supplied the differentials.

def OAI.CircleDomainRigidity.FiniteTransfer.covectorWedges line 22
Source documentation
Each unordered pair is counted exactly once.
```
def covectorWedges (x y : ℕ → ℝ) (n : ℕ) : ℝ :=
…
```

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_regularization_energy_lt line 27

Source documentation

The exact finite-transfer energy choice, using the actually constructed finite family of coordinate differentials.

theorem exists_regularization_energy_lt
    {X : Type*} [MeasurableSpace X] {μ : Measure X}
    (x y : ℕ → X → ℝ) (n : ℕ)
    (hx : ∀ i, Measurable (x i)) (hy : ∀ i, Measurable (y i))
    (htrace : Integrable (fun z => covectorTrace (fun i => x i z) (fun i => y i z) n) μ)
    (hwedge : Integrable (fun z => covectorWedges (fun i => x i z) (fun i => y i z) n) μ)
    {ε : ℝ} (hε : (∫ z, 2 * covectorWedges (fun i => x i z) (fun i => y i z) n ∂μ) < ε) :
    ∃ τ : ℝ, 0 < τ ∧
      (∫ z, tensorEnergy
        (covectorTrace (fun i => x i z) (fun i => y i z) n)
        (covectorDet (fun i => x i z) (fun i => y i z) n) τ ∂μ) < ε := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.covectorTrace, OAI.CircleDomainRigidity.FiniteTransfer.covectorWedges, OAI.CircleDomainRigidity.FiniteTransfer.tensorEnergy, OAI.CircleDomainRigidity.FiniteTransfer.covectorDet