StrongReturns.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous strong returns

The fixed-parameter small-return theorem extends to a whole subgroup by separability and closedness. This removes the parameter-dependent null sets in the exceptional-return argument of EKL (2006), Lemma 4.2.

def OAI.DukePrimeDegree.singleRootCentralizer line 20
lemma OAI.DukePrimeDegree.mem_singleRootCentralizer line 23
lemma OAI.DukePrimeDegree.matrixBall_subset_matrixClosedBall line 29

theorem OAI.DukePrimeDegree.ae_strong_returns_on_chart line 36

Source documentation

On a fixed injectivity chart, one conull set works for every parameter in any subgroup commuting with the contracting diagonal and the root.

theorem ae_strong_returns_on_chart
    (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)) = μ)
    (H : Subgroup (G (d + 1)))
    (hHroot : ∀ b : H, (b : G (d + 1)) ∈ singleRootCentralizer hij)
    (hHdiag : ∀ b : H, ∀ t : ℝ,
      (b : G (d + 1)) * 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)
…

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