TupleLiftProjection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Projection of thickened endpoint tuples into increment coordinates

Bounding the auxiliary coordinates costs at most their product volume. The subsequent change from total nilpotent coordinates to increments is Haar preserving, including for noncommutative nilpotent groups.

def OAI.PolycyclicRecognition.tupleIncrementRegion line 23

theorem OAI.PolycyclicRecognition.tuple_lift_projection_volume line 28

Source documentation

The projection estimate needed before applying the polynomial endpoint map to the joint increment set.

theorem tuple_lift_projection_volume (μ : Measure N) [SigmaFinite μ]
    [μ.IsMulLeftInvariant] (ν : Measure D) [SFinite ν] (h : ℕ)
    {K : Set ((Fin h → N) × D)} (hK : IsCompact K)
    {Q : Set D} (hQ : ∀ z ∈ K, z.2 ∈ Q) :
    MeasurableSet (tupleIncrementRegion h K) ∧
      ((Measure.pi fun _ : Fin h => μ).prod ν) K ≤
        (Measure.pi fun _ : Fin h => μ) (tupleIncrementRegion h K) * ν Q := by
…

Mentions: OAI.PolycyclicRecognition.tupleIncrementRegion