ShortTimeParameters.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The source cutoff beats the enlarged width and every fixed polynomial.

theorem OAI.LipschitzHilbert.eventually_short_time_decay line 18
Source documentation
The two exponents are exactly the manuscript's 0.9 and 0.97. This is the numerical small-time input to compact-witness transfer.
```
theorem eventually_short_time_decay (p : ℝ) {C : ℝ} (hC : 0 < C) :
    ∀ᶠ L : ℝ in atTop,
      2 * C * L ^ p * Real.exp (L ^ (9 / 10 : ℝ) - L ^ (97 / 100 : ℝ)) ≤ 1 / 2 := by
…
```

theorem OAI.LipschitzHilbert.eventually_transfer_small_time line 54

Source documentation

The actual source inequalities m≤2 exp(L^0.9) and tau≤exp(-L^0.97) imply the exact transfer hypothesis uniformly over all top lengths below tau.

theorem eventually_transfer_small_time (p : ℝ) (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ m tau ell : ℝ,
      0 ≤ m → m ≤ 2 * Real.exp (L ^ (9 / 10 : ℝ)) →
      0 ≤ tau → tau ≤ Real.exp (-(L ^ (97 / 100 : ℝ))) →
      0 ≤ ell → ell ≤ tau → C * L ^ p * m * ell ≤ 1 / 2 := by
…