CartanRayTrace.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual boundary trace is a positive multiple of its generator ray

theorem OAI.PolycyclicRecognition.CartanWordModel.ray_height_trace_pos_multiple line 22

Source documentation

The positive pure-word multiplicities in a ray quotient identify its Haar trace with a strictly positive multiple of the chosen height ray.

theorem ray_height_trace_pos_multiple
    (j : Fin M.letterCount) (c : Fin M.letterCount → ℕ)
    (hout : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ positiveWeightRay
      (M.weight j : H →ₗ[ℝ] ℝ) → c i = 0)
    (hcj : 0 < c j) :
    ∃ r : ℝ, 0 < r ∧
      (∑ i, (c i : ℝ) • cartanHeightWeight T H (M.weight i)).comp eW.symm.toLinearMap =
        r • (cartanHeightWeight T H (M.weight j)).comp eW.symm.toLinearMap := by
…

Mentions: OAI.PolycyclicRecognition.positiveWeightRay, OAI.PolycyclicRecognition.cartanHeightWeight