OAI/NumberTheory/CubicMoment/Decomposition/StoppedDyadPartition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Sharp dyads with the strict lower endpoint used by stopped rows. The partition is finite and its count depends only on the norm envelope.

  1. def OAI.CubicFirstMoment.stoppedNormDyadIndex line 13
  2. def OAI.CubicFirstMoment.stoppedNormDyad line 15
  3. def OAI.CubicFirstMoment.stoppedNormDyadLength line 18
  4. lemma OAI.CubicFirstMoment.stoppedNormDyadLength_pos line 20
  5. lemma OAI.CubicFirstMoment.stoppedNormDyad_bounds line 24
  6. lemma OAI.CubicFirstMoment.stoppedNormDyad_outer_bounds line 49
  7. lemma OAI.CubicFirstMoment.stoppedNormDyad_partition line 70
  8. lemma OAI.CubicFirstMoment.stoppedNormDyad_count line 78