OAI/NumberTheory/CubicGram/CubicOperator.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Finite cubic sieve operators, bilinear norms and coprime completion.

  1. def OAI.CubicFirstMoment.primarySmoothedSieveMass line 16
  2. lemma OAI.CubicFirstMoment.primarySmoothedSieveMass_gram line 21
  3. lemma OAI.CubicFirstMoment.primaryPrime_mem_factors line 64
  4. lemma OAI.CubicFirstMoment.primaryPrime_mem_factors_iff line 74
  5. lemma OAI.CubicFirstMoment.primeSet_subset_factors_of_prod_dvd line 78
  6. lemma OAI.CubicFirstMoment.primary_moebius_universal_indicator line 85
  7. theorem OAI.CubicFirstMoment.coprime_bilinear_moebius line 112
  8. def OAI.CubicFirstMoment.finiteCubicOperator line 154
  9. def OAI.CubicFirstMoment.finiteCubicBound line 158
  10. lemma OAI.CubicFirstMoment.finiteCubicBound_nonneg line 160
  11. lemma OAI.CubicFirstMoment.finiteCubicOperator_apply line 163
  12. lemma OAI.CubicFirstMoment.finiteCubicBound_controls_mass line 173
  13. def OAI.CubicFirstMoment.euclideanConj line 192
  14. lemma OAI.CubicFirstMoment.euclideanConj_norm line 195
  15. def OAI.CubicFirstMoment.matrixHilbertOperator line 200
  16. lemma OAI.CubicFirstMoment.matrixHilbertOperator_conj line 204
  17. lemma OAI.CubicFirstMoment.matrixHilbertOperator_conj_norm_le line 213
  18. lemma OAI.CubicFirstMoment.matrixHilbertOperator_conj_norm line 223
  19. lemma OAI.CubicFirstMoment.matrixHilbertOperator_transpose_norm line 231
  20. theorem OAI.CubicFirstMoment.finiteCubicBound_symm line 242
  21. theorem OAI.CubicFirstMoment.finiteCubicBound_bilinear line 257
  22. theorem OAI.CubicFirstMoment.finiteCubicBound_conjugate_bilinear line 286
  23. lemma OAI.CubicFirstMoment.coefficientVector_norm_sq line 309
  24. lemma OAI.CubicFirstMoment.finiteCubicOperator_norm_sq line 315
  25. lemma OAI.CubicFirstMoment.finiteCubicBound_le_iff line 324
  26. lemma OAI.CubicFirstMoment.finiteCubicBound_mono line 353
  27. lemma OAI.CubicFirstMoment.finiteCubicBound_mul_support_le line 373
  28. lemma OAI.CubicFirstMoment.norm_idealMoebius_le_one line 407

    Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Transform/MetaplecticAuxiliary.lean:55 (different declaration text). Qualify references as OAI.CubicFirstMoment.norm_idealMoebius_le_one@path.

  29. theorem OAI.CubicFirstMoment.finiteCubicBound_coprime_bilinear line 416