OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousDerivativeBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.homogeneous_linear_two_jet_bound line 13
2. theorem OAI.DefocusingNLS.homogeneous_bilinear_two_jet_bound line 34
3. theorem OAI.DefocusingNLS.exists_homogeneousOddPower_two_jet_bound line 66

   Source documentation

   All derivatives of order at most two are uniformly bounded on a homogeneous-space ball. The proof uses the polynomial's actual bounded bilinear operations.

   theorem exists_homogeneousOddPower_two_jet_bound (a k : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
       (R : ℝ) (hR : 0 ≤ R) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ f : (HomogeneousY a k), ‖f‖ ≤ R → ∀ n : ℕ, n ≤ 2 →
         ‖iteratedFDeriv ℝ n (homogeneousOddPower a k ha ha1 hk m) f‖ ≤ C := by
   …

   Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousOddPower

4. theorem OAI.DefocusingNLS.exists_homogeneousOddPower_derivative_lipschitz line 90

   Source documentation

   The real Fréchet derivative of the homogeneous odd-power map is uniformly Lipschitz on balls.

   theorem exists_homogeneousOddPower_derivative_lipschitz (a k : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
       (R : ℝ) (hR : 0 ≤ R) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ f g : (HomogeneousY a k), ‖f‖ ≤ R → ‖g‖ ≤ R →
         ‖fderiv ℝ (homogeneousOddPower a k ha ha1 hk m) f - fderiv ℝ (homogeneousOddPower a k ha ha1 hk m) g‖ ≤
           C * ‖f - g‖ := by
   …

   Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousOddPower