RayIdealConjugation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

+# Fixed ideal displacements along a Cartan ray

The residual adjoint part costs a polynomial, which is absorbed by the strict mixed-word widths. Exact weight dilation translates the template. This gives small coordinates for the actual conjugated displacement in the template translated to contain zero, as required by Cartan paths.

theorem OAI.PolycyclicRecognition.CartanWordModel.fixed_ideal_residual_box_norm_tendsto_zero line 29

Source documentation

Polynomial residual distortion is absorbed for a fixed ideal vector.

theorem fixed_ideal_residual_box_norm_tendsto_zero
    (C : Set (H →ₗ[ℝ] ℝ)) (E : Set W) (hE : IsCompact E) (hne : E.Nonempty)
    (hpos : ∀ w : M.coneMixedWords C, 0 < M.boxCost T hunimod eW E w.val)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (β : ℕ → M.Bases)
    (hβ : ∀ n, IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) (β n).val)
    (h : H) (x : M.coneWordIdeal C) :
    Tendsto (fun n : ℕ =>
      ‖(M.boxBasis T hunimod eW E (β n) n).equivFun
        (cartanIdealResidualAutomorphism T H (-(n : ℝ) • h) x)‖)
      atTop (𝓝 0) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism

theorem OAI.PolycyclicRecognition.CartanWordModel.fixed_ideal_adjoint_shifted_box_norm_tendsto_zero line 63

Source documentation

The full adjoint action on a fixed ideal vector has vanishing coordinates in the translated template. The bases are the same actual word bases, whose maximizing property is translation invariant.

theorem fixed_ideal_adjoint_shifted_box_norm_tendsto_zero
    (C : Set (H →ₗ[ℝ] ℝ)) (E : Set W) (hE : IsCompact E) (hne : E.Nonempty)
    (hpos : ∀ w : M.coneMixedWords C, 0 < M.boxCost T hunimod eW E w.val)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (β : ℕ → M.Bases)
    (hβ : ∀ n, IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) (β n).val)
    (v₀ : W) (x : M.coneWordIdeal C) :
    Tendsto (fun n : ℕ =>
      ‖(M.boxBasis T hunimod eW ((fun v => v - v₀) '' E) (β n) n).equivFun
        (cartanIdealAdjointAutomorphism T H
          (-(n : ℝ) • cartanHeightSection T H (eW.symm v₀)) x)‖)
…