OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingWeightedLocal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local estimates for the exponentially weighted Picard map

The Lipschitz estimate is needed only along the two paths being compared. This permits the polynomial nonlinearity to be used on a bounded path ball without replacing it by a globally Lipschitz map.

  1. theorem OAI.DefocusingNLS.expandingBieleckiPicard_pair_dist_le line 18
  2. theorem OAI.DefocusingNLS.expandingTimeWeight_zero line 64
  3. theorem OAI.DefocusingNLS.expandingBieleckiPicard_zero_bound line 71