OAI/GroupTheory/PolycyclicRecognition/Geometry/SequenceCartanAccessible.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.accessible_templateSupport_le_sequence line 42

   Source documentation

   A compact successful logarithmic image of subexponential volume cannot have a larger source support exponent than its image-path height template.

   theorem accessible_templateSupport_le_sequence
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (source target : Set W) (htarget : IsCompact target) (hne : target.Nonempty)
       (β : M.Bases)
       (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
         (M.boxCost T hunimod eW source) β.val)
       (C : ℕ → Set (Fin (finrank ℝ (cartanRootIdeal H)) → ℝ))
       (hC : ∀ n, IsCompact (C n))
       (hvol : HasSubexponentialLowerBoundSeq scale (fun n => (volume (C n)).toReal))
       (x : ℕ → G) (d : ℕ → F.D.carrier) (start : ℕ → G)
       (f : ℕ → NormalizedPair G Λ) (hΛ : 0 < (Λ : ℝ))
   …

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