MatrixPacking.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Packing matrix regions in a left invariant group metric

A local metric bound near the identity converts separation into separation of matrix coordinates. Polynomial bounds on matrices and their inverses therefore produce polynomially many integer grid labels. The local metric bound remains explicit so it can be supplied by the actual Lie-group chart.

theorem OAI.PolycyclicRecognition.matrix_entry_norm_le line 24
theorem OAI.PolycyclicRecognition.matrix_norm_le_of_entries line 32

theorem OAI.PolycyclicRecognition.exists_local_matrix_metric_bound line 51

Source documentation

The local metric bound follows from a genuine matrix embedding.

theorem exists_local_matrix_metric_bound
    (ρ : G →* (Matrix (Fin n) (Fin n) ℝ)ˣ)
    (hρ : Topology.IsInducing (fun g => (ρ g : Matrix (Fin n) (Fin n) ℝ))) :
    ∃ ε : ℝ, 0 < ε ∧ ∀ g,
      ‖(ρ g : Matrix (Fin n) (Fin n) ℝ) - 1‖ ≤ ε → dist 1 g ≤ 1 := by
…

theorem OAI.PolycyclicRecognition.exists_bounded_step_matrices line 70

Source documentation

Properness and continuity bound all step matrices of a fixed metric size.

theorem exists_bounded_step_matrices [ProperSpace G]
    (ρ : G →* (Matrix (Fin n) (Fin n) ℝ)ˣ)
    (hρ : Continuous (fun g => (ρ g : Matrix (Fin n) (Fin n) ℝ))) (L : ℝ) :
    ∃ M : ℝ, 0 ≤ M ∧ ∀ g, dist 1 g ≤ L → ‖(ρ g : Matrix (Fin n) (Fin n) ℝ)‖ ≤ M := by
…

theorem OAI.PolycyclicRecognition.exists_separated_matrix_entry line 81

Source documentation

Metric separation forces one matrix coordinate difference at the scale predicted by the inverse-matrix bound.

theorem exists_separated_matrix_entry
    (ρ : G →* (Matrix (Fin n) (Fin n) ℝ)ˣ) {ε Q : ℝ} (hε : 0 < ε) (hQ : 0 < Q)
    (hlocal : ∀ g, ‖(ρ g : Matrix (Fin n) (Fin n) ℝ) - 1‖ ≤ ε → dist 1 g ≤ 1)
    (x y : G) (hxy : 1 < dist x y)
    (hinv : ‖(↑(ρ x)⁻¹ : Matrix (Fin n) (Fin n) ℝ)‖ ≤ Q) :
    ∃ i j, ε / (Q * ((n : ℝ) + 1)) ≤
      |(ρ x : Matrix (Fin n) (Fin n) ℝ) i j - (ρ y : Matrix (Fin n) (Fin n) ℝ) i j| := by
…

theorem OAI.PolycyclicRecognition.matrix_packing_bound line 117

Source documentation

An explicit finite packing bound for regions with controlled matrices and inverses. No volume or measurability of the endpoint set is assumed.

theorem matrix_packing_bound (ρ : G →* (Matrix (Fin n) (Fin n) ℝ)ˣ)
    {ε P Q : ℝ} (hε : 0 < ε) (hQ : 0 < Q)
    (hlocal : ∀ g, ‖(ρ g : Matrix (Fin n) (Fin n) ℝ) - 1‖ ≤ ε → dist 1 g ≤ 1)
    (s : Finset G)
    (hmat : ∀ g ∈ s, ‖(ρ g : Matrix (Fin n) (Fin n) ℝ)‖ ≤ P)
    (hinv : ∀ g ∈ s, ‖(↑(ρ g)⁻¹ : Matrix (Fin n) (Fin n) ℝ)‖ ≤ Q)
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → 1 < dist x y) :
    s.card ≤ (2 * ⌈P / (ε / (Q * ((n : ℝ) + 1)))⌉₊ + 1) ^ (n * n) := by
…

theorem OAI.PolycyclicRecognition.exists_polynomial_matrix_packing line 139

Source documentation

Polynomial bounds for matrix coordinates and inverse coordinates give a polynomial packing bound, with a fixed degree independent of the finite set.

theorem exists_polynomial_matrix_packing
    (ρ : G →* (Matrix (Fin n) (Fin n) ℝ)ˣ) {ε A B : ℝ}
    (hε : 0 < ε) (hA : 0 < A) (hB : 0 < B) (a b : ℕ)
    (hlocal : ∀ g, ‖(ρ g : Matrix (Fin n) (Fin n) ℝ) - 1‖ ≤ ε → dist 1 g ≤ 1) :
    ∃ C d : ℕ, ∀ (t : ℕ) (s : Finset G),
      (∀ g ∈ s, ‖(ρ g : Matrix (Fin n) (Fin n) ℝ)‖ ≤ A * (1 + (t : ℝ)) ^ a) →
      (∀ g ∈ s, ‖(↑(ρ g)⁻¹ : Matrix (Fin n) (Fin n) ℝ)‖ ≤ B * (1 + (t : ℝ)) ^ b) →
      (∀ x ∈ s, ∀ y ∈ s, x ≠ y → 1 < dist x y) → s.card ≤ C * (1 + t) ^ d := by
…