StationaryScales.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the finite stationary remainders

These are the exact scale calculations in osc:stationary. The ratio A^2 / Λ pays for each extra stationary term. The remaining d+2 derivatives are absorbed using A ≤ R^2. No stationary-phase estimate is assumed here.

theorem OAI.Falconer.stationary_remainder_ratio line 19
theorem OAI.Falconer.stationary_weighted_remainder_factor line 26
Source documentation
Applying a direct expansion of length J-j to the inverse coefficient of order j has exactly the same remainder scale for every j.
```
theorem stationary_weighted_remainder_factor {J j : ℕ} (hj : j ≤ J)
    (d : ℕ) (A Λ : ℝ) :
    (Λ⁻¹)^j * ((Λ⁻¹)^(J-j) * A^(2*(J-j)+d+2+2*j)) =
      (Λ⁻¹)^J * A^(2*J+d+2) := by
…
```
theorem OAI.Falconer.stationary_remainder_scale line 33

theorem OAI.Falconer.exists_stationary_remainder_order line 52

Source documentation

A single finite order, independent of the large scale, achieves any prescribed negative power. This also permits fixed derivative overhead.

theorem exists_stationary_remainder_order (d : ℕ) {κ T : ℝ} (hκ : 0 < κ) :
    ∃ J : ℕ, 1 ≤ J ∧ ∀ R A Λ : ℝ,
      1 ≤ R → 0 ≤ A → 0 < Λ → A ≤ R^2 → A^2/Λ ≤ R^(-κ) →
      (Λ⁻¹)^J * A^(2*J+d+2) ≤ R^(-T) := by
…