InverseEnclosure.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AtomicTriangular.MatrixBounds.isUnit_of_right_residual line 12
Source documentation
A right residual with column norm less than one certifies invertibility.
```
lemma isUnit_of_right_residual (A B : Matrix n n ℝ)
    (h : matNorm (1 - A * B) < 1) : IsUnit A := by
…
```
Mentions: OAI.AtomicTriangular.A, OAI.AtomicTriangular.MatrixBounds.matNorm
lemma OAI.AtomicTriangular.MatrixBounds.inverse_right_residual_identity line 23
lemma OAI.AtomicTriangular.MatrixBounds.inverse_bound_of_right_residual line 30
Source documentation
The right residual bounds the norm of the actual matrix inverse.
```
lemma inverse_bound_of_right_residual (A B : Matrix n n ℝ) (k e : ℝ)
    (hB : matNorm B ≤ k) (hE : matNorm (1 - A * B) ≤ e) (he : e < 1) :
    matNorm A⁻¹ ≤ k / (1 - e) := by
…
```
Mentions: OAI.AtomicTriangular.A, OAI.AtomicTriangular.MatrixBounds.matNorm

lemma OAI.AtomicTriangular.MatrixBounds.inverse_second_order_right_residual_bound line 49

Source documentation

One residual correction leaves a second order error in the inverse.

lemma inverse_second_order_right_residual_bound (A B : Matrix n n ℝ) (k e : ℝ)
    (hB : matNorm B ≤ k) (hE : matNorm (1 - A * B) ≤ e)
    (he0 : 0 ≤ e) (he : e < 1) :
    matNorm (A⁻¹ - (B + B * (1 - A * B))) ≤ k * e ^ 2 / (1 - e) := by
…

Mentions: OAI.AtomicTriangular.A, OAI.AtomicTriangular.MatrixBounds.matNorm

lemma OAI.AtomicTriangular.MatrixBounds.inverse_entry_second_order_right_residual_bound line 72

Source documentation

The matrix norm certificate gives the same second order entrywise enclosure.

lemma inverse_entry_second_order_right_residual_bound (A B : Matrix n n ℝ) (k e : ℝ)
    (hB : matNorm B ≤ k) (hE : matNorm (1 - A * B) ≤ e)
    (he0 : 0 ≤ e) (he : e < 1) (i j : n) :
    |A⁻¹ i j - (B + B * (1 - A * B)) i j| ≤ k * e ^ 2 / (1 - e) := by
…

Mentions: OAI.AtomicTriangular.A, OAI.AtomicTriangular.MatrixBounds.matNorm