OAI/NumberTheory/DukePrimeDegree/Dynamics/CentralizerFlow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Small centralizer factors in late diagonal returns

The root-pair centralizer supplies a scalar double block and a complementary matrix. A fixed neighborhood controls that complementary matrix; late neutral diagonal times separate its spectrum and keep the scalar away from the rational units.

  1. def OAI.DukePrimeDegree.complementaryMatrix line 21
  2. lemma OAI.DukePrimeDegree.rootPairCentralizer_block_explicit line 25
  3. lemma OAI.DukePrimeDegree.diagonal_mem_rootPairCentralizer line 40
  4. lemma OAI.DukePrimeDegree.complementaryMatrix_diagonal_mul line 60
  5. lemma OAI.DukePrimeDegree.continuous_complementaryMatrix line 71
  6. lemma OAI.DukePrimeDegree.complementaryMatrix_one line 79
  7. lemma OAI.DukePrimeDegree.eventually_separated_scaled_weights line 84
  8. lemma OAI.DukePrimeDegree.eventually_scalar_between_zero_one line 101
  9. lemma OAI.DukePrimeDegree.eventually_small_centralizer_blocks line 116

    Source documentation

    A fixed identity neighborhood simultaneously controls the scalar and complementary blocks of every centralizer factor.

    lemma eventually_small_centralizer_blocks {n m : ℕ}
    (e : Fin n ≃ Fin 2 ⊕ Fin m)
    (hij : e.symm (Sum.inl 0) ≠ e.symm (Sum.inl 1)) :
    ∀ᶠ g : rootPairCentralizer hij in 𝓝 1,
      0 < g.val.val (e.symm (Sum.inl 0)) (e.symm (Sum.inl 0)) ∧
      g.val.val (e.symm (Sum.inl 0)) (e.symm (Sum.inl 0)) < Real.exp 1 ∧
      ∀ r, ∑ s, ‖(complementaryMatrix e g.val - 1) r s‖ < spectralRelativeRadius := by
…

    Mentions: OAI.DukePrimeDegree.rootPairCentralizer, OAI.DukePrimeDegree.complementaryMatrix, OAI.DukePrimeDegree.spectralRelativeRadius