WedgeEstimate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Wedge estimate for cutoff staircase coordinates

The common cutoff differential makes the quadratic error term vanish. The remaining terms have exactly the bounds used before taking independent shift expectations in the finite-transfer construction.

def OAI.CircleDomainRigidity.FiniteTransfer.planarWedge line 15
theorem OAI.CircleDomainRigidity.FiniteTransfer.planarWedge_cutoff_expansion line 18
Source documentation
The two error covectors have the same direction, so their wedge is zero.
```
theorem planarWedge_cutoff_expansion (u v c : ℝ × ℝ) (q p r s : ℝ) :
    planarWedge (q • u + r • c) (p • v + s • c) =
      q * p * planarWedge u v + q * s * planarWedge u c + r * p * planarWedge c v := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarWedge

theorem OAI.CircleDomainRigidity.FiniteTransfer.abs_planarWedge_cutoff_le line 25

Source documentation

Pointwise bound for the wedge of two modified coordinate gradients.

theorem abs_planarWedge_cutoff_le (u v c : ℝ × ℝ) {q p r s h : ℝ}
    (hq : 0 ≤ q) (hp : 0 ≤ p) (hr : |r| ≤ h) (hs : |s| ≤ h) :
    |planarWedge (q • u + r • c) (p • v + s • c)| ≤
      q * p * |planarWedge u v| + h * q * |planarWedge u c| +
        h * p * |planarWedge c v| := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarWedge