CovectorConstantRecovery.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Recovering the displacement from the two-center affine constant

theorem OAI.RegularPointCoordinates.covector_norm_le_two_comp line 13
Source documentation
Right composition with a near-identity coordinate operator controls the norm of a constant covector.
```
theorem covector_norm_le_two_comp {n : ℕ} (A : Euclidean n →L[ℝ] Euclidean n)
    (hA : ‖A - 1‖ ≤ 1 / 2) (c : Euclidean n →L[ℝ] ℝ) :
    ‖c‖ ≤ 2 * ‖c.comp A‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.covector_constant_recovery line 30

Source documentation

The controlled commutator constant and matrix difference recover the actual displacement covector. No inverse matrix is introduced.

theorem covector_constant_recovery {n : ℕ}
    (Ax Az : Euclidean n →L[ℝ] Euclidean n) (d c : Euclidean n →L[ℝ] ℝ)
    (hx : ‖Ax - 1‖ ≤ 1 / 2) (hc : c = d.comp Ax)
    {L η M : ℝ} (hB : ‖Az - Ax‖ ≤ L) (hM : ‖c‖ ≤ M)
    (hconst : ‖c.comp (Az - 1)‖ ≤ η) :
    ‖c - d‖ ≤ 2 * (η + M * L) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean