OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSecondMomentWeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The inverse-weight moment needed for classical second derivatives

In dimension twelve, k > 8 makes |xi|⁴ divided by the Y weight integrable. At the origin the factor |xi|⁴ only improves the existing inverse-weight estimate. This is the exact moment required for the physical C² bridge.

  1. theorem OAI.DefocusingNLS.homogeneous_secondMoment_high_bound line 18
  2. theorem OAI.DefocusingNLS.integrable_homogeneousSecondMomentWeight line 34