HopfTranslationOrbits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Contracting translations of conditional pairs

The Hopf argument applies to forward iterates whenever their relative translation contracts in the acting group. This formulation also works for measurable observables with a countably separated target.

theorem OAI.DukePrimeDegree.ae_eq_of_contracting_pair_orbits line 24

theorem OAI.DukePrimeDegree.ae_conditional_eq_of_contracting_orbits line 62

Source documentation

The actual conditional kernel version of the translation criterion.

theorem ae_conditional_eq_of_contracting_orbits
    {S B : Type*} [MeasurableSpace S] [MeasurableSpace B]
    [StandardBorelSpace B] [Nonempty B]
    (μ : Measure X) [μ.Regular]
    (ρ : Measure (S × B)) [IsFiniteMeasure ρ]
    (R : S × B → X) (hR : Measurable R) (hRμ : ρ.map R ≤ μ)
    (T : X → X) (hT : MeasurePreserving T μ μ)
    (a : ℕ → ((S × B) × B) → G)
    (ha : ∀ᵐ z ∂conditionalPairMeasure ρ,
      Tendsto (fun n => a n z) atTop (𝓝 1))
    (hpair : ∀ᵐ z ∂conditionalPairMeasure ρ, ∀ n,
      T^[n] (R (z.1.1, z.2)) = a n z • T^[n] (R z.1))
…

Mentions: OAI.DukePrimeDegree.conditionalPairMeasure