SectionTileVolume.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The quotient trace in the per-tile volume exponent

theorem OAI.PolycyclicRecognition.subexponential_exp_error line 15
Source documentation
A vanishing error in the exponent contributes a subexponential factor.
```
theorem subexponential_exp_error {ε : ℝ → ℝ} (hε : Tendsto ε atTop (𝓝 0)) :
    HasSubexponentialUpperBound (fun r => Real.exp (ε r * r)) := by
…
```
Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBound

theorem OAI.PolycyclicRecognition.section_tile_volume_exponent line 33

Source documentation

The ideal exponent and the exact quotient multiplier combine to P - ell. Arbitrary translated quotient locations are allowed.

theorem section_tile_volume_exponent
    (E : ℝ → Set N) (T : ℝ → Set Q) (B : ℝ → Set π.ker)
    (q₀ : ℝ → Q) (α : ℝ → Q ≃ Q)
    (P ell : ℝ) (ε U V : ℝ → ℝ)
    (hε : Tendsto ε atTop (𝓝 0))
    (hU : HasSubexponentialUpperBound U) (hV : HasSubexponentialUpperBound V)
    (hU0 : ∀ r, 0 ≤ U r) (hV0 : ∀ r, 0 ≤ V r)
    (hT : ∀ r, μQ (T r) ≠ ⊤) (hB : ∀ r, μI (B r) ≠ ⊤)
    (hα : ∀ r, μQ (α r '' T r) =
      ENNReal.ofReal (Real.exp (-ell * r + ε r * r)) * μQ (T r))
    (hTB : ∀ r, (μQ (T r)).toReal ≤ U r)
    (hIB : ∀ r, (μI (B r)).toReal ≤ V r * Real.exp (P * r))
…

Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBound