FiniteDiagonalVelocity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Root recovery from finitely many diagonal recurrence statements

For each root, a single diagonal has that root as its unique largest weight. Stability under this one diagonal gives stability under all its positive integer powers, which is enough to project onto that root. Thus the actual component application requires only finitely many recurrence statements, rather than a simultaneous assertion for an uncountable family of diagonal elements.

lemma OAI.DukePrimeDegree.slMatrixConjugation_pow_mem line 24
theorem OAI.DukePrimeDegree.single_mem_of_isolating_diagonal_stability line 35
theorem OAI.DukePrimeDegree.full_root_of_isolating_diagonal_velocity line 61

theorem OAI.DukePrimeDegree.ae_normalized_component_velocity_support line 83

Source documentation

Conditioning on a subgroup normalized by the diagonal action cannot introduce velocity coefficients outside the ambient invariant-root pattern. This applies in particular to a single coordinate block; the individual conditional measures need not be diagonal invariant.

theorem ae_normalized_component_velocity_support
    (d : ℕ) (H : Subgroup (G (d + 1)))
    (hAH : ∀ u : LogCoordinates d,
      diagonalFlow u ∈ Subgroup.normalizer (H : Set (G (d + 1))))
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ] :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le H (X (d + 1))),
      ∀ V ∈ matrixVelocitySpace (invariantRightSubgroup
        (condExpKernel μ (actionInvariantSigma H (X (d + 1))) z)),
      ∀ i j, ¬rootInvarianceRelation μ i j → V i j = 0 := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.matrixVelocitySpace

theorem OAI.DukePrimeDegree.ae_rootGenerated_component_velocity_support line 133

Source documentation

The actual root-generated conditional measures have the required velocity support by the explicit diagonal normalization of their group.

theorem ae_rootGenerated_component_velocity_support
    (d : ℕ) (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ] :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le (invariantRootGeneratedGroup μ) (X (d + 1))),
      ∀ V ∈ matrixVelocitySpace (invariantRightSubgroup
        (condExpKernel μ (actionInvariantSigma (invariantRootGeneratedGroup μ) (X (d + 1))) z)),
      ∀ i j, ¬rootInvarianceRelation μ i j → V i j = 0 := by
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace