OAI/NumberTheory/DukePrimeDegree/Dynamics/WeylAtomicRoots.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coordinate permutations transport atomic intrinsic root leaves

  1. lemma OAI.DukePrimeDegree.reindex_transvection line 13
  2. theorem OAI.DukePrimeDegree.atomic_root_reindex line 26

    Source documentation

    Only the geometric characterization of an atomic leaf is needed; there is no assumed covariance formula for arbitrary intrinsic leaves.

    theorem atomic_root_reindex (d : ℕ) (e : Equiv.Perm (Fin (d+1)))
    {i j : Fin (d+1)} (hij : i ≠ j)
    (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
    (hatom : ∀ᵐ x ∂μ, intrinsicRootLeaf hij μ x=Measure.dirac 0) :
    ∀ᵐ x ∂μ.map (quotientReindex e),
      intrinsicRootLeaf (e.injective.ne hij) (μ.map (quotientReindex e)) x=Measure.dirac 0 := by
…

    Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.quotientReindex