ConeIdealTiling.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite tilings of actual ideal boxes with exact volume bounds

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coneIdeal_tiling_radius line 28

Source documentation

Uniformly bounded-radius enlarged boxes suffice for the maximal-packing construction, even after a Haar-preserving automorphism of the small box. The hypothesis on its image is the strict-width inclusion proved separately.

theorem exists_coneIdeal_tiling_radius (dynkin : NilpotentDynkinExpansionInput E G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C)) :
    ∃ R : ℝ, 0 < R ∧ ∀ (s₁ s₂ : Fin M.letterCount → ℝ) (β : M.ConeIdealBases C),
      M.IsMaximizingConeIdealBasis C b₀ s₁ β →
      M.IsMaximizingConeIdealBasis C b₀ s₂ β → ∀ r : ℝ, 0 ≤ r →
      ∀ (μ : Measure G), μ.IsHaarMeasure →
      ∀ F : G ≃ₜ* G, MeasurePreserving F μ μ →
      F '' M.coneIdealBox C (Exp ∘ e) s₂ β r 1 ⊆
        M.coneIdealBox C (Exp ∘ e) s₁ β r 1 →
      μ (M.coneIdealBox C (Exp ∘ e) s₂ β r 1) ≠ 0 →
      ∃ (n : ℕ) (anchor : Fin n → G) (tile : Fin n → Set G),
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput