CentralizerContraction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded diagonal returns in a root centralizer

A matrix centralizing one root can have entries outside the opposite-root centralizer only in expanding directions of a suitable diagonal flow. Bounded conjugates along arbitrarily late times therefore centralize both roots. This is the matrix step in EKL (2006), Lemma 4.2.

lemma OAI.DukePrimeDegree.eq_zero_of_bounded_exp_mul line 21

lemma OAI.DukePrimeDegree.conjugation_expanding_entry_eq_zero line 34

Source documentation

Each strictly expanding matrix entry must vanish if the conjugates remain bounded along a sequence of times tending to infinity.

lemma conjugation_expanding_entry_eq_zero {n : ℕ}
    (ell : Fin n → ℝ) (hell : ∑ r, ell r = 0) (g : G n)
    {t : ℕ → ℝ} (ht : Tendsto t atTop atTop) (B : ℝ)
    (hb : ∀ᶠ k in atTop, ∀ r s,
      |(diagonalOneParameter ell hell (t k) * g *
        diagonalOneParameter ell hell (-t k)).val r s| ≤ B)
    {r s : Fin n} (hrs : ell s < ell r) : g.val r s = 0 := by
…

theorem OAI.DukePrimeDegree.rootPairCentralizer_of_bounded_conjugates line 47

Source documentation

With the two distinguished weights extremal, bounded conjugates in one root centralizer belong to the common centralizer of opposite roots.

theorem rootPairCentralizer_of_bounded_conjugates {n : ℕ}
    {i j : Fin n} (hij : i ≠ j)
    (ell : Fin n → ℝ) (hell : ∑ r, ell r = 0)
    (hijw : ell j < ell i)
    (hmiddle : ∀ r, r ≠ i → r ≠ j → ell j < ell r ∧ ell r < ell i)
    (g : G n)
    (hg : g * Matrix.SpecialLinearGroup.transvection hij 1 =
      Matrix.SpecialLinearGroup.transvection hij 1 * g)
    {t : ℕ → ℝ} (ht : Tendsto t atTop atTop) (B : ℝ)
    (hb : ∀ᶠ k in atTop, ∀ r s,
      |(diagonalOneParameter ell hell (t k) * g *
        diagonalOneParameter ell hell (-t k)).val r s| ≤ B) :
…

theorem OAI.DukePrimeDegree.ae_rootPairCentralizer_of_recurrent_conjugates line 80

Source documentation

Poincaré recurrence supplies the unbounded sequence needed by the matrix criterion, even when conjugate bounds hold only on returns to a measurable set.

theorem ae_rootPairCentralizer_of_recurrent_conjugates
    {Y : Type*} [MeasurableSpace Y]
    (μ : Measure Y) [IsFiniteMeasure μ]
    (T : Y → Y) (hT : MeasurePreserving T μ μ)
    (E : Set Y) (hE : MeasurableSet E)
    {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (ell : Fin n → ℝ) (hell : ∑ r, ell r = 0)
    (hijw : ell j < ell i)
    (hmiddle : ∀ r, r ≠ i → r ≠ j → ell j < ell r ∧ ell r < ell i)
    (g : Y → G n)
    (hg : ∀ x ∈ E, g x * Matrix.SpecialLinearGroup.transvection hij 1 =
      Matrix.SpecialLinearGroup.transvection hij 1 * g x)
…