OAI/Analysis/PureInfiniteness/FiniteMatrixDiagonalization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.coefficientMatrix line 16
2. def OAI.WeakPureInfiniteness.updateTwoCoefficients line 19
3. def OAI.WeakPureInfiniteness.updateTwoMultiplier line 22
4. lemma OAI.WeakPureInfiniteness.updateTwoCoefficients_inr line 26
5. lemma OAI.WeakPureInfiniteness.norm_updateTwoMultiplier_le line 32
6. lemma OAI.WeakPureInfiniteness.coefficientMatrix_update_inr line 41
7. lemma OAI.WeakPureInfiniteness.norm_coefficientMatrix_update_le line 49
8. lemma OAI.WeakPureInfiniteness.norm_updateTwoCoefficients_le line 70
9. lemma OAI.WeakPureInfiniteness.coefficientMatrix_update_first line 83
10. lemma OAI.WeakPureInfiniteness.coefficientMatrix_update_second line 89
11. lemma OAI.WeakPureInfiniteness.coefficientMatrix_update_selected line 96
12. lemma OAI.WeakPureInfiniteness.coefficientMatrix_update_other line 103
13. theorem OAI.WeakPureInfiniteness.finite_matrix_diagonalization_uniform line 115

    Source documentation

    Finite diagonalization with an implementer bound independent of the off-diagonal tolerance. Only the positive diagonal entries enter the bound.

    theorem finite_matrix_diagonalization_uniform (hP : MainGap.PropertyP A)
        {n : ℕ} (M₀ η : ℝ) (hη : 0 < η) :
        ∃ C : ℝ, 1 ≤ C ∧ ∀ M : Fin n → Fin n → A,
          (∀ i, 0 ≤ M i i) → (∀ i, ‖M i i‖ ≤ M₀) →
          ∀ ζ : ℝ, 0 < ζ → ∃ d : Fin n → A,
          (∀ i, ‖d i‖ ≤ C) ∧ (∀ i, ‖coefficientMatrix M d i i - M i i‖ < η) ∧
          ∀ i j, i ≠ j → ‖coefficientMatrix M d i j‖ < ζ := by
    …

    Mentions: OAI.MainGap.PropertyP, OAI.WeakPureInfiniteness.coefficientMatrix