OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzSamplingJetBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite physical jet control of expanding-torus sampling

A fixed finite set of physical Schwartz derivatives controls every sampled vector, uniformly for all periods L ≥ 1. The test function may vary with L.

  1. def OAI.DefocusingNLS.samplingDecaySeminorm line 18
  2. theorem OAI.DefocusingNLS.samplingDecaySeminorm_continuous line 21
  3. theorem OAI.DefocusingNLS.decay_le_samplingDecaySeminorm line 25
  4. theorem OAI.DefocusingNLS.exists_schwartzTorusSample_physicalJet_bound line 31