OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousHamiltonian.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact frozen-potential energy cancellation

The principal odd-power linearization is skew for its positive anisotropic quadratic form. This is the scalar cancellation needed before estimating spatially varying coefficients and lower derivatives.

  1. theorem OAI.DefocusingNLS.oddPowerDerivative_rotated line 18
  2. theorem OAI.DefocusingNLS.oddPowerLinearization_rotated_components line 34
  3. def OAI.DefocusingNLS.frozenHamiltonianEnergy line 50
  4. theorem OAI.DefocusingNLS.frozenHamiltonianEnergy_bounds line 53
  5. theorem OAI.DefocusingNLS.frozenHamiltonianEnergy_cancellation line 71
  6. theorem OAI.DefocusingNLS.hasDerivAt_frozenHamiltonianEnergy line 80
  7. def OAI.DefocusingNLS.normalizedFrozenHamiltonianEnergy line 96
  8. theorem OAI.DefocusingNLS.normalizedFrozenHamiltonianEnergy_bounds line 100

    Source documentation

    Dividing by the frozen amplitude gives coercivity independent of that amplitude.

    theorem normalizedFrozenHamiltonianEnergy_bounds (m : ℕ) (q v : ℂ) (hq : q ≠ 0) :
    ‖v‖ ^ 2 ≤ normalizedFrozenHamiltonianEnergy m q v ∧
      normalizedFrozenHamiltonianEnergy m q v ≤ (2 * (m : ℝ) + 1) * ‖v‖ ^ 2 := by
…

    Mentions: OAI.DefocusingNLS.normalizedFrozenHamiltonianEnergy

  9. theorem OAI.DefocusingNLS.hasDerivAt_normalizedFrozenHamiltonianEnergy line 111