OAI/Analysis/RieszRectifiability/Limits/WeakL2Subsequence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weak subsequences of bounded L² sequences

A bounded sequence in a separable Hilbert space admits a weakly convergent subsequence whose limit obeys the same norm bound. For real L² functions, the Hilbert-space pairings become integrals against arbitrary L² tests.

  1. theorem OAI.RieszRectifiability.bounded_hilbert_sequence_weak_subsequence line 21
  2. theorem OAI.RieszRectifiability.bounded_L2_sequence_weak_subsequence line 48