OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingWeightContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform continuity estimates for the exact expanding weights

The weight is the Euclidean norm of two scalar power components. This gives one frequency-independent modulus of continuity for the scale-transfer map.

  1. def OAI.DefocusingNLS.expandingWeightProfile line 13
  2. theorem OAI.DefocusingNLS.norm_expandingWeightProfile line 17
  3. theorem OAI.DefocusingNLS.expandingSobolevWeight_eq_profile line 37
  4. theorem OAI.DefocusingNLS.expandingSobolevWeight_difference_le line 44

    Source documentation

    One modulus controls every Fourier weight relative to the radius-one weight.

    theorem expandingSobolevWeight_difference_le (a k L M : ℝ)
    (hL : 1 ≤ L) (hM : 1 ≤ M) (n : frequencyLattice) :
    |expandingSobolevWeight a k L n - expandingSobolevWeight a k M n| ≤
      (|L ^ a - M ^ a| + |L ^ (6 - k) - M ^ (6 - k)|) *
        expandingSobolevWeight a k 1 n := by
…

    Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingSobolevWeight

  5. theorem OAI.DefocusingNLS.expandingScaleRatio_difference_le line 90

    Source documentation

    The diagonal transfer coefficients have a common modulus in the scale.

    theorem expandingScaleRatio_difference_le (a k L M : ℝ)
    (hL : 1 ≤ L) (hM : 1 ≤ M) (n : frequencyLattice) :
    |expandingScaleRatio a k 1 L n - expandingScaleRatio a k 1 M n| ≤
      |L ^ a - M ^ a| + |L ^ (6 - k) - M ^ (6 - k)| := by
…

    Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingScaleRatio