OAI/NumberTheory/DukePrimeDegree/Dynamics/OrbitGenericity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing the generic-basepoint condition

A finite invariant measure on a block orbit pushes to an invariant measure on the lattice space. Diagonal recurrence gives a generic basepoint almost everywhere. Changing to that basepoint removes the genericity hypothesis from the prime-degree block-orbit obstruction.

  1. def OAI.DukePrimeDegree.latticeOrbitPoint line 23
  2. lemma OAI.DukePrimeDegree.continuous_latticeOrbitPoint line 34
  3. lemma OAI.DukePrimeDegree.latticeOrbitPoint_rightAction line 39
  4. lemma OAI.DukePrimeDegree.latticeOrbitPoint_map_invariant line 48
  5. lemma OAI.DukePrimeDegree.diagonalFlow_mem_blockMatrixGroup line 66
  6. theorem OAI.DukePrimeDegree.exists_generic_block_orbit_point line 75

    Source documentation

    Every nonzero finite invariant block-orbit measure admits a generic lattice representative in the same actual orbit.

    theorem exists_generic_block_orbit_point {d : ℕ}
    (g : G (d + 1)) (r : Setoid (Fin (d + 1)))
    (μ : Measure (LatticeOrbitQuotient g (blockMatrixGroup r)))
    [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hinv : ∀ h : blockMatrixGroup r,
      μ.map (fun x => latticeOrbitRightAction g (blockMatrixGroup r) x h) = μ) :
    ∃ h : blockMatrixGroup r,
      ∀ v ∈ rowLattice (g * h.val).val, v ≠ 0 → ∀ j, v j ≠ 0 := by
…

    Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.latticeOrbitRightAction

  7. theorem OAI.DukePrimeDegree.block_partition_universal_of_invariant_finite_orbit line 100

    Source documentation

    In prime dimension, every nontrivial block subgroup with a nonzero finite invariant lattice-orbit measure has just one block. The basepoint is arbitrary; genericity is supplied by recurrence.

    theorem block_partition_universal_of_invariant_finite_orbit {d : ℕ}
    (hn : (d + 1).Prime) (g : G (d + 1))
    (r : Setoid (Fin (d + 1))) (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (μ : Measure (LatticeOrbitQuotient g (blockMatrixGroup r)))
    [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hinv : ∀ h : blockMatrixGroup r,
      μ.map (fun x => latticeOrbitRightAction g (blockMatrixGroup r) x h) = μ) :
    ∀ i j, r i j := by
…

    Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.latticeOrbitRightAction