CoarsePackingAsymptotics.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial losses and logarithmic errors in path packing

theorem OAI.PolycyclicRecognition.eventually_logarithmic_error_le line 15
Source documentation
Every fixed affine function of the logarithmic path error is sublinear.
```
theorem eventually_logarithmic_error_le (a b : ℝ) {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ r : ℝ in atTop, a * (1 + Real.log (2 + r)) + b ≤ ε * r := by
…
```

theorem OAI.PolycyclicRecognition.coarse_path_word_prefactor_le line 41

Source documentation

The path-word subdivision prefactor is bounded by one fixed quadratic.

theorem coarse_path_word_prefactor_le {A r : ℝ} (hA : 0 ≤ A) (hr : 1 ≤ r) :
    3 + (A * r + 1) * (A * (1 + Real.log (2 + r)) + 2) ≤
      (3 + (A + 1) * (3 * A + 2)) * (1 + r) ^ 2 := by
…

theorem OAI.PolycyclicRecognition.exponent_le_of_separated_card_bounds line 63

Source documentation

Positive exponential lower mass and a polynomial exponential upper cardinality force the comparison of their exponents.

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

theorem OAI.PolycyclicRecognition.exponent_le_of_separated_mass_bounds line 83

Source documentation

The same comparison with a positive finite lower mass coefficient.

theorem exponent_le_of_separated_mass_bounds {p q D : ℝ}
    {a Q : ℝ≥0∞} (ha : 0 < a) (hafin : a < ⊤) (hD : 0 < D) (hQ : Q < ⊤) (k : ℕ)
    (h : ∀ᶠ r : ℝ in atTop, ∃ N : ℕ,
      a * ENNReal.ofReal (Real.exp (r * p)) ≤ (N : ℝ≥0∞) * Q ∧
      (N : ℝ) ≤ D * (1 + r) ^ k * Real.exp (r * q)) : p ≤ q := by
…