OAI/Analysis/ModularTheory/WeightRightMultiplier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Right multiplication by a contractive translation multiplier decreases the core square weight. This follows from the proved scalar-compression commutation, independently of traciality.

  1. lemma OAI.WeakPureInfiniteness.commuting_contraction_compression_le line 16
  2. lemma OAI.WeakPureInfiniteness.modularCoreSquareWeight_rightMultiplier line 39