OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowConjugation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Schwarz conjugation of the actual regularized H integral and its boundary column.

  1. theorem OAI.DefocusingNLS.star_cpow_of_mem_slit line 12
  2. theorem OAI.DefocusingNLS.regularizedSlowKernel_star line 17
  3. theorem OAI.DefocusingNLS.regularizedSlowSolution_star line 28
  4. theorem OAI.DefocusingNLS.slowBoundaryColumn_star line 42