ParameterChoice.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite choices of the nonlinearity power and Sobolev index

The manuscript first constructs profiles for all sufficiently small positive a, then chooses an odd integer power with a = 1 / (p - 1), and only afterward chooses the finite Sobolev index. These lemmas justify that order of choices.

theorem OAI.DefocusingNLS.exists_odd_power_with_small_reciprocal line 19
Source documentation
Every small-parameter interval contains the reciprocal of an even positive integer, yielding an odd power at least three.
```
theorem exists_odd_power_with_small_reciprocal (a₀ : ℝ) (ha₀ : 0 < a₀) :
    ∃ p : ℕ, Odd p ∧ 3 ≤ p ∧ 0 < 1 / ((p : ℝ) - 1) ∧
      1 / ((p : ℝ) - 1) < a₀ := by
…
```
theorem OAI.DefocusingNLS.exists_sobolev_index line 36
Source documentation
The high derivative index can be chosen after the profile and potential bound, without an infinite regularity requirement.
```
theorem exists_sobolev_index (a B : ℝ) :
    ∃ k : ℕ, 8 < k ∧ 6 - 2 * a + 2 * B + 1 < (k : ℝ) := by
…
```
theorem OAI.DefocusingNLS.energy_supercritical_in_twelve line 44
Source documentation
Every power considered here is energy-supercritical in dimension twelve.
```
theorem energy_supercritical_in_twelve {p : ℕ} (hp : 3 ≤ p) :
    1 < 6 - 2 / ((p : ℝ) - 1) := by
…
```