CoordinatePacking.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite coordinate packing

Rounding coordinates embeds a separated set into a finite integer box. This provides explicit cardinal bounds for polynomially bounded matrix coordinates, without any measurability assumption on the set of path endpoints.

theorem OAI.PolycyclicRecognition.card_le_integer_grid line 19

Source documentation

Integer boxes count separated points in a bounded coordinate box.

theorem card_le_integer_grid {X I : Type*} [Fintype I]
    (s : Finset X) (f : X → I → ℝ) (N : ℕ)
    (hbox : ∀ x ∈ s, ∀ i, -(N : ℝ) ≤ f x i ∧ f x i < (N : ℝ) + 1)
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∃ i, 1 ≤ |f x i - f y i|) :
    s.card ≤ (2 * N + 1) ^ Fintype.card I := by
…

theorem OAI.PolycyclicRecognition.card_le_scaled_grid line 47

Source documentation

Scaling a coordinate box gives the corresponding fixed-separation bound.

theorem card_le_scaled_grid {X I : Type*} [Fintype I]
    (s : Finset X) (f : X → I → ℝ) {δ R : ℝ} (hδ : 0 < δ)
    (N : ℕ) (hN : R / δ ≤ N)
    (hbox : ∀ x ∈ s, ∀ i, |f x i| ≤ R)
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∃ i, δ ≤ |f x i - f y i|) :
    s.card ≤ (2 * N + 1) ^ Fintype.card I := by
…

theorem OAI.PolycyclicRecognition.card_le_polynomial_grid line 67

Source documentation

Polynomially bounded coordinate boxes contain only polynomially many points with unit coordinate separation.

theorem card_le_polynomial_grid {X I : Type*} [Fintype I]
    (s : Finset X) (f : X → I → ℝ) (A b t : ℕ)
    (hbox : ∀ x ∈ s, ∀ i, |f x i| ≤ ((A * (1 + t) ^ b : ℕ) : ℝ))
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∃ i, 1 ≤ |f x i - f y i|) :
    s.card ≤ (2 * A + 1) ^ Fintype.card I * (1 + t) ^ (b * Fintype.card I) := by
…