OAI/GroupTheory/PolycyclicRecognition/Analysis/SequencePathPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exponent_le_of_sequence_image_paths line 21

   Source documentation

   Successful endpoint sets may lose subexponential mass. Center every image path at its actual start before applying the ambient packing theorem.

   theorem exponent_le_of_sequence_image_paths
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (π : G →* Multiplicative W) (E : Set W) (P : Set W → ℝ)
       {p K C D : ℝ} {Q : ℝ≥0∞} {mass : ℕ → ℝ}
       (hmass : HasSubexponentialLowerBoundSeq scale mass) (hΛ : 0 < (Λ : ℝ))
       (hK : 0 ≤ K) (hC : 0 ≤ C) (hQ : Q < ⊤) (hD : 0 < D) (k : ℕ)
       (hlower : ∀ η : ℝ, 0 < η → ∀ᶠ n in atTop,
         ∃ (f : NormalizedPair G Λ) (a : G) (s : Finset G),
           (∀ x ∈ s, ∀ y ∈ s, x ≠ y → (Λ : ℝ) * ((Λ : ℝ) + 1) < dist x y) ∧
           ENNReal.ofReal (mass n) * ENNReal.ofReal (Real.exp (scale n * p)) ≤
             (s.card : ℝ≥0∞) * Q ∧
           ∀ g ∈ s, ∃ γ : Path a g,
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq, OAI.PolycyclicRecognition.NormalizedPair