ExceptionalReturns.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exceptional-return strengthening

Outside one null set, every sufficiently small lift of a return along the root-pair centralizer, if it centralizes the chosen root, centralizes both roots. In particular this applies to every neutral diagonal return. This is the implication from exceptional to strong exceptional returns in EKL (2006), Lemma 4.2, on the actual arithmetic quotient.

lemma OAI.DukePrimeDegree.rootContractionWeights_swap line 23
lemma OAI.DukePrimeDegree.rootPairCentralizer_commutes_contraction line 28

theorem OAI.DukePrimeDegree.ae_exceptional_returns_are_strong line 50

Source documentation

The null set is independent of the return parameter and of the local chart. The radius may depend on the base point.

theorem ae_exceptional_returns_are_strong
    (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)) = μ) :
    ∀ᵐ x ∂μ, ∃ r : ℝ, 0 < r ∧
      ∀ b : rootPairCentralizer hij, ∀ g ∈ matrixBall (d + 1) r,
        g ∈ singleRootCentralizer hij → rightAction x g = rightAction x b →
          g ∈ rootPairCentralizer hij := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.rootPairCentralizer, OAI.DukePrimeDegree.singleRootCentralizer

theorem OAI.DukePrimeDegree.ae_neutral_diagonal_returns_are_strong line 80

Source documentation

Every neutral diagonal lies in the root-pair centralizer, so the strengthening applies to precisely the return group used by EKL.

theorem ae_neutral_diagonal_returns_are_strong
    (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)) = μ) :
    ∀ᵐ x ∂μ, ∃ r : ℝ, 0 < r ∧
      ∀ (ell : Fin (d + 1) → ℝ) (hell : ∑ a, ell a = 0), ell i = ell j →
        ∀ t : ℝ, ∀ g ∈ matrixBall (d + 1) r,
          g ∈ singleRootCentralizer hij →
          rightAction x g = rightAction x (diagonalOneParameter ell hell t) →
            g ∈ rootPairCentralizer hij := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.singleRootCentralizer, OAI.DukePrimeDegree.rootPairCentralizer