SequenceCartanProfilePacking.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Packing comparison for successful good sheets along profile sequences

theorem OAI.PolycyclicRecognition.CartanWordModel.templateSupport_le_of_good_profile_paths_sequence line 38

Source documentation

The good-sheet leg estimates and short root switches supply the full controlled-path premise of the Cartan volume comparison.

theorem templateSupport_le_of_good_profile_paths_sequence
    (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (source E : Set W) (hE : IsCompact E) (hne : E.Nonempty) (w₀ : W)
    (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW source) β.val)
    (C : ℕ → Set (Fin (finrank ℝ (cartanRootIdeal H)) → ℝ))
    (hC : ∀ r, IsCompact (C r))
    (hvol : HasSubexponentialLowerBoundSeq scale (fun r => (volume (C r)).toReal))
    (x : ℕ → G) (d₀ : ℕ → F.D.carrier) (n₀ : ℕ → F.N.carrier)
    (A : ℕ → Set F.N.carrier) (hn₀ : ∀ r, n₀ r ∈ A r)
…

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