BoundaryGeneratorHeight.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Recovering a uniform generator height bound from the boundary traces

theorem OAI.PolycyclicRecognition.uniform_height_bound_of_ray_trace_bounds line 15

Source documentation

Positive multiples of the original ray forms can be used as trace characters. Controlling all traces off one ray controls the whole vector, uniformly over which ray is omitted and over repeated rays.

theorem uniform_height_bound_of_ray_trace_bounds
    {W I Z : Type*} [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)
    (v : Z → W) (missing : Z → I) (B : I → ℝ) (hB : ∀ i, 0 ≤ B i)
    (htrace : ∀ z i, α i ∉ positiveWeightRay (α (missing z)) → |ell i (v z)| ≤ B i) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ z, ‖v z‖ ≤ K := by
…

Mentions: OAI.PolycyclicRecognition.positiveWeightRay