OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzCoreSampling.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform sampling of the fixed compact core of a profile

  1. theorem OAI.DefocusingNLS.exists_schwartz_weightedJet_bound line 13
  2. theorem OAI.DefocusingNLS.exists_schwartzCore_sampling_bound line 23