ShearingCollision.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Compactness for pairs with equal leaf data

The last limiting step of the low-entropy argument: equal continuous leaf data on a compact set survive a normalized shearing limit. This isolates the compactness step from the return-time selection and the horospherical separation argument in EKL (2006), Section 4.2.

lemma OAI.DukePrimeDegree.slMatrixDifference_entry_le line 21
lemma OAI.DukePrimeDegree.rootShearLimit_size line 29
theorem OAI.DukePrimeDegree.compact_equal_data_orbit_limit line 44

theorem OAI.DukePrimeDegree.normalized_shearing_forces_horospherical_collision line 74

Source documentation

Equal compact leaf data on normalized shearing pairs force a nonidentity horospherical collision. The measure-theoretic selection of these pairs is a separate step.

theorem normalized_shearing_forces_horospherical_collision
    {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    {Z : Type*} [TopologicalSpace Z] [T2Space Z]
    (K : Set (X n)) (hK : IsCompact K) (F : X n → Z) (hF : ContinuousOn F K)
    (x : ℕ → X n) (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1))
    (t : ℕ → ℝ) (ht : ∀ m, 0 < t m) (htop : Tendsto t atTop atTop)
    {a : ℝ} (ha : 0 < a)
    (hsize : ∀ m, rootShearSize hij (g m) (t m) = a)
    (hsmall : ∀ m, ∀ u ∈ Icc 0 (t m), rootShearSize hij (g m) u ≤ a)
    (hx : ∀ m, x m ∈ K)
    (hy : ∀ m, rightAction (x m)
      (Matrix.SpecialLinearGroup.transvection hij (t m) * g m *
…

Mentions: OAI.DukePrimeDegree.rootShearSize

theorem OAI.DukePrimeDegree.no_small_normalized_shearing_pairs line 104

Source documentation

Continuous data that separate horospherical points rule out small normalized shearing pairs in one compact injectivity region.

theorem no_small_normalized_shearing_pairs
    {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    {Z : Type*} [TopologicalSpace Z] [T2Space Z]
    (K : Set (X n)) (hK : IsCompact K) (F : X n → Z) (hF : ContinuousOn F K)
    (r : ℝ) (hr : 0 < r)
    (hinj : ∀ z ∈ K, Set.InjOn (fun g => rightAction z g) (matrixBall n r))
    (hsep : ∀ z ∈ K, ∀ h : G n, RootHorosphereShape i j h → rightAction z h ∈ K →
      F z = F (rightAction z h) → rightAction z h = z)
    (x : ℕ → X n) (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1))
    (t : ℕ → ℝ) (ht : ∀ m, 0 < t m) (htop : Tendsto t atTop atTop)
    {a : ℝ} (ha : 0 < a) (har : a < r)
    (hsize : ∀ m, rootShearSize hij (g m) (t m) = a)
…

Mentions: OAI.DukePrimeDegree.RootHorosphereShape, OAI.DukePrimeDegree.rootShearSize