OAI/Analysis/ModularTheory/OriginalNorm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Evaluation at time zero transfers the modular product norm bound to the original left/right representation.

  1. lemma OAI.WeakPureInfiniteness.modularLp_product_ae line 16
  2. lemma OAI.WeakPureInfiniteness.modularLp_product_sum_ae line 26
  3. lemma OAI.WeakPureInfiniteness.modularLp_product_sum_norm_ge line 45
  4. lemma OAI.WeakPureInfiniteness.modularRight_product_sum_norm_ge line 64