DeterminantLowerNorm.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative invertibility from a determinant lower bound

Compactness bounds the adjugate on the unit ball. Homogeneity then gives the polynomial loss needed to choose injective patches for polynomial maps.

theorem OAI.PolycyclicRecognition.exists_adjugate_norm_bound line 22

theorem OAI.PolycyclicRecognition.determinant_mul_norm_le_adjugate_mul_norm line 41

Source documentation

The adjugate identity bounds below the action of the original matrix.

theorem determinant_mul_norm_le_adjugate_mul_norm {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) (v : Fin n → ℝ) :
    |A.det| * ‖v‖ ≤ ‖A.adjugate‖ * ‖A *ᵥ v‖ := by
…

theorem OAI.PolycyclicRecognition.exists_determinant_lower_norm_bound line 52

Source documentation

Uniform lower norm control for all matrices with bounded norm and a prescribed positive determinant lower bound.

theorem exists_determinant_lower_norm_bound (n : ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) (L η : ℝ),
      0 < L → ‖A‖ ≤ L → η ≤ |A.det| → ∀ v,
      η * ‖v‖ ≤ (C * L ^ (n - 1)) * ‖A v‖ := by
…