WeylRootInformation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual root information and coefficients under coordinate permutations

The reindexed measure is the pushforward on the arithmetic quotient. The preceding box-level transport proves covariance of the normalized intrinsic leaves, so their small-ball logarithms and integrated coefficients agree.

theorem OAI.DukePrimeDegree.ae_rootInformation_reindex line 22
theorem OAI.DukePrimeDegree.rootInformationMean_reindex line 32

theorem OAI.DukePrimeDegree.canonicalRootCoefficient_reindex line 49

Source documentation

No entropy formula is used to permute the actual canonical root coefficients; this follows by transporting their defining leaf integrals.

theorem canonicalRootCoefficient_reindex (d : ℕ) (e : Equiv.Perm (Fin (d + 1)))
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (i j : Fin (d + 1)) :
    canonicalRootCoefficient d (μ.map (quotientReindex e)) (e i) (e j) =
      canonicalRootCoefficient d μ i j := by
…

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

theorem OAI.DukePrimeDegree.rootEntropyForm_canonical_reindex line 67

Source documentation

The complete finite root-information form is unchanged when both the measure and the diagonal weights are reindexed.

theorem rootEntropyForm_canonical_reindex (d : ℕ)
    (e : Equiv.Perm (Fin (d + 1))) (μ : Measure (X (d + 1)))
    [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (ell : Fin (d + 1) → ℝ) :
    rootEntropyForm (canonicalRootCoefficient d (μ.map (quotientReindex e)))
        (fun i => ell (e.symm i)) =
      rootEntropyForm (canonicalRootCoefficient d μ) ell := by
…

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