CartanShrinkingBoxEnvelope.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Absorbing vanishing homothetic enlargements into the box radius

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_homothetic_box_envelope_sequence line 23

Source documentation

The diagonal's shrinking enlargement changes only a subexponential radius in one fixed maximizing box. The enlarged basis may vary with scale.

theorem exists_homothetic_box_envelope_sequence {N : Type*}
    (Exp : cartanRootIdeal H → N)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) β.val)
    (scale δ R : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
    (hscale0 : ∀ n, 0 ≤ scale n) (hδ0 : ∀ n, 0 ≤ δ n) (hδ : Tendsto δ atTop (𝓝 0))
    (hR0 : ∀ n, 0 ≤ R n) (hR : HasSubexponentialUpperBoundSeq scale R) :
    ∃ V : ℕ → ℝ, (∀ n, 0 ≤ V n) ∧ HasSubexponentialUpperBoundSeq scale V ∧
      ∀ n (γ : M.Bases),
…

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