SeparatedTupleVolume.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent increment volume from separated ambient endpoint tuples

Thickening chosen lifts gives disjoint cells even when the factor map has a kernel. Projection discards only the volume of the bounded Cartan coordinates; changing to increments preserves the remaining Haar volume.

def OAI.PolycyclicRecognition.tupleFactorAction line 21

theorem OAI.PolycyclicRecognition.exists_increment_volume_of_separated_tuples line 35

Source documentation

The lower-volume part of tuple-lift-volume, with the individual lifts and their thickening retained for the subsequent box estimates.

theorem exists_increment_volume_of_separated_tuples
    (φ : D →* MulAut N) (ι : N →* G) (κ : D →* G)
    (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (μ : Measure N) (ν : Measure D) [SigmaFinite μ] [SigmaFinite ν]
    [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
    (hφ : ∀ d, MeasurePreserving (φ d) μ μ) (hφc : ∀ d, Continuous (φ d))
    (h : ℕ) (s : Finset (Fin h → G))
    (p : (Fin h → G) → (Fin h → N) × (Fin h → D))
    (U : Set ((Fin h → N) × (Fin h → D))) (hU : IsCompact U)
    {ρ : ℝ}
    (hp : ∀ x ∈ s, ∀ i, ι ((p x).1 i) * κ ((p x).2 i) = x i)
    (hsmall : ∀ z ∈ U, dist (1 : Fin h → G) (fun i => ι (z.1 i) * κ (z.2 i)) < ρ / 2)
…