OAI/GroupTheory/PolycyclicRecognition/Analysis/SubexponentialPathPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exponent_le_of_subexponential_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_subexponential_image_paths
       (π : G →* Multiplicative W) (E : Set W) (P : Set W → ℝ)
       {p K C D : ℝ} {Q : ℝ≥0∞} {mass : ℝ → ℝ}
       (hmass : HasSubexponentialLowerBound mass) (hΛ : 0 < (Λ : ℝ))
       (hK : 0 ≤ K) (hC : 0 ≤ C) (hQ : Q < ⊤) (hD : 0 < D) (k : ℕ)
       (hlower : ∀ η : ℝ, 0 < η → ∀ᶠ r in atTop,
         ∃ (f : NormalizedPair G Λ) (a : G) (s : Finset G),
           (∀ x ∈ s, ∀ y ∈ s, x ≠ y → (Λ : ℝ) * ((Λ : ℝ) + 1) < dist x y) ∧
           ENNReal.ofReal (mass r) * ENNReal.ofReal (Real.exp (r * p)) ≤
             (s.card : ℝ≥0∞) * Q ∧
           ∀ g ∈ s, ∃ γ : Path a g,
             PathMetricBound γ (C * r) (C * (1 + Real.log (2 + r))) ∧
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound, OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.PathMetricBound