SpectralSeparation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The spectral estimate for exceptional returns

EKL (2006), Lemma 5.3, in the form needed for real diagonal return matrices. A fixed neighborhood of the identity works for every set of logarithmic diagonal weights separated by more than one.

def OAI.DukePrimeDegree.spectralRelativeRadius line 21
Source documentation
Uniform relative error allowed by half-unit logarithmic brackets.
```
def spectralRelativeRadius : ℝ := 1 - Real.exp (-(1 / 2 : ℝ))
```
lemma OAI.DukePrimeDegree.spectralRelativeRadius_pos line 23
lemma OAI.DukePrimeDegree.exp_gap_distance line 28
lemma OAI.DukePrimeDegree.logarithmic_gap_brackets line 55

theorem OAI.DukePrimeDegree.real_spectrum_of_logarithmic_gaps line 105

Source documentation

The roots of a small perturbation of a logarithmically separated positive diagonal matrix are real, distinct, and stay in their half-unit log brackets.

theorem real_spectrum_of_logarithmic_gaps (ell : ι → ℝ)
    (hgap : ∀ i j, i ≠ j → 1 < |ell i - ell j|)
    (H : Matrix ι ι ℝ)
    (hH : ∀ i, ∑ j, ‖(H - 1) i j‖ < spectralRelativeRadius) :
    ∃ r : ι → ℝ, Function.Injective r ∧
      (∀ i, 0 < r i ∧ |Real.log (r i) - ell i| < 1 / 2 ∧
        (H * diagonal (fun j => Real.exp (ell j))).charpoly.eval (r i) = 0) ∧
      (H * diagonal (fun j => Real.exp (ell j))).charpoly.roots =
        (Finset.univ.image r).val ∧
      (H * diagonal (fun j => Real.exp (ell j))).charpoly.Splits ∧
      (H * diagonal (fun j => Real.exp (ell j))).charpoly.Separable := by
…

Mentions: OAI.DukePrimeDegree.spectralRelativeRadius

lemma OAI.DukePrimeDegree.eventually_spectral_row_bound line 150
Source documentation
The row bound defines a fixed neighborhood of the identity.
```
lemma eventually_spectral_row_bound :
    ∀ᶠ H : Matrix ι ι ℝ in nhds 1,
      ∀ i, ∑ j, ‖(H - 1) i j‖ < spectralRelativeRadius := by
…
```
Mentions: OAI.DukePrimeDegree.spectralRelativeRadius

theorem OAI.DukePrimeDegree.eventually_real_spectrum_uniform line 164

Source documentation

EKL Lemma 5.3: a single neighborhood works uniformly over the separated weights.

theorem eventually_real_spectrum_uniform :
    ∀ᶠ H : Matrix ι ι ℝ in nhds 1, ∀ ell : ι → ℝ,
      (∀ i j, i ≠ j → 1 < |ell i - ell j|) →
      ∃ r : ι → ℝ, Function.Injective r ∧
        (∀ i, 0 < r i ∧ |Real.log (r i) - ell i| < 1 / 2 ∧
          (H * diagonal (fun j => Real.exp (ell j))).charpoly.eval (r i) = 0) ∧
        (H * diagonal (fun j => Real.exp (ell j))).charpoly.roots =
          (Finset.univ.image r).val ∧
        (H * diagonal (fun j => Real.exp (ell j))).charpoly.Splits ∧
        (H * diagonal (fun j => Real.exp (ell j))).charpoly.Separable := by
…