OAI/NumberTheory/DukePrimeDegree/Dynamics/BlockTransverseDiagonal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Scalar diagonal representatives transverse to the root blocks

After clearing the within-block off-diagonal entries, a positive split diagonal makes all diagonal entries equal. Both corrections belong to the actual invariant subgroup when it contains A and the specified roots. Thus this normalization preserves being outside that subgroup.

  1. def OAI.DukePrimeDegree.balancedDiagonalMean line 22
  2. def OAI.DukePrimeDegree.balancedDiagonalWeights line 25
  3. lemma OAI.DukePrimeDegree.balancedDiagonalWeights_sum line 28
  4. def OAI.DukePrimeDegree.balancedDiagonalCorrection line 35
  5. lemma OAI.DukePrimeDegree.balancedDiagonalCorrection_entry line 38
  6. lemma OAI.DukePrimeDegree.balancedDiagonalCorrection_diagonal line 46
  7. lemma OAI.DukePrimeDegree.balancedDiagonalMean_tendsto line 53
  8. lemma OAI.DukePrimeDegree.balancedDiagonalCorrection_tendsto line 66
  9. theorem OAI.DukePrimeDegree.exists_scalar_block_transverse_sequence line 99

    Source documentation

    Every small matrix has a representative with scalar diagonal and zero within-block off-diagonal entries, using actual elements of L.

    theorem exists_scalar_block_transverse_sequence {n : ℕ} (hn : n ≠ 0)
    (r : Setoid (Fin n)) (L : Subgroup (G n))
    (hroot : ∀ (i j : Fin n) (hij : i ≠ j), r i j → ∀ t : ℝ,
      Matrix.SpecialLinearGroup.transvection hij t ∈ L)
    (hdiag : ∀ (ell : Fin n → ℝ) (hsum : ∑ i, ell i = 0) (t : ℝ),
      diagonalOneParameter ell hsum t ∈ L)
    (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1)) :
    ∃ s b : ℕ → G n, ∃ c : ℕ → ℝ,
      Tendsto s atTop (𝓝 1) ∧ Tendsto b atTop (𝓝 1) ∧
      (∀ k, s k = g k * b k) ∧ (∀ k, b k ∈ L) ∧
      (∀ k, 0 < c k) ∧
      ∀ᶠ k in atTop, (∀ i, (s k).val i i = c k) ∧
…
  10. lemma OAI.DukePrimeDegree.right_corrected_not_mem line 147
  11. theorem OAI.DukePrimeDegree.exists_cross_block_entry_of_scalar_diagonal line 154

    Source documentation

    A nonidentity scalar-diagonal representative must retain a genuine cross-block entry; a positive scalar determinant-one matrix is identity.

    theorem exists_cross_block_entry_of_scalar_diagonal {n : ℕ} (hn : n ≠ 0)
    (r : Setoid (Fin n)) (g : G n) (c : ℝ) (hc : 0 < c)
    (hdiag : ∀ i, g.val i i = c)
    (hwithin : ∀ i j, i ≠ j → r i j → g.val i j = 0)
    (hne : g ≠ 1) : ∃ i j, ¬ r i j ∧ g.val i j ≠ 0 := by
…