OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousRegularPrimitive.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Twice differentiable regular Volterra primitives at the origin

  1. theorem OAI.DefocusingNLS.homogeneousRegularSlope_hasDerivAt line 13
  2. theorem OAI.DefocusingNLS.homogeneousRegularAverage_zero line 47
  3. theorem OAI.DefocusingNLS.homogeneousRegular_mul_at_zero line 61
  4. theorem OAI.DefocusingNLS.homogeneousRegularPrimitive_contDiff_two line 71
  5. theorem OAI.DefocusingNLS.homogeneousRegularLift_contDiff_two line 105
  6. theorem OAI.DefocusingNLS.homogeneousRegularPhysical_contDiff_two line 112