BoundaryLeaf.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

From ray bounds to a leafwise height bound

On each generator orbit the boundary argument controls all ray characters except one. The positive relation recovers that character, uniformly over the finite ray set. A bounded product of generator orbits then controls the whole nilpotent leaf. These are the two algebraic steps in the leaf-height lemma.

theorem OAI.PolycyclicRecognition.separates_after_deleting_one line 24

Source documentation

Deleting one character from a positive balanced separating family still leaves a separating family.

theorem separates_after_deleting_one
    (α : I → Module.Dual ℝ W) (c : I → ℝ) (hc : ∀ i, 0 < c i)
    (hrel : ∀ w, ∑ i, c i * α i w = 0)
    (hsep : ∀ w, (∀ i, α i w = 0) → w = 0)
    (i₀ : I) (w : W) (hw : ∀ i, i ≠ i₀ → α i w = 0) : w = 0 := by
…

theorem OAI.PolycyclicRecognition.exists_bound_of_all_but_one_form line 43

Source documentation

The bound can be chosen uniformly in the omitted ray.

theorem exists_bound_of_all_but_one_form
    (α : I → Module.Dual ℝ W) (c : I → ℝ) (hc : ∀ i, 0 < c i)
    (hrel : ∀ w, ∑ i, c i * α i w = 0)
    (hsep : ∀ w, (∀ i, α i w = 0) → w = 0) :
    ∃ C : ℝ, 0 < C ∧ ∀ (i₀ : I) (w : W) (B : ℝ), 0 ≤ B →
      (∀ i, i ≠ i₀ → |α i w| ≤ B) → ‖w‖ ≤ C * B := by
…

theorem OAI.PolycyclicRecognition.norm_increment_list_prod line 68

Source documentation

Uniform control for elementary right increments adds along a word.

theorem norm_increment_list_prod {G : Type*} [Group G]
    (f : G → W) (S : Set G) {B : ℝ}
    (hstep : ∀ g ∈ S, ∀ x, ‖f (x * g) - f x‖ ≤ B)
    (l : List G) (hl : ∀ g ∈ l, g ∈ S) (x : G) :
    ‖f (x * l.prod) - f x‖ ≤ (l.length : ℝ) * B := by
…

theorem OAI.PolycyclicRecognition.norm_increment_of_bounded_word_width line 89

Source documentation

A uniform bound on word length in generator orbits makes the entire leaf height variation uniformly bounded. Parameters inside each orbit are unrestricted.

theorem norm_increment_of_bounded_word_width {G : Type*} [Group G]
    (f : G → W) (S : Set G) (N : Subgroup G) (M : ℕ) {B : ℝ} (hB : 0 ≤ B)
    (hstep : ∀ g ∈ S, ∀ x, ‖f (x * g) - f x‖ ≤ B)
    (hwidth : ∀ n : N, ∃ l : List G,
      l.length ≤ M ∧ l.prod = n ∧ ∀ g ∈ l, g ∈ S) :
    ∀ (x : G) (n : N), ‖f (x * n) - f x‖ ≤ (M : ℝ) * B := by
…