PublishedEKL.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Haar rigidity from root-leaf symmetries

Projective normalization can be removed from root-leaf symmetries, and nontrivial root periods yield invariance under the corresponding unipotent group. Haar measure follows from all root periods, or from a single root and a transitive prime-degree symmetry group.

lemma OAI.DukePrimeDegree.leaf_period_of_projective_multiplier_zero line 24

Source documentation

A projective period of a leaf with zero logarithmic multiplier is an ordinary period.

lemma leaf_period_of_projective_multiplier_zero
    (ν : Measure ℝ) (p : ℝ × ℝ) (hp : projectiveLeafPeriod ν p) (hzero : p.2 = 0) :
    p.1 ∈ realLeafPeriods ν := by
…

lemma OAI.DukePrimeDegree.projectivePeriod_of_based_fixed line 32

Source documentation

Equality with a rebased normalized leaf yields a projective period. The normalizing scalar is recovered from the unit-ball mass.

lemma projectivePeriod_of_based_fixed
    (ν : Measure ℝ) [IsLocallyFiniteMeasure ν] (hunit : ν (Metric.ball 0 1) = 1)
    (t : ℝ) (hfixed : basedRealMeasure ν t = ν) :
    projectiveLeafPeriod ν (-t, Real.log (ν (Metric.ball t 1)).toReal) := by
…

theorem OAI.DukePrimeDegree.ae_intrinsic_projective_multiplier_zero line 58

Source documentation

For a finite invariant ambient measure, the full diagonal scaling covariance forces every projective root-leaf period to have multiplier one. This is the normalization step needed by the low-entropy argument.

theorem ae_intrinsic_projective_multiplier_zero
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    ∀ᵐ x ∂μ, ∀ p : ℝ × ℝ,
      projectiveLeafPeriod (intrinsicRootLeaf hij μ x) p → p.2 = 0 := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow

theorem OAI.DukePrimeDegree.root_invariant_of_projective_leaf_symmetry line 95

Source documentation

Nontrivial projective root-leaf symmetries already imply exact unipotent invariance; no multiplier has to be supplied separately.

theorem root_invariant_of_projective_leaf_symmetry
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (hsym : ∀ᵐ x ∂μ, ∃ p : ℝ × ℝ, p.1 ≠ 0 ∧
      projectiveLeafPeriod (intrinsicRootLeaf hij μ x) p) (a : ℝ) :
    μ.map (fun x => rightAction x (Matrix.SpecialLinearGroup.transvection hij a)) = μ := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow

theorem OAI.DukePrimeDegree.ae_atomless_of_positive_rootInformation line 111

Source documentation

Positive mean root information rules out the Dirac alternative in an ergodic diagonal component. This supplies the nonatomic half of the leafwise-constancy criterion from an entropy contribution.

theorem ae_atomless_of_positive_rootInformation
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (hpos : 0 < rootInformationMean hij μ 1) :
    ∀ᵐ x ∂μ, NullSingletonClass (intrinsicRootLeaf hij μ x) := by
…

theorem OAI.DukePrimeDegree.root_invariant_of_leafwise_constant_nonatomic line 127

Source documentation

A non-atomic root leaf that is almost everywhere unchanged when rebased has a nontrivial translation symmetry.

theorem root_invariant_of_leafwise_constant_nonatomic
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (hatom : ∀ᵐ x ∂μ, NullSingletonClass (intrinsicRootLeaf hij μ x))
    (hfixed : ∀ᵐ x ∂μ, ∀ᵐ t ∂intrinsicRootLeaf hij μ x,
      intrinsicRootLeaf hij μ (rightAction x
        (Matrix.SpecialLinearGroup.transvection hij t)) = intrinsicRootLeaf hij μ x)
    (a : ℝ) :
    μ.map (fun x => rightAction x (Matrix.SpecialLinearGroup.transvection hij a)) = μ := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow

theorem OAI.DukePrimeDegree.isHaar_of_projective_leaf_symmetries line 163

Source documentation

Full root-leaf symmetry identifies Haar probability directly through the elementary-generation theorem for the special linear group.

theorem isHaar_of_projective_leaf_symmetries
    (d : ℕ) (hd : 1 ≤ d) (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (hsym : ∀ (i j : Fin (d + 1)) (hij : i ≠ j),
      ∀ᵐ x ∂μ, ∃ p : ℝ × ℝ, p.1 ≠ 0 ∧
        projectiveLeafPeriod (intrinsicRootLeaf hij μ x) p) :
    IsHaarProbability μ := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow

theorem OAI.DukePrimeDegree.isHaar_of_prime_root_symmetries line 177

Source documentation

In prime degree a transitive symmetry of the root-invariance relation propagates one nontrivial projective leaf symmetry to Haar invariance.

theorem isHaar_of_prime_root_symmetries
    (d : ℕ) (hprime : (d + 1).Prime) (hd : 1 ≤ d)
    (J : Type*) [Group J] [MulAction J (Fin (d + 1))]
    [MulAction.IsPretransitive J (Fin (d + 1))]
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (hperm : ∀ (g : J) i j, rootInvarianceRelation μ i j →
      rootInvarianceRelation μ (g • i) (g • j))
    {i j : Fin (d + 1)} (hij : i ≠ j)
    (hsym : ∀ᵐ x ∂μ, ∃ p : ℝ × ℝ, p.1 ≠ 0 ∧
      projectiveLeafPeriod (intrinsicRootLeaf hij μ x) p) :
…

Mentions: OAI.DukePrimeDegree.diagonalFlow