FactorProductPacking.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Packing through a possibly noninjective factor map

Left translations on a semidirect product act separately on its two factor coordinates. Their product measure is preserved when the action preserves the first factor's measure. Disjointness is tested after projection to the ambient metric group, so no injectivity of that projection is required.

def OAI.PolycyclicRecognition.factorTranslate line 26
Source documentation
Semidirect left translation, written on the product of the factors.
```
def factorTranslate (φ : D →* MulAut N) (p z : N × D) : N × D :=
…
```
def OAI.PolycyclicRecognition.factorTranslationEquiv line 30
Source documentation
Measurable automorphisms give measurable product-coordinate translations.
```
def factorTranslationEquiv (φ : D →* MulAut N)
    (hφ : ∀ d, Measurable (φ d)) (p : N × D) : (N × D) ≃ᵐ (N × D) :=
…
```
theorem OAI.PolycyclicRecognition.factorTranslationEquiv_apply line 44

theorem OAI.PolycyclicRecognition.factorTranslate_measure line 49

Source documentation

Product Haar mass is unchanged by these translations.

theorem factorTranslate_measure (φ : D →* MulAut N)
    (μ : Measure N) (ν : Measure D) [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
    [SFinite μ] [SFinite ν] (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
    (p : N × D) (U : Set (N × D)) :
    (μ.prod ν) (factorTranslate φ p '' U) = (μ.prod ν) U := by
…

Mentions: OAI.PolycyclicRecognition.factorTranslate

theorem OAI.PolycyclicRecognition.factorTranslate_projection line 65

Source documentation

The product-coordinate map intertwines translations and ambient multiplication.

theorem factorTranslate_projection (φ : D →* MulAut N)
    (ι : N →* G) (κ : D →* G)
    (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹) (p z : N × D) :
    ι (factorTranslate φ p z).1 * κ (factorTranslate φ p z).2 =
      (ι p.1 * κ p.2) * (ι z.1 * κ z.2) := by
…

Mentions: OAI.PolycyclicRecognition.factorTranslate

theorem OAI.PolycyclicRecognition.factor_separated_card_mul_le line 78

Source documentation

Every finite separated family of ambient projections gives disjoint translated cells in the product of the factors, even if the factor map has nontrivial fibers.

theorem factor_separated_card_mul_le (φ : D →* MulAut N)
    (ι : N →* G) (κ : D →* G)
    (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (μ : Measure N) (ν : Measure D) [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
    [SFinite μ] [SFinite ν] (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
    (s : Finset G) (p : G → N × D) (U region : Set (N × D))
    (hU : MeasurableSet U) {ρ : ℝ}
    (hp : ∀ x ∈ s, ι (p x).1 * κ (p x).2 = x)
    (hsmall : ∀ z ∈ U, dist (1 : G) (ι z.1 * κ z.2) < ρ / 2)
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ρ ≤ dist x y)
    (hthick : ∀ x ∈ s, factorTranslate φ (p x) '' U ⊆ region) :
    (s.card : ℝ≥0∞) * (μ.prod ν) U ≤ (μ.prod ν) region := by
…

Mentions: OAI.PolycyclicRecognition.factorTranslate