OAI/NumberTheory/DukePrimeDegree/Geometry/WeylRootLeaves.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Numerical covariance of the intrinsic root leaves under permutations

The actual normalized leaf is identified in reindexed boxes by disintegration on arbitrarily long root intervals. The time coordinate and its unit ball do not change, so the normalized measures themselves agree.

  1. lemma OAI.DukePrimeDegree.ae_root_free_reindex line 19
  2. theorem OAI.DukePrimeDegree.RootBox.ae_leafMeasure_reindex line 44
  3. lemma OAI.DukePrimeDegree.RootBox.ae_basedLeaf_reindex line 101
  4. lemma OAI.DukePrimeDegree.RootBox.ae_intrinsicRootLeaf_reindex_restrict line 117
  5. theorem OAI.DukePrimeDegree.ae_intrinsicRootLeaf_reindex line 139

    Source documentation

    Numeric leaf covariance on the actual quotient, not just preservation of the atomic/non-atomic alternative.

    theorem ae_intrinsicRootLeaf_reindex {n : ℕ} (e : Equiv.Perm (Fin n))
    {i j : Fin n} (hij : i ≠ j) (μ : Measure (X n)) [IsFiniteMeasure μ]
    (hfree : ∀ᵐ x ∂μ, ∀ t : ℝ,
      rightAction x (Matrix.SpecialLinearGroup.transvection hij t) = x → t = 0) :
    ∀ᵐ x ∂μ, intrinsicRootLeaf (e.injective.ne hij) (μ.map (quotientReindex e))
      (quotientReindex e x) = intrinsicRootLeaf hij μ x := by
…

    Mentions: OAI.DukePrimeDegree.quotientReindex