OwnLeafSeparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Separation along a noninvariant root leaf

This is the root-leaf separation used in EKL (2006), Lemma 4.4(2). The projective multiplier vanishes by diagonal recurrence, and ergodicity makes every translation period trivial unless the ambient measure is invariant under the root group. No product-structure assertion for a larger horospherical group is included here.

theorem OAI.DukePrimeDegree.ae_based_rootLeaf_eq_only_at_zero line 24

Source documentation

In the noninvariant ergodic case, a normalized leaf cannot equal a nontrivial rebasing of itself. This is pointwise in the rebase parameter.

theorem ae_based_rootLeaf_eq_only_at_zero
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (hnot : ¬ ∀ a : ℝ, μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij a)) = μ) :
    ∀ᵐ x ∂μ, ∀ t : ℝ,
      basedRealMeasure (intrinsicRootLeaf hij μ x) t = intrinsicRootLeaf hij μ x → t = 0 := by
…

theorem OAI.DukePrimeDegree.ae_rootLeaf_separates_own_fiber line 54

Source documentation

On almost every conditional root fiber, equality of the intrinsic leaves detects the original point in the noninvariant ergodic case.

theorem ae_rootLeaf_separates_own_fiber
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (hnot : ¬ ∀ a : ℝ, μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij a)) = μ) :
    ∀ᵐ x ∂μ, ∀ᵐ t ∂intrinsicRootLeaf hij μ x,
      (intrinsicRootLeaf hij μ (rightAction x
        (Matrix.SpecialLinearGroup.transvection hij t)) = intrinsicRootLeaf hij μ x ↔ t = 0) := by
…