OAI/NumberTheory/CubicMoment/Decomposition/StoppedMatrixDyads.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact independent sharp side dyads for the stopped matrices. The squarefree product envelope supplies the side support; no coprimality restriction or boundary contribution is discarded.

  1. def OAI.CubicFirstMoment.stoppedFactorSupport line 13
  2. lemma OAI.CubicFirstMoment.centralProduct_factor_support line 16
  3. lemma OAI.CubicFirstMoment.stopped_matrix_side_support line 26
  4. lemma OAI.CubicFirstMoment.finite_matrix_stopped_dyads line 53
  5. lemma OAI.CubicFirstMoment.stopped_matrix_dyadic line 69
  6. lemma OAI.CubicFirstMoment.stoppedFactorSupport_log_count line 82