SmallReturns.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Small quotient returns centralize both roots

For a fixed neutral return parameter, compact sets of possible small return matrices give measurable sets of returning points. Conjugation in the contracting direction preserves the single-root centralizer ball; uniqueness of quotient lifts then identifies returning matrices exactly. Poincaré recurrence proves the fixed-parameter form of EKL Lemma 4.2.

def OAI.DukePrimeDegree.compactReturnSet line 22
lemma OAI.DukePrimeDegree.isClosed_compactReturnSet line 25

theorem OAI.DukePrimeDegree.ae_small_rootCentralizer_return_in_pair line 41

Source documentation

A fixed neutral return parameter has, almost everywhere, no small single-root-centralizing lift outside the opposite-root centralizer.

theorem ae_small_rootCentralizer_return_in_pair
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (b : G (d + 1))
    (hcomm : ∀ t : ℝ,
      b * diagonalOneParameter (rootContractionWeights i j) (rootContractionWeights_sum i j) t =
        diagonalOneParameter (rootContractionWeights i j) (rootContractionWeights_sum i j) t * b)
    (r R : ℝ) (hr : 0 ≤ r) (hrR : r < R)
    (U : Set (X (d + 1))) (hU : MeasurableSet U)
    (hinj : ∀ x ∈ U, Set.InjOn (fun g => rightAction x g) (matrixBall (d + 1) R))
    (K : Set (G (d + 1))) (hK : IsCompact K)
…

Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.rootContractionWeights, OAI.DukePrimeDegree.rootContractionWeights_sum