TwoCenterCommutator.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The two-center commutator estimate

Near-identity radial matrices allow absorption of the commutator error. The constant coefficient then recovers the coordinate difference between the two centers with an error proportional to the same defect.

theorem OAI.RegularPointCoordinates.radial_commutator_norm_le line 21
Source documentation
Near the identity, the commutator appearing in the two-center radial identities controls the difference of the two normalization matrices.
```
theorem radial_commutator_norm_le (A B : E →L[ℝ] E)
    (hA : ‖A - 1‖ ≤ 1 / 4) {η : ℝ}
    (herror : ‖B * A - (A - 1) * B‖ ≤ η) : ‖B‖ ≤ 2 * η := by
…
```
theorem OAI.RegularPointCoordinates.norm_le_two_mul_norm_of_near_id line 41
Source documentation
An approximate identity controls vectors from below without choosing an inverse.
```
theorem norm_le_two_mul_norm_of_near_id (A : E →L[ℝ] E)
    (hA : ‖A - 1‖ ≤ 1 / 2) (v : E) : ‖v‖ ≤ 2 * ‖A v‖ := by
…
```

theorem OAI.RegularPointCoordinates.two_center_constant_recovery line 54

Source documentation

The constant recovered from the radial identities is close to the actual coordinate difference, with error proportional to the same defect.

theorem two_center_constant_recovery (Ax Az : E →L[ℝ] E) (δ c : E)
    (hx : ‖Ax - 1‖ ≤ 1 / 2) (hz : ‖Az - 1‖ ≤ 1 / 4)
    (hc : c = Ax δ) {η M : ℝ} (hM : ‖c‖ ≤ M)
    (hcomm : ‖(Az - Ax) * Az - (Az - 1) * (Az - Ax)‖ ≤ η)
    (hconst : ‖(Az - 1) c‖ ≤ η) :
    ‖Az - Ax‖ ≤ 2 * η ∧ ‖δ - c‖ ≤ 2 * η * (1 + 2 * M) := by
…