HopfPairs.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Invariant observables on asymptotic pairs

This is the measurable part of the stable-leaf argument. The two coordinates of a family of pairs have uniformly dominated marginals. If the coordinates become asymptotic, every integrable observable which is unchanged along both coordinate sequences has equal values on the pair.

The proof uses compactly supported continuous approximation in L¹ and dominated convergence. It requires no ergodicity or pointwise ergodic theorem.

theorem OAI.DukePrimeDegree.integral_compact_observable_difference_tendsto_zero line 32

Source documentation

Compactly supported continuous observables have vanishing mean oscillation on a finite measure of asymptotic pairs.

theorem integral_compact_observable_difference_tendsto_zero
    (nu : Measure Z) [IsFiniteMeasure nu]
    (p q : ℕ → Z → α)
    (hp : ∀ n, Measurable (p n))
    (hq : ∀ n, Measurable (q n))
    (hasymptotic : ∀ᵐ z ∂nu,
      Tendsto (fun n => (p n z, q n z)) atTop (𝓤 α))
    (g : α → ℝ) (hg : Continuous g) (hcompact : HasCompactSupport g) :
    Tendsto (fun n => ∫ z, |g (p n z) - g (q n z)| ∂nu) atTop (𝓝 0) := by
…

theorem OAI.DukePrimeDegree.ae_eq_of_compact_observable_dominated_pairs line 69

Source documentation

An integrable invariant observable is equal on any asymptotic pair family with dominated marginals. This is the Hopf stable-pair principle in the form used for neutral diagonal actions on leaf measures.

theorem ae_eq_of_compact_observable_dominated_pairs
    (μ : Measure α) [μ.Regular] (nu : Measure Z) [IsFiniteMeasure nu]
    (p q : ℕ → Z → α)
    (hp : ∀ n, Measurable (p n))
    (hq : ∀ n, Measurable (q n))
    (hpμ : ∀ n, nu.map (p n) ≤ μ)
    (hqμ : ∀ n, nu.map (q n) ≤ μ)
    (hcompactlim : ∀ g : α → ℝ, Continuous g → HasCompactSupport g →
      Tendsto (fun n => ∫ z, |g (p n z) - g (q n z)| ∂nu) atTop (𝓝 0))
    (f : α → ℝ) (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)) :
…

theorem OAI.DukePrimeDegree.ae_eq_of_asymptotic_dominated_pairs line 146

Source documentation

Asymptotic pairs give the compact-observable condition by uniform continuity and dominated convergence.

theorem ae_eq_of_asymptotic_dominated_pairs
    (μ : Measure α) [μ.Regular] (nu : Measure Z) [IsFiniteMeasure nu]
    (p q : ℕ → Z → α)
    (hp : ∀ n, Measurable (p n))
    (hq : ∀ n, Measurable (q n))
    (hpμ : ∀ n, nu.map (p n) ≤ μ)
    (hqμ : ∀ n, nu.map (q n) ≤ μ)
    (hasymptotic : ∀ᵐ z ∂nu,
      Tendsto (fun n => (p n z, q n z)) atTop (𝓤 α))
    (f : α → ℝ) (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)) :
…

theorem OAI.DukePrimeDegree.ae_eq_of_asymptotic_preserving_pairs line 165

Source documentation

Equal marginals are a useful special case of the dominated-pair principle. No invariance of the joint pair measure is required.

theorem ae_eq_of_asymptotic_preserving_pairs
    (μ : Measure α) [μ.Regular] (nu : Measure Z) [IsFiniteMeasure nu]
    (p q : ℕ → Z → α)
    (hp : ∀ n, MeasurePreserving (p n) nu μ)
    (hq : ∀ n, MeasurePreserving (q n) nu μ)
    (hasymptotic : ∀ᵐ z ∂nu,
      Tendsto (fun n => (p n z, q n z)) atTop (𝓤 α))
    (f : α → ℝ) (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) :=
…

theorem OAI.DukePrimeDegree.ae_eq_of_asymptotic_pair_orbits line 183

Source documentation

The dynamical form: invariant observables agree on pairs whose forward orbits become asymptotic. The pair marginals need only be dominated by the invariant measure, as happens for a foliation chart.

theorem ae_eq_of_asymptotic_pair_orbits
    (μ : Measure α) [μ.Regular] (nu : Measure Z) [IsFiniteMeasure nu]
    (r s : Z → α) (hr : Measurable r) (hs : Measurable s)
    (hrμ : nu.map r ≤ μ) (hsμ : nu.map s ≤ μ)
    (T : α → α) (hT : MeasurePreserving T μ μ)
    (hasymptotic : ∀ᵐ z ∂nu,
      Tendsto (fun n => (T^[n] (r z), T^[n] (s z))) atTop (𝓤 α))
    (f : α → ℝ) (hf : Integrable f μ)
    (hfinv : (fun x => f (T x)) =ᵐ[μ] f) :
    (fun z => f (r z)) =ᵐ[nu] fun z => f (s z) := by
…