OAI/NumberTheory/DirichletL/Descent/Hybrid.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseMoment.inverseCubicKernel line 16
  2. theorem OAI.SevenEighths.InverseMoment.inverseCubicKernel_eq_inverse_square line 20
  3. theorem OAI.SevenEighths.InverseMoment.inverseCubicKernel_norm_le_one line 27
  4. def OAI.SevenEighths.InverseMoment.hybridCubicCoefficient line 32
  5. theorem OAI.SevenEighths.InverseMoment.dyadic_normalized_coefficient_energy line 37
  6. theorem OAI.SevenEighths.InverseMoment.hybridCubicCoefficient_energy line 67
  7. theorem OAI.SevenEighths.InverseMoment.inverseCubicKernel_mul_left line 80
  8. theorem OAI.SevenEighths.InverseMoment.inverseCubicKernel_mul_right line 85
  9. theorem OAI.SevenEighths.InverseMoment.inverseCubicKernel_quotients line 93
  10. theorem OAI.SevenEighths.InverseMoment.inverseCubicKernel_eq_zero_of_not_coprime line 102
  11. theorem OAI.SevenEighths.InverseMoment.hybrid_cubic_column_mask line 111
  12. theorem OAI.SevenEighths.InverseMoment.hybrid_original_kernel_decomposition line 130
  13. theorem OAI.SevenEighths.InverseMoment.hybrid_kernel_quotients line 157
  14. def OAI.SevenEighths.InverseMoment.hybridColumnCoefficient line 174
  15. theorem OAI.SevenEighths.InverseMoment.hybridColumnCoefficient_norm_le_one line 180
  16. theorem OAI.SevenEighths.InverseMoment.normalized_ideal_product_weight line 192
  17. theorem OAI.SevenEighths.InverseMoment.hybrid_extracted_block_identity line 200
  18. def OAI.SevenEighths.InverseMoment.hybridInner line 219
  19. def OAI.SevenEighths.InverseMoment.hybridRow line 226
  20. def OAI.SevenEighths.InverseMoment.hybridDivisorTerm line 231
  21. theorem OAI.SevenEighths.InverseMoment.hybridRow_mobius line 237
  22. theorem OAI.SevenEighths.InverseMoment.hybrid_first_mask_energy line 256
  23. def OAI.SevenEighths.InverseMoment.doubleMaskRow line 288
  24. def OAI.SevenEighths.InverseMoment.doubleMaskDivisorTerm line 292
  25. theorem OAI.SevenEighths.InverseMoment.doubleMaskRow_mobius line 297
  26. theorem OAI.SevenEighths.InverseMoment.hybrid_double_mask_energy line 317