WedgeEnergy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Wedge products control the optimized metric energy

The two-dimensional Cauchy–Binet identity is proved directly for finite lists of coordinate differentials. No rank or determinant identity is assumed. The resulting bound is the pointwise algebra behind the finite-transfer energy estimate.

theorem OAI.CircleDomainRigidity.FiniteTransfer.gramDet_eq_wedgeSquares line 20

Source documentation

Cauchy–Binet for the Gram matrix of a finite family of two-dimensional covectors, with each unordered pair counted once.

theorem gramDet_eq_wedgeSquares (x y : ℕ → ℝ) (n : ℕ) :
    (∑ i ∈ range n, x i ^ 2) * (∑ i ∈ range n, y i ^ 2) -
      (∑ i ∈ range n, x i * y i) ^ 2 =
    ∑ j ∈ range n, ∑ i ∈ range j, (x i * y j - x j * y i) ^ 2 := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.sqrt_gramDet_le_wedges line 46
Source documentation
The square root of the Gram determinant is bounded by the sum of the absolute wedge products. This uses the full finite list without a pairwise-independence assumption.
```
theorem sqrt_gramDet_le_wedges (x y : ℕ → ℝ) (n : ℕ) :
    Real.sqrt ((∑ i ∈ range n, x i ^ 2) * (∑ i ∈ range n, y i ^ 2) -
      (∑ i ∈ range n, x i * y i) ^ 2) ≤
    ∑ j ∈ range n, ∑ i ∈ range j, |x i * y j - x j * y i| := by
…
```