OAI/Analysis/KadisonKastler/ScalarPullbackWeakGraph.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Weak closure of the nonsingular pullback graph

Pullback need not be a bounded operator on L2. Its graph is nonetheless closed: norm-convergent pairs have subsequences converging pointwise, and nonsingularity transports the first almost-everywhere limit. Linearity then makes this graph weakly closed. This suffices for the boundary averages.

  1. def OAI.KadisonKastler.scalarL2PullbackGraph line 23
  2. theorem OAI.KadisonKastler.isClosed_scalarL2PullbackGraph line 27
  3. theorem OAI.KadisonKastler.convex_scalarL2PullbackGraph line 45
  4. theorem OAI.KadisonKastler.scalarL2PullbackGraph_of_inner_tendsto line 57
  5. theorem OAI.KadisonKastler.scalarInfinityPullback_of_weak_limits line 69