ConeOffsetExponent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Cancellation of the three exponential counts in the offset argument

theorem OAI.PolycyclicRecognition.card_le_real_tile_bound line 15
Source documentation
Assigning finitely many endpoints to tiles multiplies the tile count by the uniform per-tile bound; an assignment need not be injective.
```
theorem card_le_real_tile_bound {n m : ℕ} (tile : Fin n → Fin m) {B : ℝ}
    (hB : ∀ j : Fin m, ((Finset.univ.filter fun i => tile i = j).card : ℝ) ≤ B) :
    (n : ℝ) ≤ (m : ℝ) * B := by
…
```

theorem OAI.PolycyclicRecognition.cone_offset_exponent_nonpos line 30

Source documentation

Source exponent P₁, tiling exponent P₁-P₂, and tile-image exponent P₂-ℓ force ℓ≤0. Every subexponential loss is retained explicitly.

theorem cone_offset_exponent_nonpos
    (scale : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (points tiles : ℕ → ℕ) (assign : ∀ k, Fin (points k) → Fin (tiles k))
    (lower tileLoss pointLoss : ℕ → ℝ)
    (hlower : HasSubexponentialLowerBoundSeq scale lower)
    (htile : HasSubexponentialUpperBoundSeq scale tileLoss)
    (hpoint : HasSubexponentialUpperBoundSeq scale pointLoss)
    (htile0 : ∀ᶠ k in atTop, 0 ≤ tileLoss k)
    (hpoint0 : ∀ᶠ k in atTop, 0 ≤ pointLoss k)
    {P₁ P₂ ℓ : ℝ}
    (hsource : ∀ᶠ k in atTop, lower k * Real.exp (scale k * P₁) ≤ points k)
    (htiles : ∀ᶠ k in atTop,
…

Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq