OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousRadialPairL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The two-channel radial L² obstruction

A lower bound for the sum of the two squared amplitudes already excludes joint square integrability. No fixed choice of a dominant channel is needed.

  1. theorem OAI.DefocusingNLS.radial_pair_energy_integrable line 16
  2. theorem OAI.DefocusingNLS.radial_pair_not_integrable_of_energy_lower line 25
  3. theorem OAI.DefocusingNLS.radial_pair_not_integrable_of_norm_lower line 53
  4. theorem OAI.DefocusingNLS.radial_pair_not_integrable_of_defect_bound line 67

    Source documentation

    Transfer a nonzero-defect energy lower bound through a derivative estimate.

    theorem radial_pair_not_integrable_of_defect_bound
    (f g : ℝ → ℂ) (E : ℝ → ℝ) (R beta d c C : ℝ)
    (hc : 0 < c) (hC : 0 < C) (hb : -6 ≤ beta - d)
    (hElower : ∀ᶠ r in atTop, c ≤ r ^ (2 * d) * E r)
    (hderiv : ∀ᶠ r in atTop, r ^ (2 * beta) * E r ≤ C * homogeneousPairEnergy (f r, g r)) :
    ¬ (IntegrableOn (fun r => r ^ (11 : ℕ) * ‖f r‖ ^ 2) (Ioi R) ∧
      IntegrableOn (fun r => r ^ (11 : ℕ) * ‖g r‖ ^ 2) (Ioi R)) := by
…

    Mentions: OAI.DefocusingNLS.homogeneousPairEnergy