CartanBoxScaling.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Homothetic templates and the interior gain for Cartan actions

theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_image_smul line 18

Source documentation

Positive homotheties scale each letter support exactly.

theorem weightSupport_image_smul
    {W I B : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    [FiniteDimensional ℝ W] [Fintype I] [Fintype B]
    (D : SupportDatum W I B) {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    {t : ℝ} (ht : 0 ≤ t) (i : I) :
    D.weightSupport ((fun x => t • x) '' E) i = t * D.weightSupport E i := by
…

Mentions: OAI.PolycyclicRecognition.SupportDatum

theorem OAI.PolycyclicRecognition.CartanWordModel.boxCost_image_smul line 47

Source documentation

Homothety scales every actual word cost, including zero-weight words.

theorem boxCost_image_smul {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    {t : ℝ} (ht : 0 ≤ t) (w : M.wordList) :
    M.boxCost T hunimod eW ((fun x => t • x) '' E) w =
      t * M.boxCost T hunimod eW E w := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.maximizing_box_basis_smul line 58

Source documentation

A maximizing basis is unchanged by a nonnegative homothety.

theorem maximizing_box_basis_smul
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty) {t : ℝ} (ht : 0 ≤ t)
    (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) β.val) :
    IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW ((fun x => t • x) '' E)) β.val := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.norm_boxBasis_interior_le line 74

Source documentation

Coordinates in a smaller homothetic box gain a definite exponential factor when measured in the original box.

theorem norm_boxBasis_interior_le
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty) {t : ℝ}
    (ht : 0 ≤ t) (ht1 : t ≤ 1) (β : M.Bases) {r lo : ℝ} (hr : 0 ≤ r)
    (hlo : ∀ w : M.wordList, lo ≤ M.boxCost T hunimod eW E w)
    (v : cartanRootIdeal H) :
    ‖(M.boxBasis T hunimod eW E β r).equivFun v‖ ≤
      Real.exp (r * ((t - 1) * lo)) *
        ‖(M.boxBasis T hunimod eW ((fun x => t • x) '' E) β r).equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_interior_adjoint_bound line 90

Source documentation

The actual Cartan action has the interior exponential gain, up to the already proved polynomial residual action.

theorem exists_interior_adjoint_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ (A : ℝ) (p : ℕ), 0 ≤ A ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
      ∀ {t : ℝ}, 0 ≤ t → t ≤ 1 → ∀ (β : M.Bases),
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ (γ : M.Bases) (r lo : ℝ), 0 ≤ r →
      (∀ w : M.wordList, lo ≤ M.boxCost T hunimod eW E w) →
      ∀ (h : H) (w : W), w ∈ (fun x => t • x) '' E →
      eW (heightProjection T.character (h : L)) = r • w → ∀ v : cartanRootIdeal H,
      ‖(M.boxBasis T hunimod eW E β r).equivFun
        (cartanIdealAdjointAutomorphism T H h v)‖ ≤
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism