OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousDefectEnergy.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A power lower bound for a nonzero transverse radial defect

The large imaginary diagonal in the radial equation does not enter this energy estimate. An integrable O(r⁻³) perturbation only changes the positive lower-bound constant, not the radial power.

  1. def OAI.DefocusingNLS.homogeneousPairEnergy line 24
  2. def OAI.DefocusingNLS.homogeneousPairReal line 27
  3. theorem OAI.DefocusingNLS.homogeneousPairEnergy_nonneg line 30
  4. theorem OAI.DefocusingNLS.homogeneousPairEnergy_eq_norms line 34
  5. theorem OAI.DefocusingNLS.homogeneousPairEnergy_lower line 38
  6. theorem OAI.DefocusingNLS.homogeneousPairEnergy_upper line 46
  7. theorem OAI.DefocusingNLS.homogeneousPairEnergy_pos line 52
  8. theorem OAI.DefocusingNLS.homogeneousPairReal_bound line 56
  9. theorem OAI.DefocusingNLS.homogeneousComplexNormSq_hasDerivAt line 68
  10. theorem OAI.DefocusingNLS.homogeneousPairEnergy_hasDerivAt line 79
  11. theorem OAI.DefocusingNLS.homogeneousPairReal_damping line 88
  12. theorem OAI.DefocusingNLS.homogeneousPairEnergy_damping_lower line 100
  13. def OAI.DefocusingNLS.homogeneousDefectWeight line 122
  14. theorem OAI.DefocusingNLS.homogeneousDefectWeight_hasDerivAt line 125
  15. theorem OAI.DefocusingNLS.homogeneousDefectWeight_pos line 141
  16. theorem OAI.DefocusingNLS.homogeneousDefectWeight_le line 144
  17. theorem OAI.DefocusingNLS.homogeneousDefectEnergy_monotone line 152

    Source documentation

    The normalized squared defect is monotone on every positive tail.

    theorem homogeneousDefectEnergy_monotone (E E' : ℝ → ℝ) (d M R : ℝ)
    (hR : 0 < R) (hE : ∀ r, R ≤ r → HasDerivAt E (E' r) r)
    (hlower : ∀ r, R ≤ r → -(2 * d / r + 4 * M / r ^ 3) * E r ≤ E' r) :
    MonotoneOn (fun r => homogeneousDefectWeight d M r * E r) (Ici R) := by
…

    Mentions: OAI.DefocusingNLS.homogeneousDefectWeight

  18. theorem OAI.DefocusingNLS.homogeneousDefectEnergy_power_lower line 174

    Source documentation

    A positive squared defect stays above a positive multiple of its radial power.

    theorem homogeneousDefectEnergy_power_lower (E E' : ℝ → ℝ) (d M R : ℝ)
    (hM : 0 ≤ M) (hR : 0 < R) (hE0 : 0 < E R)
    (hEn : ∀ r, R ≤ r → 0 ≤ E r)
    (hE : ∀ r, R ≤ r → HasDerivAt E (E' r) r)
    (hlower : ∀ r, R ≤ r → -(2 * d / r + 4 * M / r ^ 3) * E r ≤ E' r) :
    ∃ c : ℝ, 0 < c ∧ ∀ r, R ≤ r → c ≤ r ^ (2 * d) * E r := by
…
  19. theorem OAI.DefocusingNLS.homogeneousDefect_nonzero_power_bound line 188