SubexponentialVolumeComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Comparing exponential rates after subexponential losses

theorem OAI.PolycyclicRecognition.exponent_le_of_subexponential_exp_bound line 15
Source documentation
The measurable-image loss disappears in the eventual packing comparison.
```
theorem exponent_le_of_subexponential_exp_bound {p q : ℝ} {f g : ℝ → ℝ}
    (hf : HasSubexponentialLowerBound f) (hg : HasSubexponentialUpperBound g)
    (hbound : ∀ᶠ r in atTop, f r * Real.exp (r * p) ≤ g r * Real.exp (r * q)) :
    p ≤ q := by
…
```
Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound, OAI.PolycyclicRecognition.HasSubexponentialUpperBound
theorem OAI.PolycyclicRecognition.exponent_le_of_subexponential_polynomial_bound line 38
Source documentation
A fixed polynomial packing prefactor also absorbs the subexponential loss of the successful endpoint set.
```
theorem exponent_le_of_subexponential_polynomial_bound {p q D : ℝ}
    {f : ℝ → ℝ} (hf : HasSubexponentialLowerBound f) (hD : 0 < D) (k : ℕ)
    (hbound : ∀ᶠ r in atTop,
      f r * Real.exp (r * p) ≤ D * (1 + r) ^ k * Real.exp (r * q)) : p ≤ q := by
…
```
Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound

theorem OAI.PolycyclicRecognition.exponent_le_of_subexponential_separated_counts line 56

Source documentation

The separated endpoint count may lose subexponential mass, as in the successful-parameter image estimate.

theorem exponent_le_of_subexponential_separated_counts {p q D : ℝ}
    {f : ℝ → ℝ} (hf : HasSubexponentialLowerBound f) (hD : 0 < D)
    {Q : ℝ≥0∞} (hQ : Q < ⊤) (k : ℕ)
    (hcount : ∀ᶠ r in atTop, ∃ N : ℕ,
      ENNReal.ofReal (f r) * ENNReal.ofReal (Real.exp (r * p)) ≤ (N : ℝ≥0∞) * Q ∧
      (N : ℝ) ≤ D * (1 + r) ^ k * Real.exp (r * q)) : p ≤ q := by
…

Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound