OAI/MathematicalPhysics/BFSS/WeakLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weak subsequences, closed convex graphs and lower semicontinuity.

  1. theorem OAI.BFSSNormalAnalysis.bounded_weak_subsequence line 13
  2. theorem OAI.BFSSNormalAnalysis.strong_weak_mem_closed_convex line 32
  3. theorem OAI.BFSSNormalAnalysis.weak_norm_sq_le_limit line 60
  4. theorem OAI.BFSSNormalAnalysis.weak_norm_sq_add_le_limit line 82