OAI/NumberTheory/DukePrimeDegree/Geometry/MatrixConjugationDensity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.ae_zero_of_mul_map_eq line 28
2. def OAI.DukePrimeDegree.diagonalMatrixConjugation line 52

   Source documentation

   Conjugation by the split real diagonal one-parameter subgroup.

   def diagonalMatrixConjugation {n : ℕ} (ell : Fin n → ℝ) (t : ℝ)
       (M : Matrix (Fin n) (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ :=
   …

3. lemma OAI.DukePrimeDegree.diagonalMatrixConjugation_entry line 57
4. lemma OAI.DukePrimeDegree.continuous_diagonalMatrixConjugation line 65
5. theorem OAI.DukePrimeDegree.ae_matrix_entry_zero_of_split_invariance line 76

   Source documentation

   Split diagonal invariance annihilates every nonzero weight.

   theorem ae_matrix_entry_zero_of_split_invariance {n : ℕ}
       (μ : Measure (Matrix (Fin n) (Fin n) ℝ)) [IsFiniteMeasure μ]
       (ell : Fin n → ℝ)
       (hdiag : ∀ t : ℝ, μ.map (diagonalMatrixConjugation ell t) = μ)
       (i j : Fin n) (hij : ell i ≠ ell j) : ∀ᵐ M ∂μ, M i j = 0 := by
   …

   Mentions: OAI.DukePrimeDegree.diagonalMatrixConjugation

6. theorem OAI.DukePrimeDegree.ae_diagonal_of_split_invariance line 105

   Source documentation

   For a regular split diagonal subgroup, an invariant finite matrix measure is supported on the diagonal matrix space.

   theorem ae_diagonal_of_split_invariance {n : ℕ}
       (μ : Measure (Matrix (Fin n) (Fin n) ℝ)) [IsFiniteMeasure μ]
       (ell : Fin n → ℝ) (hell : Function.Injective ell)
       (hdiag : ∀ t : ℝ, μ.map (diagonalMatrixConjugation ell t) = μ) :
       ∀ᵐ M ∂μ, M = Matrix.diagonal (fun i => M i i) := by
   …

   Mentions: OAI.DukePrimeDegree.diagonalMatrixConjugation

7. def OAI.DukePrimeDegree.rootMatrixConjugation line 127

   Source documentation

   Conjugation by a root unipotent matrix.

   def rootMatrixConjugation {n : ℕ} (i j : Fin n) (t : ℝ)
       (M : Matrix (Fin n) (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ :=
   …

8. lemma OAI.DukePrimeDegree.continuous_rootMatrixConjugation line 131
9. theorem OAI.DukePrimeDegree.ae_diagonal_entries_eq_of_root_invariance line 138

   Source documentation

   Once the matrix measure is diagonal, one invariant root forces the two corresponding diagonal entries to coincide.

   theorem ae_diagonal_entries_eq_of_root_invariance {n : ℕ}
       (μ : Measure (Matrix (Fin n) (Fin n) ℝ))
       (hD : ∀ᵐ M ∂μ, M = Matrix.diagonal (fun i => M i i))
       (i j : Fin n) (hij : i ≠ j)
       (hroot : μ.map (rootMatrixConjugation i j 1) = μ) :
       ∀ᵐ M ∂μ, M i i = M j j := by
   …

   Mentions: OAI.DukePrimeDegree.rootMatrixConjugation

10. theorem OAI.DukePrimeDegree.ae_blockScalar_of_conjugation_invariance line 170

    Source documentation

    Finite matrix measures invariant under split diagonals and the within-block root groups are concentrated on the block-scalar algebra.

    theorem ae_blockScalar_of_conjugation_invariance {n : ℕ}
        (μ : Measure (Matrix (Fin n) (Fin n) ℝ)) [IsFiniteMeasure μ]
        (ell : Fin n → ℝ) (hell : Function.Injective ell)
        (hdiag : ∀ t : ℝ, μ.map (diagonalMatrixConjugation ell t) = μ)
        (r : Setoid (Fin n))
        (hroot : ∀ i j, i ≠ j → r i j → μ.map (rootMatrixConjugation i j 1) = μ) :
        ∀ᵐ M ∂μ, M ∈ blockScalarAlgebra r := by
    …

    Mentions: OAI.DukePrimeDegree.diagonalMatrixConjugation, OAI.DukePrimeDegree.rootMatrixConjugation, OAI.DukePrimeDegree.blockScalarAlgebra

11. theorem OAI.DukePrimeDegree.support_subset_blockScalar_of_conjugation_invariance line 195

    Source documentation

    The same conclusion holds at every point of the measure's support. This is the form used by a continuous conjugation-orbit map.

    theorem support_subset_blockScalar_of_conjugation_invariance {n : ℕ}
        (μ : Measure (Matrix (Fin n) (Fin n) ℝ)) [IsFiniteMeasure μ]
        (ell : Fin n → ℝ) (hell : Function.Injective ell)
        (hdiag : ∀ t : ℝ, μ.map (diagonalMatrixConjugation ell t) = μ)
        (r : Setoid (Fin n))
        (hroot : ∀ i j, i ≠ j → r i j → μ.map (rootMatrixConjugation i j 1) = μ) :
        μ.support ⊆ (blockScalarAlgebra r : Set (Matrix (Fin n) (Fin n) ℝ)) := by
    …

    Mentions: OAI.DukePrimeDegree.diagonalMatrixConjugation, OAI.DukePrimeDegree.rootMatrixConjugation, OAI.DukePrimeDegree.blockScalarAlgebra