OAI/MathematicalPhysics/DefocusingNLS/Linear/TorusPrincipalPotential.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The order-independent principal energy estimate on torus L²

The actual odd-power derivative is applied to each physical derivative component. Its bound uses the profile supremum, independently of the number of derivatives; commutators are treated separately.

  1. theorem OAI.DefocusingNLS.torusPrincipalPotential_memLp line 22
  2. def OAI.DefocusingNLS.torusPrincipalAction line 42
  3. theorem OAI.DefocusingNLS.torusPrincipalAction_ae line 48
  4. theorem OAI.DefocusingNLS.torusPrincipalAction_norm_le line 54
  5. def OAI.DefocusingNLS.torusPrincipalPotential line 64
  6. theorem OAI.DefocusingNLS.torusPrincipalPotential_norm_le line 91
  7. theorem OAI.DefocusingNLS.torusPrincipalPotential_energy_le line 97
  8. theorem OAI.DefocusingNLS.torusPrincipalPotential_ordered_energy_le line 111

    Source documentation

    Every ordered derivative receives the same pointwise operator; the constant is independent of the number of derivatives.

    theorem torusPrincipalPotential_ordered_energy_le (m N : ℕ)
    (Q : E → ℂ) (hQ : Continuous Q) (M : ℝ) (hM : 0 ≤ M)
    (hQB : ∀ x, ‖Q x‖ ^ (2 * m) ≤ M)
    (f : (Fin N → Fin 12) → Lp ℂ 2 (volume : Measure E)) :
    ∑ j, inner ℝ (f j) (torusPrincipalPotential m Q hQ M hM hQB (f j)) ≤
      ((2 * (m : ℝ) + 1) * M) * ∑ j, ‖f j‖ ^ 2 := by
…

    Mentions: OAI.DefocusingNLS.torusPrincipalPotential