OAI/Analysis/ModularTheory/FiniteProjections.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite-weight Fourier interval projections in the actual modular core.

  1. def OAI.WeakPureInfiniteness.modularFiniteProjection line 17
  2. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_apply line 22
  3. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_isStarProjection line 26
  4. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_norm_le line 31
  5. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_mem line 38
  6. lemma OAI.WeakPureInfiniteness.vectorLpProjection_scalarInclusion line 53
  7. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_fourierInclusion line 66
  8. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_weightVector line 80
  9. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_weightVector_comm line 87
  10. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_weight line 101
  11. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_finite line 118
  12. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_weightGNS line 123