OAI/Analysis/ModularTheory/FiniteWeightSpace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite-square-weight domain and its concrete Hilbert-space map. The norm on its image is the actual modular L² norm.

  1. lemma OAI.WeakPureInfiniteness.modularCoreSquareWeight_smul_finite line 17
  2. lemma OAI.WeakPureInfiniteness.modularCoreSquareWeight_star_finite line 25
  3. def OAI.WeakPureInfiniteness.modularFiniteWeightSpace line 32
  4. lemma OAI.WeakPureInfiniteness.modularWeightVector_smul line 41
  5. def OAI.WeakPureInfiniteness.modularFiniteWeightMap line 53
  6. lemma OAI.WeakPureInfiniteness.modularFiniteWeightMap_injective line 60
  7. lemma OAI.WeakPureInfiniteness.modularWeightVector_star_norm line 74