HopfContracting.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Contracting group translations in the Hopf argument

Two orbit points may leave every compact set. It is enough that their relative group translation tends to the identity: every compactly supported observable then has vanishing oscillation, and L¹ approximation identifies invariant observables along the pair.

lemma OAI.DukePrimeDegree.integral_compact_observable_of_contracting_pairs line 26

theorem OAI.DukePrimeDegree.ae_eq_of_contracting_translation_pairs line 60

Source documentation

The measurable stable-pair conclusion follows from contraction in the acting group, with no compactness assumption on the orbit points.

theorem ae_eq_of_contracting_translation_pairs
    (μ : Measure X) [μ.Regular] (nu : Measure Z) [IsFiniteMeasure nu]
    (p q : ℕ → Z → X) (hp : ∀ n, Measurable (p n)) (hq : ∀ n, Measurable (q n))
    (hpμ : ∀ n, nu.map (p n) ≤ μ) (hqμ : ∀ n, nu.map (q n) ≤ μ)
    (a : ℕ → Z → G)
    (ha : ∀ᵐ z ∂nu, Tendsto (fun n => a n z) atTop (𝓝 1))
    (hpair : ∀ᵐ z ∂nu, ∀ n, q n z = a n z • p n z)
    (f : X → ℝ) (hf : Integrable f μ)
    (hfp : ∀ n, (fun z => f (p n z)) =ᵐ[nu] fun z => f (p 0 z))
    (hfq : ∀ n, (fun z => f (q n z)) =ᵐ[nu] fun z => f (q 0 z)) :
    (fun z => f (p 0 z)) =ᵐ[nu] fun z => f (q 0 z) :=
…