OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPrincipalPotential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The physical principal potential on L²

The actual odd-power derivative acts pointwise on every ordered spatial derivative. Its L² bound is independent of the derivative order; only the lower commutator terms require separate compact-error estimates.

  1. theorem OAI.DefocusingNLS.norm_oddPowerDerivative_le line 19
  2. theorem OAI.DefocusingNLS.norm_schrodingerOddPowerDerivative_le line 37
  3. theorem OAI.DefocusingNLS.principalPotential_memLp line 42
  4. def OAI.DefocusingNLS.homogeneousPrincipalAction line 62
  5. theorem OAI.DefocusingNLS.homogeneousPrincipalAction_ae line 68
  6. theorem OAI.DefocusingNLS.homogeneousPrincipalAction_norm_le line 74
  7. def OAI.DefocusingNLS.homogeneousPrincipalPotential line 84
  8. theorem OAI.DefocusingNLS.homogeneousPrincipalPotential_norm_le line 111
  9. theorem OAI.DefocusingNLS.homogeneousPrincipalPotential_energy_le line 117
  10. theorem OAI.DefocusingNLS.homogeneousPrincipalPotential_ordered_energy_le line 131

    Source documentation

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

    theorem homogeneousPrincipalPotential_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) (homogeneousPrincipalPotential m Q hQ M hM hQB (f j)) ≤
      ((2 * (m : ℝ) + 1) * M) * ∑ j, ‖f j‖ ^ 2 := by
…

    Mentions: OAI.DefocusingNLS.homogeneousPrincipalPotential