OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffPointwiseBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A scale- and derivative-order independent bound for a sampled cutoff

  1. theorem OAI.DefocusingNLS.norm_tsum_le_of_disjoint line 16
  2. theorem OAI.DefocusingNLS.sampledCutoff_pointwise_bound line 28