ComponentRootConstancy.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

No new invariant roots on the component base

Diagonal covariance makes each full-root invariance event invariant on the parameter space. Diagonal ergodicity makes that event null or conull. In the conull case, integration of the actual conditional measures gives root invariance of the original measure. This conclusion does not assume that the individual conditional measures are diagonal invariant.

lemma OAI.DukePrimeDegree.translation_mem_of_ae_kernel_invariant line 22
lemma OAI.DukePrimeDegree.root_mem_of_ae_kernel_invariant line 34

theorem OAI.DukePrimeDegree.ae_component_root_implies_ambient_root line 48

Source documentation

On the actual invariant-sigma conditional measures, a root can be present on a positive set of parameters only if it fixes the ambient diagonal-ergodic measure. The normalizer condition concerns the subgroup used for conditioning, not the stabilizer of each component.

theorem ae_component_root_implies_ambient_root
    (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)) μ]
    {i j : Fin (d + 1)} (hij : i ≠ j) :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le H (X (d + 1))),
      (∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ invariantRightSubgroup
        (condExpKernel μ (actionInvariantSigma H (X (d + 1))) z)) →
      ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ invariantRightSubgroup μ := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow

theorem OAI.DukePrimeDegree.ae_rootGenerated_component_no_new_roots line 112

Source documentation

The subgroup generated by the ambient invariant roots has the normalizer property needed above by the explicit diagonal conjugation formula. Thus conditioning on it introduces no new roots almost surely.

theorem ae_rootGenerated_component_no_new_roots
    (d : ℕ) (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    {i j : Fin (d + 1)} (hij : i ≠ j) :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le (invariantRootGeneratedGroup μ) (X (d + 1))),
      (∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ invariantRightSubgroup
        (condExpKernel μ (actionInvariantSigma (invariantRootGeneratedGroup μ) (X (d + 1))) z)) →
      ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ invariantRightSubgroup μ := by
…

theorem OAI.DukePrimeDegree.ae_conditional_root_invariant_of_subgroup_root line 135

Source documentation

Roots in the conditioning subgroup also preserve the conditional measures. Countably many rational times suffice because each actual measure stabilizer is closed.

theorem ae_conditional_root_invariant_of_subgroup_root
    {n : ℕ} (H : Subgroup (G n)) (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (hH : H ≤ invariantRightSubgroup μ) {i j : Fin n} (hij : i ≠ j)
    (hU : ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ H) :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le H (X n)),
      ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ invariantRightSubgroup
        (condExpKernel μ (actionInvariantSigma H (X n)) z) := by
…

theorem OAI.DukePrimeDegree.ae_rootGenerated_component_root_iff line 162

Source documentation

The full-root pattern of the actual invariant-sigma conditional measures agrees almost everywhere with the ambient pattern. This is stronger than a measurable root-pattern assertion and still does not assert diagonal invariance or homogeneity of individual components.

theorem ae_rootGenerated_component_root_iff
    (d : ℕ) (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    {i j : Fin (d + 1)} (hij : i ≠ j) :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le (invariantRootGeneratedGroup μ) (X (d + 1))),
      (∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ invariantRightSubgroup
        (condExpKernel μ (actionInvariantSigma (invariantRootGeneratedGroup μ) (X (d + 1))) z)) ↔
      ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ invariantRightSubgroup μ := by
…