OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborRowReverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.exists_reverse line 49

   Source documentation

   The opposite trace inequality uses an actual row with the same root and the two labels and offsets swapped. Only its subexponential radius changes.

   theorem AffineNeighborRow.exists_reverse
       (hExp : IsGroupExponential ExpG)
       (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
       (hcell : IsCompact cell) (hne : cell.Nonempty)
       (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
         (M.boxCost T hunimod eW cell) βcell.val)
       (hδ : 0 ≤ δ) (hs : ∀ n, 0 ≤ D.scale n) :
       ∃ R : AffineNeighborRow T M F hunimod eW π b₀ cell βcell X βD
         haarN chartN hchartN pivot shrink B δ S (Λ := Λ),
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow