GlobalHeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Assembling the scalar boundary bounds into global height bounds

The scalar estimates are uniform over all base points. Separating boundary traces then control the full height on a transversal, and the leaf estimate extends the same bound to the whole group. The existence of the boundary maps and their shadow estimates remains the geometric obligation.

theorem OAI.PolycyclicRecognition.affine_bound_of_trace_bounds line 18

Source documentation

Finitely many uniform trace bounds give a uniform vector-valued affine bound. No choice of a basis depending on the quasi-isometry is involved.

theorem affine_bound_of_trace_bounds
    {X W I : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    [FiniteDimensional ℝ W] [Fintype I]
    (β : I → Module.Dual ℝ W)
    (hsep : ∀ w, (∀ i, β i w = 0) → w = 0)
    (π F : X → W) (A : W →ₗ[ℝ] W) (v : W)
    {B : ℝ} (hB : 0 ≤ B)
    (htrace : ∀ x i, |β i (F x - (v + A (π x)))| ≤ B) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ x, ‖F x - (v + A (π x))‖ ≤ C := by
…

theorem OAI.PolycyclicRecognition.global_affine_bound_of_leaf_transversal line 32

Source documentation

The bounded leaf and transversal estimates combine using G = N D. The decomposition need not be unique, and its factors need not commute.

theorem global_affine_bound_of_leaf_transversal
    {G W : Type*} [Group G] [NormedAddCommGroup W] [NormedSpace ℝ W]
    (π F : G → W) (A : W →ₗ[ℝ] W) (v : W) (N D : Set G)
    (hdecomp : ∀ g, ∃ n ∈ N, ∃ d ∈ D, g = n * d)
    (hheight : ∀ n ∈ N, ∀ d ∈ D, π (n * d) = π d)
    {B C : ℝ}
    (hleaf : ∀ n ∈ N, ∀ d ∈ D, ‖F (n * d) - F d‖ ≤ B)
    (htrans : ∀ d ∈ D, ‖F d - (v + A (π d))‖ ≤ C) :
    ∀ g, ‖F g - (v + A (π g))‖ ≤ B + C := by
…

theorem OAI.PolycyclicRecognition.affine_trace_bound_of_identified_coefficient line 51

Source documentation

Once the sublinear comparison identifies a trace coefficient, its bounded scalar error has exactly the affine form required for vector assembly.

theorem affine_trace_bound_of_identified_coefficient
    {X W : Type*} [AddCommGroup W] [Module ℝ W]
    (π F : X → W) (α β : Module.Dual ℝ W) (A : W →ₗ[ℝ] W) (x₀ : X)
    (hπ₀ : π x₀ = 0) (hid : α = β.comp A) {B : ℝ}
    (hbound : ∀ x, |(β (F x) - β (F x₀)) - (α (π x) - α (π x₀))| ≤ B) :
    ∀ x, |β (F x - (F x₀ + A (π x)))| ≤ B := by
…