OAI/MathematicalPhysics/DefocusingNLS/Linear/WeakLinearCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Linear coordinates of a weak limit

  1. theorem OAI.DefocusingNLS.weakLimit_map_eq_zero line 16
  2. theorem OAI.DefocusingNLS.tendsto_finite_coordinates_of_weak line 31