OAI/Analysis/KadisonKastler/WeakHilbertConvexLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Closed convex constraints on weak scalar limits

Separation retains closed convex conditions under a bounded Hilbert-space weak limit. Applied in L2, this retains almost-everywhere disk and positivity conditions for the scalar boundary averages.

  1. theorem OAI.KadisonKastler.mem_closed_convex_of_dual_tendsto line 22
  2. theorem OAI.KadisonKastler.dual_tendsto_of_inner_tendsto line 32
  3. theorem OAI.KadisonKastler.mem_closed_convex_of_inner_tendsto line 41
  4. theorem OAI.KadisonKastler.mem_closed_convex_of_pair_inner_tendsto line 54
  5. theorem OAI.KadisonKastler.isClosed_L2_ae_mem line 76
  6. theorem OAI.KadisonKastler.convex_L2_ae_mem line 84
  7. theorem OAI.KadisonKastler.L2_ae_mem_of_inner_tendsto line 93