OAI/NumberTheory/CubicGram/InnerExtension.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Full inner cube covers and sharp coefficient extension bounds.

  1. lemma OAI.CubicFirstMoment.complex_norm_sum_sq_le line 15
  2. lemma OAI.CubicFirstMoment.innerCubeBlock_fixed_mass line 22
  3. theorem OAI.CubicFirstMoment.innerCubeBlock_mass line 41
  4. def OAI.CubicFirstMoment.finiteCoverCoefficient line 84
  5. lemma OAI.CubicFirstMoment.finiteCoverCoefficient_norm_le line 88
  6. lemma OAI.CubicFirstMoment.finiteCoverCoefficient_sum line 100
  7. abbrev OAI.CubicFirstMoment.InnerCubeIndex line 124
  8. def OAI.CubicFirstMoment.innerCubeIndices line 126
  9. def OAI.CubicFirstMoment.innerCubeValue line 131
  10. lemma OAI.CubicFirstMoment.frequencyDyad_subset_innerCubeImage line 134
  11. def OAI.CubicFirstMoment.innerCubeCoefficient line 150
  12. def OAI.CubicFirstMoment.innerCubeBlockSum line 153
  13. lemma OAI.CubicFirstMoment.innerCubeCoefficient_sum line 159
  14. lemma OAI.CubicFirstMoment.innerCubeCoefficient_block_mass line 176
  15. lemma OAI.CubicFirstMoment.complex_mass_sum_sq_le line 193
  16. theorem OAI.CubicFirstMoment.innerCubeCover_mass line 202
  17. theorem OAI.CubicFirstMoment.innerCubeBlock_sharp line 229
  18. theorem OAI.CubicFirstMoment.cubic_inner_extension_scaled line 287
  19. theorem OAI.CubicFirstMoment.cubic_inner_extension line 342