SpectralPerturbation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Separated real spectra under small perturbations

The spectral step in EKL (2006), Lemma 5.3, can be obtained from diagonal row dominance and the intermediate value theorem. The determinant keeps its sign along a perturbation whose row sums are smaller than the corresponding diagonal entries. Opposite endpoint signs then locate a real characteristic root in each separated interval.

lemma OAI.DukePrimeDegree.det_diagonal_add_ne_zero_of_row_norm line 29
lemma OAI.DukePrimeDegree.det_diagonal_add_same_sign line 49
lemma OAI.DukePrimeDegree.continuous_has_root_of_mul_neg line 76

theorem OAI.DukePrimeDegree.charpoly_has_root_of_diagonal_bracket line 93

Source documentation

A diagonal root bracket survives perturbations controlled by row sums.

theorem charpoly_has_root_of_diagonal_bracket
    (w : ι → ℝ) (E : Matrix ι ι ℝ) {a b : ℝ} (hab : a < b)
    (ha : ∀ i, ∑ j, ‖E i j‖ < ‖a - w i‖)
    (hb : ∀ i, ∑ j, ‖E i j‖ < ‖b - w i‖)
    (hsign : (∏ i, (a - w i)) * (∏ i, (b - w i)) < 0) :
    ∃ x ∈ Ioo a b, (diagonal w + E).charpoly.eval x = 0 := by
…

lemma OAI.DukePrimeDegree.diagonal_bracket_sign line 122

theorem OAI.DukePrimeDegree.charpoly_roots_of_separated_brackets line 138

Source documentation

Disjoint brackets around all diagonal entries supply every characteristic root. The bounds are on the actual perturbation, not on an assumed spectrum.

theorem charpoly_roots_of_separated_brackets
    (w : ι → ℝ) (E : Matrix ι ι ℝ) (a b : ι → ℝ)
    (ha : ∀ i, a i < w i) (hb : ∀ i, w i < b i)
    (hout : ∀ i j, j ≠ i → w j < a i ∨ b i < w j)
    (hdis : ∀ i j, i ≠ j → b i ≤ a j ∨ b j ≤ a i)
    (hEa : ∀ i k, ∑ j, ‖E k j‖ < ‖a i - w k‖)
    (hEb : ∀ i k, ∑ j, ‖E k j‖ < ‖b i - w k‖) :
    ∃ r : ι → ℝ, (∀ i, r i ∈ Ioo (a i) (b i) ∧
      (diagonal w + E).charpoly.eval (r i) = 0) ∧
      Function.Injective r ∧
      (diagonal w + E).charpoly.roots = (Finset.univ.image r).val ∧
      (diagonal w + E).charpoly.Splits ∧
…