MatrixNormConversion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Entry bounds and the Euclidean norm of coordinate transformations

Huang--Huang (2024), Theorem 4.1 uses the maximum of the absolute matrix entries. The elementary dimension factor below converts that bound into an operator bound before it is used in the coordinate construction.

theorem OAI.RegularPointCoordinates.euclidean_operator_norm_le_of_entries line 21
Source documentation
A deliberately non-sharp dimension factor suffices: all smallness parameters in the transformation theorem can be chosen after dimension.
```
theorem euclidean_operator_norm_le_of_entries {n : ℕ}
    (A : Euclidean n →L[ℝ] Euclidean n) {C : ℝ} (hC : 0 ≤ C)
    (hentry : ∀ i j, |A (EuclideanSpace.single j 1) i| ≤ C) :
    ‖A‖ ≤ (n : ℝ) ^ 2 * C := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.matrix_euclidean_norm_le_of_entries line 56

Source documentation

An entrywise estimate on a published transformation matrix gives the operator norm bound required by the metric iteration.

theorem matrix_euclidean_norm_le_of_entries {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) {C : ℝ} (hC : 0 ≤ C)
    (hentry : ∀ i j, |A i j| ≤ C) :
    ‖Matrix.toEuclideanCLM (n := Fin n) (𝕜 := ℝ) A‖ ≤ (n : ℝ) ^ 2 * C := by
…

theorem OAI.RegularPointCoordinates.matrix_sub_id_norm_le_of_entries line 66

Source documentation

Near identity in the source's entry norm implies near identity in Euclidean operator norm, with the dimension factor kept explicit.

theorem matrix_sub_id_norm_le_of_entries {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) {epsilon : ℝ} (hepsilon : 0 ≤ epsilon)
    (hentry : ∀ i j, |(A - 1) i j| ≤ epsilon) :
    ‖Matrix.toEuclideanCLM (n := Fin n) (𝕜 := ℝ) A - ContinuousLinearMap.id ℝ (Euclidean n)‖ ≤
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.equiv_inverse_norm_le_of_sub_id line 79

Source documentation

A near-identity invertible transformation has a controlled inverse; no inverse bound needs to be separately supplied by the application.

theorem equiv_inverse_norm_le_of_sub_id (A : E ≃L[ℝ] E)
    {delta : ℝ} (hdelta1 : delta < 1)
    (hA : ‖(A : E →L[ℝ] E) - ContinuousLinearMap.id ℝ E‖ ≤ delta) :
    ‖(A.symm : E →L[ℝ] E)‖ ≤ (1 - delta)⁻¹ := by
…

theorem OAI.RegularPointCoordinates.equiv_norm_le_of_sub_id line 96

Source documentation

The forward operator has the matching elementary bound.

theorem equiv_norm_le_of_sub_id (A : E ≃L[ℝ] E)
    {delta : ℝ} (hdelta : 0 ≤ delta)
    (hA : ‖(A : E →L[ℝ] E) - ContinuousLinearMap.id ℝ E‖ ≤ delta) :
    ‖(A : E →L[ℝ] E)‖ ≤ 1 + delta := by
…