ComponentRootPattern.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The measurable root pattern of actual ergodic components

A split diagonal rescales each real root group by a nonzero scalar. Thus it preserves the predicate that the whole root group fixes a measure, even when it moves that measure. For the normalizer-covariant component kernel this gives an invariant measurable event on the component base; it does not assert that individual components are fixed.

lemma OAI.DukePrimeDegree.rootInvarianceRelation_iff_full_root line 23
lemma OAI.DukePrimeDegree.all_root_mem_map_diagonal_iff line 33
lemma OAI.DukePrimeDegree.rootInvarianceRelation_map_diagonal_iff line 57
lemma OAI.DukePrimeDegree.measurableSet_kernel_rootInvarianceRelation line 68

theorem OAI.DukePrimeDegree.ae_component_root_pattern_diagonal line 85

Source documentation

The actual component root pattern is unchanged along the specified diagonal's action on the component base, almost everywhere.

theorem ae_component_root_pattern_diagonal {n : ℕ}
    (H : Subgroup (G n)) (ell : Fin n → ℝ) (hell : ∑ k, ell k = 0) (t : ℝ)
    (ha : diagonalOneParameter ell hell t ∈ Subgroup.normalizer (H : Set (G n)))
    (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (hμ : μ.map (fun x => rightAction x (diagonalOneParameter ell hell t)) = μ)
    (i j : Fin n) :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le H (X n)),
      rootInvarianceRelation
        (condExpKernel μ (actionInvariantSigma H (X n))
          (rightAction z (diagonalOneParameter ell hell t))) i j ↔
      rootInvarianceRelation (condExpKernel μ (actionInvariantSigma H (X n)) z) i j := by
…