OAI/NumberTheory/DukePrimeDegree/Dynamics/GenericMatrixPairs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Small matrix lifts of generic pairs outside a subgroup orbit

If all subgroup orbits are null, a positive-mass generic set contains arbitrarily close pairs from different orbits. Openness of the actual quotient orbit map lifts these pairs to matrices tending to identity, all outside the subgroup. This is a concrete input to polynomial shearing, without a homogeneous-orbit assumption.

  1. def OAI.DukePrimeDegree.rightSubgroupOrbit line 23
  2. lemma OAI.DukePrimeDegree.rightSubgroupOrbit_mk line 26
  3. theorem OAI.DukePrimeDegree.exists_small_matrix_generic_pairs line 38

    Source documentation

    An actual sequence of small matrices transports one good point to other good points and never belongs to the given subgroup.

    theorem exists_small_matrix_generic_pairs {n : ℕ}
    (L : Subgroup (G n)) (μ : Measure (X n)) (E : Set (X n)) (hE : μ E ≠ 0)
    (hnull : ∀ g : G n, μ (range (latticeOrbitPoint g L)) = 0) :
    ∃ x ∈ E, ∃ a : ℕ → G n,
      Tendsto a atTop (𝓝 1) ∧ ∀ k, a k ∉ L ∧ rightAction x (a k) ∈ E := by
…

    Mentions: OAI.DukePrimeDegree.latticeOrbitPoint