OAI/NumberTheory/DukePrimeDegree/Dynamics/SmallCentralizer.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Compact balls in a root centralizer

The diagonal with weights 1, -1, and 0 contracts the centralizer of the corresponding root in reverse time. In particular, it preserves each closed matrix ball in that centralizer. These compact sets give measurable sets of small returns in the proof of EKL (2006), Lemma 4.2.

  1. def OAI.DukePrimeDegree.matrixClosedBall line 21
  2. lemma OAI.DukePrimeDegree.isCompact_matrixClosedBall line 24
  3. lemma OAI.DukePrimeDegree.mem_matrixClosedBall_iff line 27
  4. lemma OAI.DukePrimeDegree.matrixClosedBall_subset_matrixBall line 33
  5. lemma OAI.DukePrimeDegree.entry_bound_of_mem_matrixClosedBall line 38
  6. def OAI.DukePrimeDegree.rootContractionWeights line 50
  7. lemma OAI.DukePrimeDegree.rootContractionWeights_sum line 53
  8. lemma OAI.DukePrimeDegree.rootContractionWeights_gap line 57
  9. lemma OAI.DukePrimeDegree.rootContractionWeights_middle line 61
  10. lemma OAI.DukePrimeDegree.rootContractionWeights_entry_nonneg line 67
  11. lemma OAI.DukePrimeDegree.rootCentralizer_conjugate line 91
  12. theorem OAI.DukePrimeDegree.rootCentralizer_conjugate_mem_closedBall line 111

    Source documentation

    Reverse diagonal time preserves the closed ball in the single-root centralizer, because every allowed off-diagonal entry contracts.

    theorem rootCentralizer_conjugate_mem_closedBall {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    {r : ℝ} (hr : 0 ≤ r) (g : G n) (hgball : g ∈ matrixClosedBall n r)
    (hg : g * Matrix.SpecialLinearGroup.transvection hij 1 =
      Matrix.SpecialLinearGroup.transvection hij 1 * g) (t : ℝ) (ht : 0 ≤ t) :
    diagonalOneParameter (rootContractionWeights i j) (rootContractionWeights_sum i j) (-t) * g *
      diagonalOneParameter (rootContractionWeights i j) (rootContractionWeights_sum i j) t ∈
        matrixClosedBall n r := by
…

    Mentions: OAI.DukePrimeDegree.matrixClosedBall, OAI.DukePrimeDegree.rootContractionWeights, OAI.DukePrimeDegree.rootContractionWeights_sum