OAI/Analysis/ModularTheory/WeightGram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality of increments of the actual modular cutoff vectors after applying a core operator. This is the Hilbert-space estimate for constructing the finite-weight GNS vector, without a traciality assumption.

  1. lemma OAI.WeakPureInfiniteness.modularFourierCompression_inner line 19
  2. lemma OAI.WeakPureInfiniteness.modularFourierCompression_square_inner line 28
  3. lemma OAI.WeakPureInfiniteness.modularCoreWeightVector_gram line 38
  4. lemma OAI.WeakPureInfiniteness.modularCoreWeightVector_difference_sq line 74
  5. lemma OAI.WeakPureInfiniteness.modularCoreWeightVector_norm_sq_le line 86
  6. lemma OAI.WeakPureInfiniteness.modularCoreWeightVector_norm_sq_tendsto line 93
  7. lemma OAI.WeakPureInfiniteness.modularCoreWeightVector_cauchy line 117
  8. theorem OAI.WeakPureInfiniteness.exists_modularCoreWeightVector_limit line 142