OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialVolterraWeight.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A Bielecki estimate for the nonsingular radial initial-value integral.

  1. def OAI.DefocusingNLS.radialVolterra line 10
  2. theorem OAI.DefocusingNLS.radialVolterra_eq_neg_kernel line 13
  3. theorem OAI.DefocusingNLS.hasDerivAt_radialVolterra line 18
  4. theorem OAI.DefocusingNLS.radialVolterra_sub line 26
  5. theorem OAI.DefocusingNLS.radialVolterra_norm_le line 34
  6. theorem OAI.DefocusingNLS.radialAverage_exponential_bound line 39
  7. theorem OAI.DefocusingNLS.integral_exp_scale line 48
  8. theorem OAI.DefocusingNLS.radialVolterra_exponential_bound line 57