HomogeneousComponents.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating homogeneous components

Invariance of almost every component in a measurable decomposition passes to the ambient measure, and ambient genericity passes back to almost every component. The orbit obstruction then identifies Haar measure under the stated homogeneous-decomposition hypothesis.

lemma OAI.DukePrimeDegree.map_bind_eq_of_ae_component_invariant line 22

theorem OAI.DukePrimeDegree.isHaar_of_prime_homogeneous_decomposition line 38

Source documentation

A homogeneous decomposition with a common A-normalized orbit group is enough for prime-degree Haar rigidity. All remaining hypotheses are concrete orbit and root data; no entropy rigidity implication is assumed.

theorem isHaar_of_prime_homogeneous_decomposition {Z : Type*} [MeasurableSpace Z]
    (d : ℕ) (hprime : (d + 1).Prime)
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (r : Setoid (Fin (d + 1)))
    (hr : ∀ i j, r i j ↔ rootInvarianceRelation μ i j)
    (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (L : Subgroup (G (d + 1))) (hclosed : IsClosed (L : Set (G (d + 1))))
    (hnormal : ∀ (ell : Fin (d + 1) → ℝ) (hsum : ∑ a, ell a = 0) (t : ℝ),
      ∀ h ∈ L, diagonalOneParameter ell hsum t * h * diagonalOneParameter ell hsum (-t) ∈ L)
    (hroot : ∀ i j (hij : i ≠ j), r i j →
      Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
…

Mentions: OAI.DukePrimeDegree.diagonalFlow