RootWeights.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Neutral diagonal directions for root leaves

Root leaves are unchanged along the kernel of their root character. For two nonparallel roots, an explicit diagonal direction is neutral on the first and expands the second. These are the directions used to compare the root foliations in the entropy argument.

lemma OAI.DukePrimeDegree.rootCanonicalWeights_neutral line 21

theorem OAI.DukePrimeDegree.exists_neutral_expanding_weights line 28

Source documentation

Every root which is not equal or opposite to a fixed root is expanded by a diagonal direction which centralizes the fixed root.

theorem exists_neutral_expanding_weights (d : ℕ)
    {i j k l : Fin (d + 1)} (_hij : i ≠ j) (hkl : k ≠ l)
    (hforward : ¬ (k = i ∧ l = j)) (hbackward : ¬ (k = j ∧ l = i)) :
    ∃ ell : Fin (d + 1) → ℝ,
      (∑ r, ell r) = 0 ∧ ell i = ell j ∧ ell l - ell k = 1 := by
…

theorem OAI.DukePrimeDegree.ae_rootLeaf_neutral_diagonal line 59

Source documentation

A diagonal direction in the kernel of a root character fixes its normalized intrinsic leaf measure almost everywhere.

theorem ae_rootLeaf_neutral_diagonal
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (ell : Fin (d + 1) → ℝ) (hell : ∑ r, ell r = 0) (hneutral : ell i = ell j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ) (t : ℝ) :
    ∀ᵐ x ∂μ, intrinsicRootLeaf hij μ
      (rightAction x (diagonalOneParameter ell hell t)) = intrinsicRootLeaf hij μ x := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow