BoundaryGeneratorActionBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Height control from the quotient actions invisible to each generator

theorem OAI.PolycyclicRecognition.generator_height_bound_of_boundary_actions line 15

Source documentation

The compact-volume comparison controls all ray traces except the ray containing the generator. The positive balanced relation recovers the full height increment with a common constant.

theorem generator_height_bound_of_boundary_actions
    {P G W I J : Type*} [Group G]
    [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W] [Fintype I]
    (α ell : I → W →ₗ[ℝ] ℝ) (c rate : I → ℝ)
    (hc : ∀ i, 0 < c i) (hrate : ∀ i, 0 < rate i)
    (hrel : ∀ w, ∑ i, c i * α i w = 0)
    (hsep : ∀ w, (∀ i, α i w = 0) → w = 0)
    (hell : ∀ i, ell i = rate i • α i)
    (S : I → Type*) (act : ∀ i, G →* Equiv.Perm (S i)) (U : ∀ i, Set (S i))
    (η : P → G → W) (gen : J → ℝ → G) (missing : J → I)
    (B : I → ℝ) (hB : ∀ i, 0 ≤ B i)
    (htrace : ∀ i p x y, act i x '' U i = act i y '' U i →
…