OAI/NumberTheory/CubicGram/CubeExtraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Primary cube decomposition and finite operator block bounds.

  1. lemma OAI.CubicFirstMoment.primary_of_primary_mul_left line 16
  2. theorem OAI.CubicFirstMoment.primary_cube_decomposition line 21
  3. lemma OAI.CubicFirstMoment.cubicSymbol_pow_upper line 51
  4. lemma OAI.CubicFirstMoment.finiteCubicBound_twist_controls_mass line 63
  5. lemma OAI.CubicFirstMoment.finiteCubicBound_twist_conjugate_mass line 75
  6. def OAI.CubicFirstMoment.cubeBlockMass line 91
  7. lemma OAI.CubicFirstMoment.cubeBlockMass_le_first line 95
  8. lemma OAI.CubicFirstMoment.cubeBlockMass_le_second line 120
  9. theorem OAI.CubicFirstMoment.cubeBlockMass_le_min line 146
  10. def OAI.CubicFirstMoment.cubeBlockSupport line 158
  11. lemma OAI.CubicFirstMoment.cubeBlockSupport_mass_le line 161
  12. theorem OAI.CubicFirstMoment.finiteCubicBound_cubeBlock line 175