VolumeExponents.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Extracting exponential volume rates

A polynomial loss in the cardinality of a separated set does not change its exponential rate. This is the limiting step after applying the path packing estimate to the good endpoint set selected by stationary averaging.

theorem OAI.PolycyclicRecognition.exponent_le_of_polynomial_exp_bound line 20

Source documentation

An eventual exponential lower bound cannot exceed an exponential upper bound with a fixed polynomial prefactor.

theorem exponent_le_of_polynomial_exp_bound
    {p q c C : ℝ} (hc : 0 < c) (hC : 0 < C) (k : ℕ)
    (hbound : ∀ᶠ r : ℝ in atTop,
      c * Real.exp (r * p) ≤ C * (1 + r) ^ k * Real.exp (r * q)) :
    p ≤ q := by
…