ShearingMeasureLimits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A limiting shear preserves the limiting measure

This is the measure step in the unipotent shearing argument. If two families of probability measures have the same weak limit, and one is the translate of the other by converging group elements, the limiting element preserves that measure. Compact observables give uniform control even when the sampled points leave every compact set.

lemma OAI.DukePrimeDegree.compact_observable_varying_smul line 32

Source documentation

Moving translations of a compact observable converge uniformly.

lemma compact_observable_varying_smul
    (f : X → ℝ) (hf : Continuous f) (hc : HasCompactSupport f)
    (a : I → G) (g : G) (ha : Tendsto a l (𝓝 g)) :
    ∀ ε > 0, ∀ᶠ i in l, ∀ x,
      |f (a i • x) - f (g • x)| < ε := by
…

lemma OAI.DukePrimeDegree.integral_compact_observable_varying_smul line 49

Source documentation

The group element and the probability measure can both vary: the integral error from replacing the group element by its limit vanishes.

lemma integral_compact_observable_varying_smul
    (μ : I → ProbabilityMeasure X)
    (f : CompactlySupportedContinuousMap X ℝ)
    (a : I → G) (g : G) (ha : Tendsto a l (𝓝 g)) :
    Tendsto (fun i => (∫ x, f (a i • x) ∂(μ i : Measure X)) -
      ∫ x, f (g • x) ∂(μ i : Measure X)) l (𝓝 0) := by
…

theorem OAI.DukePrimeDegree.map_eq_of_converging_translated_probabilities line 77

Source documentation

A limiting shear belongs to the actual stabilizer of the limiting probability measure. The hypotheses are weak limits and an exact translation relation between approximating measures.

theorem map_eq_of_converging_translated_probabilities
    (μ ν : I → ProbabilityMeasure X) (ρ : ProbabilityMeasure X)
    (hμ : Tendsto μ l (𝓝 ρ)) (hν : Tendsto ν l (𝓝 ρ))
    (a : I → G) (g : G) (ha : Tendsto a l (𝓝 g))
    (htranslate : ∀ᶠ i in l,
      (μ i : Measure X).map (fun x => a i • x) = (ν i : Measure X)) :
    (ρ : Measure X).map (fun x => g • x) = (ρ : Measure X) := by
…

theorem OAI.DukePrimeDegree.map_eq_of_asymptotically_translated_pairs line 110

Source documentation

The sampled group element may vary across the orbit window. Uniform smallness of its error, almost everywhere in each window, is enough. This is the form used with a terminal polynomial shear.

theorem map_eq_of_asymptotically_translated_pairs
    {Z : Type*} [MeasurableSpace Z]
    (taus : I → ProbabilityMeasure Z) (p q : I → Z → X)
    (hp : ∀ i, Measurable (p i)) (hq : ∀ i, Measurable (q i))
    (ρ : ProbabilityMeasure X)
    (hplim : Tendsto (fun i => (taus i).map (p i)) l (𝓝 ρ))
    (hqlim : Tendsto (fun i => (taus i).map (q i)) l (𝓝 ρ))
    (g : G) (b : I → Z → G)
    (hsmall : ∀ U ∈ 𝓝 (1 : G), ∀ᶠ i in l, ∀ᵐ z ∂(taus i : Measure Z), b i z ∈ U)
    (hpair : ∀ᶠ i in l, ∀ᵐ z ∂(taus i : Measure Z),
      q i z = b i z • (g • p i z)) :
    (ρ : Measure X).map (fun x => g • x) = (ρ : Measure X) := by
…