CorrectedPairLimits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compactly corrected generic pairs approach the same point

The common correcting parameters lie in one compact stabilizer patch. After a subsequence, both corrected starting points approach the same quotient point. Their actual invariant means can consequently be compared using a fixed finite continuous approximation.

theorem OAI.DukePrimeDegree.exists_common_corrected_pair_limit line 22

theorem OAI.DukePrimeDegree.exists_corrected_mean_comparison_subsequence line 53

Source documentation

The comparison does not identify the invariant mean with a global constant; it uses the genuine value at each corrected generic point.

theorem exists_corrected_mean_comparison_subsequence {n : ℕ}
    (H : Subgroup (G n)) (K : Set H) (hK : IsCompact K)
    (u : ℕ → H) (hu : ∀ k, u k ∈ K)
    (a b : ℕ → G n) (ha : Tendsto a atTop (𝓝 1)) (hb : Tendsto b atTop (𝓝 1))
    (x : X n) (q F : X n → ℝ) (hF : Continuous F)
    (E : Set (X n)) (ε η : ℝ) (hη : 0 < η)
    (happrox : ∀ y ∈ E, |q y - F y| ≤ ε)
    (hgood : ∀ k, rightAction x (u k : G n) ∈ E ∧
      rightAction x (a k * b k * (u k : G n)) ∈ E) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧
      ∀ᶠ k in atTop,
        |q (rightAction x (u (φ k) : G n)) -
…