TriangularChainPacking.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial path packing for a concrete triangular representation

A proper left invariant metric compatible with an actual positive triangular matrix embedding has polynomial packing for paths of bounded logarithmic height. All coordinate and inverse estimates are proved here. No polynomial packing hypothesis is imposed on this representation.

theorem OAI.PolycyclicRecognition.chain_matrix_bound line 26

Source documentation

Every bounded-height chain has a polynomially bounded endpoint matrix.

theorem chain_matrix_bound (ρ : G →* positiveTriangular n)
    (x : G) (L H V : ℝ) (hV : 0 ≤ V)
    (hstep : ∀ a, dist 1 a ≤ L → ‖matrix (ρ a)‖ ≤ V) :
    ∃ A : ℝ, 0 < A ∧ ∀ (t m : ℕ), m ≤ t → ∀ y,
      BoundedHeightChain (fun g => (height (ρ g)).toAdd) L H m x y →
      ‖matrix (ρ y)‖ ≤ A * (1 + (t : ℝ)) ^ n := by
…

Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.BoundedHeightChain

theorem OAI.PolycyclicRecognition.chain_inverse_matrix_bound line 69

Source documentation

The same region has a polynomial inverse-matrix bound.

theorem chain_inverse_matrix_bound (ρ : G →* positiveTriangular n)
    (x : G) (L H : ℝ) {A : ℝ} (hA : 0 < A)
    (hmat : ∀ (t m : ℕ), m ≤ t → ∀ y,
      BoundedHeightChain (fun g => (height (ρ g)).toAdd) L H m x y →
      ‖matrix (ρ y)‖ ≤ A * (1 + (t : ℝ)) ^ n) :
    ∃ B : ℝ, 0 < B ∧ ∀ (t m : ℕ), m ≤ t → ∀ y,
      BoundedHeightChain (fun g => (height (ρ g)).toAdd) L H m x y →
      ‖matrix ((ρ y)⁻¹)‖ ≤ B * (1 + (t : ℝ)) ^ (n * n) := by
…

Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.BoundedHeightChain

theorem OAI.PolycyclicRecognition.polynomialBoundedChainPacking_of_triangular_representation line 101
Source documentation
A proper group with an actual positive triangular matrix embedding has polynomial packing of bounded-logarithmic-height chains. This theorem proves the packing property from the representation and topology.
```
theorem polynomialBoundedChainPacking_of_triangular_representation
    [ProperSpace G] [DecidableEq G]
    (ρ : G →* positiveTriangular n)
    (hρ : Topology.IsInducing (fun g => matrix (ρ g))) :
    PolynomialBoundedChainPacking (fun g => (height (ρ g)).toAdd) := by
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.PolynomialBoundedChainPacking
theorem OAI.PolycyclicRecognition.polynomialBoundedChainPacking_of_factored_triangular_representation line 134
Source documentation
If the diagonal characters of the representation factor through canonical height, the same polynomial packing theorem applies to canonical-height chains. Only this concrete factorization is needed from the representation.
```
theorem polynomialBoundedChainPacking_of_factored_triangular_representation
    [ProperSpace G] [DecidableEq G]
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (π : G → W) (ρ : G →* positiveTriangular n)
    (hρ : Topology.IsInducing (fun g => matrix (ρ g)))
    (T : W →L[ℝ] (Fin n → ℝ))
    (hheight : ∀ g, (height (ρ g)).toAdd = T (π g)) : PolynomialBoundedChainPacking π := by
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.PolynomialBoundedChainPacking