CartanAccessibleComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The volume comparison for compact accessible Cartan endpoint sets

theorem OAI.PolycyclicRecognition.CartanWordModel.accessible_templateSupport_le line 41

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
    (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 : ∀ r, IsCompact (C r))
    (hvol : HasSubexponentialLowerBound (fun r => (volume (C r)).toReal))
    (x : ℝ → G) (d : ℝ → F.D.carrier) (start : ℝ → G)
    (f : ℝ → NormalizedPair G Λ) (hΛ : 0 < (Λ : ℝ))
    (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
…

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