HomogeneousSpectralLocalizationSubunit.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-order bounds for the polynomial nonlinearity on strictly subunit balls. Complexifying the two real variables permits Cauchy estimates with constants independent of the power.

def OAI.DefocusingNLS.homogeneousSubunitPolynomial line 17
theorem OAI.DefocusingNLS.homogeneousSubunitPolynomial_contDiff line 20
theorem OAI.DefocusingNLS.homogeneousSubunitPolynomial_norm line 24

theorem OAI.DefocusingNLS.homogeneousSubunitPolynomial_derivatives line 36

Source documentation

The gap between the two radii absorbs every fixed derivative order.

theorem homogeneousSubunitPolynomial_derivatives (k : ℕ) (ρ σ : ℝ)
    (hρ : 0 ≤ ρ) (hρσ : ρ < σ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ n : ℕ, ∀ x : ℂ × ℂ, ‖x‖ ≤ ρ →
      ‖iteratedFDeriv ℂ k (homogeneousSubunitPolynomial n) x‖ ≤
        C * σ ^ (2 * n + 1) := by
…

Mentions: OAI.DefocusingNLS.homogeneousSubunitPolynomial

theorem OAI.DefocusingNLS.homogeneousSubunitPolynomial_derivatives_small line 87

Source documentation

All fixed-order complexified jets tend uniformly to zero on a subunit ball.

theorem homogeneousSubunitPolynomial_derivatives_small (k : ℕ) (ρ : ℝ)
    (hρ : 0 ≤ ρ) (hρ1 : ρ < 1) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n : ℕ in atTop, ∀ x : ℂ × ℂ, ‖x‖ ≤ ρ →
      ‖iteratedFDeriv ℂ k (homogeneousSubunitPolynomial n) x‖ < ε := by
…

Mentions: OAI.DefocusingNLS.homogeneousSubunitPolynomial

theorem OAI.DefocusingNLS.homogeneousSubunitPolynomial_diagonal line 108
def OAI.DefocusingNLS.homogeneousSubunitDiagonal line 111
theorem OAI.DefocusingNLS.homogeneousSubunitPolynomial_real_norm line 116
theorem OAI.DefocusingNLS.homogeneousSubunitPolynomial_oddPower_bound line 126
theorem OAI.DefocusingNLS.homogeneous_oddPower_derivatives_subunit line 139
Source documentation
Uniform decay holds for the actual real odd-power derivatives, including the real-linear derivative used in the spectral potential.
```
theorem homogeneous_oddPower_derivatives_subunit (k : ℕ) (ρ : ℝ)
    (hρ : 0 ≤ ρ) (hρ1 : ρ < 1) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n : ℕ in atTop, ∀ z : ℂ, ‖z‖ ≤ ρ →
      ‖iteratedFDeriv ℝ k (oddPowerNonlinearity n) z‖ < ε := by
…
```
Mentions: OAI.DefocusingNLS.oddPowerNonlinearity